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.

def CategoryTheory.Grpd :
Type (max (u + 1) u (v + 1))

Category of groupoids

Instances For

    Construct a bundled Grpd from the underlying type and the typeclass Groupoid.

    Instances For

      Functor that gets the set of objects of a groupoid. It is not called forget, because it is not a faithful functor.

      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
            noncomputable def CategoryTheory.Grpd.piIsoPi (J : Type u) (f : JCategoryTheory.Grpd) :
            CategoryTheory.Grpd.of ((j : J) → ↑(f j)) f

            The product of a family of groupoids is isomorphic to the product object in the category of Groupoids

            Instances For