# Library Groupoid

Require Import Utf8.

Require Export Category.

Require Import Notations Common CategoryIsomorphisms ComputableCategory.

Set Implicit Arguments.

Generalizable All Variables.

# Groupoids

Definition 4.2.3.7. 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.