Library Groupoid

Require Import Utf8.
Require Export Category.
Require Import Notations Common CategoryIsomorphisms ComputableCategory.

Set Implicit Arguments.

Generalizable All Variables.


Definition A groupoid is a category C such that every morphism is an isomorphism. If C and D are groupoids, a morphism of groupoids, denoted F : C D, is simply a functor. The category of groupoids is denoted Grpd.

Class IsGroupoid `(C : @Category obj) :=
  { is_groupoid :> s d (m : Morphism C s d),
                     IsomorphismOf m }.

Record > Groupoid :=
    GroupoidType :> Type;
    GroupoidCategory :> @Category GroupoidType;
    GroupoidIsGroupoid :> IsGroupoid GroupoidCategory

Existing Instance GroupoidIsGroupoid.

Definition CategoryOfGroupoids : @Category Groupoid :=
  Eval hnf in @ComputableCategory _ _ GroupoidCategory.