Category of categories #

This file contains the definition of the category Cat of all categories. In this category objects are categories and morphisms are functors between these categories.

Implementation notes #

Though Cat is not a concrete category, we use bundled to define its carrier type.

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

Category of categories.

Instances For

    Construct a bundled Cat from the underlying type and the typeclass.

    Instances For
      theorem CategoryTheory.Cat.id_map {C : CategoryTheory.Cat} {X : C} {Y : C} (f : X Y) :
      theorem CategoryTheory.Cat.comp_obj {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} {E : CategoryTheory.Cat} (F : C D) (G : D E) (X : C) :
      (CategoryTheory.CategoryStruct.comp F G).obj X = G.obj (F.obj X)
      theorem CategoryTheory.Cat.comp_map {C : CategoryTheory.Cat} {D : CategoryTheory.Cat} {E : CategoryTheory.Cat} (F : C D) (G : D E) {X : C} {Y : C} (f : X Y) :
      (CategoryTheory.CategoryStruct.comp F G).map f = ( f)

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

      Instances For

        Any isomorphism in Cat induces an equivalence of the underlying categories.

        Instances For
          theorem CategoryTheory.typeToCat_map {X : Type u} {Y : Type u} (f : X Y) :
 f = id (CategoryTheory.Discrete.functor ( f))

          Embedding Type into Cat as discrete categories.

          This ought to be modelled as a 2-functor!

          Instances For