mathlib3 documentation

category_theory.category.Cat

Category of categories #

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 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.

@[protected, instance]
Equations

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

Equations
@[protected, instance]

Bicategory structure on Cat

Equations
@[protected, instance]

Cat is a strict bicategory.

@[simp]
theorem category_theory.Cat.id_map {C : category_theory.Cat} {X Y : C} (f : X Y) :
(𝟙 C).map f = f
@[simp]
theorem category_theory.Cat.comp_obj {C D E : category_theory.Cat} (F : C D) (G : D E) (X : C) :
(F G).obj X = G.obj (F.obj X)
@[simp]
theorem category_theory.Cat.comp_map {C D E : category_theory.Cat} (F : C D) (G : D E) {X Y : C} (f : X Y) :
(F G).map f = G.map (F.map f)

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

Equations

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

Equations

Embedding Type into Cat as discrete categories.

This ought to be modelled as a 2-functor!

Equations
Instances for category_theory.Type_to_Cat