Category of groupoids #
This file contains the definition of the category Grpd
of all groupoids.
In this category objects are groupoids and morphisms are functors
between these groupoids.
We also provide two “forgetting” functors: objects : Grpd ⥤ Type
and forgetToCat : Grpd ⥤ Cat
.
Implementation notes #
Though Grpd
is not a concrete category, we use Bundled
to define
its carrier type.
Construct a bundled Grpd
from the underlying type and the typeclass Groupoid
.
Instances For
Category structure on Grpd
Functor that gets the set of objects of a groupoid. It is not
called forget
, because it is not a faithful functor.
Instances For
Forgetting functor to Cat
Instances For
Convert arrows in the category of groupoids to functors, which sometimes helps in applying simp lemmas
Converts identity in the category of groupoids to the functor identity
Construct the product over an indexed family of groupoids, as a fan.
Instances For
The product fan over an indexed family of groupoids, is a limit cone.
Instances For
The product of a family of groupoids is isomorphic to the product object in the category of Groupoids