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.
Category of groupoids
Instances For
Equations
Equations
- C.str' = C.str
Equations
- CategoryTheory.Grpd.instCoeSortType = CategoryTheory.Bundled.coeSort
Functor that gets the set of objects of a groupoid. It is not
called forget
, because it is not a faithful functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Forgetting functor to Cat
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
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.
Equations
- CategoryTheory.Grpd.piLimitFan F = CategoryTheory.Limits.Fan.mk (CategoryTheory.Grpd.of ((j : J) → ↑(F j))) fun (j : J) => CategoryTheory.Pi.eval (fun (j : J) => ↑(F j)) j
Instances For
The product fan over an indexed family of groupoids, is a limit cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The product of a family of groupoids is isomorphic to the product object in the category of Groupoids
Equations
- CategoryTheory.Grpd.piIsoPi J f = (CategoryTheory.Grpd.piLimitFanIsLimit f).conePointUniqueUpToIso (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor f))