Category of groupoids #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file contains the definition of the category
Groupoid of all groupoids.
In this category objects are groupoids and morphisms are functors
between these groupoids.
We also provide two “forgetting” functors:
objects : Groupoid ⥤ Type
forget_to_Cat : Groupoid ⥤ Cat.
Implementation notes #
Groupoid is not a concrete category, we use
bundled to define
its carrier type.
Category of groupoids
Construct a bundled
Groupoid from the underlying type and the typeclass.
Category structure on
Functor that gets the set of objects of a groupoid. It is not
forget, because it is not a faithful functor.
Forgetting functor to
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.
The product fan over an indexed family of groupoids, is a limit cone.
The product of a family of groupoids is isomorphic
to the product object in the category of Groupoids