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.
Category of categories.
@[instance]
Equations
- category_theory.Cat.inhabited = {default := {α := Type u, str := category_theory.types}}
@[instance]
Equations
@[instance]
Construct a bundled Cat from the underlying type and the typeclass.
Equations
@[instance]
Category structure on Cat
Equations
- category_theory.Cat.category = {to_category_struct := {to_has_hom := {hom := λ (C D : category_theory.Cat), ↥C ⥤ ↥D}, id := λ (C : category_theory.Cat), 𝟭 ↥C, comp := λ (C D E : category_theory.Cat) (F : C ⟶ D) (G : D ⟶ E), F ⋙ G}, id_comp' := category_theory.Cat.category._proof_1, comp_id' := category_theory.Cat.category._proof_2, assoc' := category_theory.Cat.category._proof_3}
Functor that gets the set of objects of a category. It is not
called forget, because it is not a faithful functor.
Equations
- category_theory.Cat.objects = {obj := λ (C : category_theory.Cat), ↥C, map := λ (C D : category_theory.Cat) (F : C ⟶ D), F.obj, map_id' := category_theory.Cat.objects._proof_1, map_comp' := category_theory.Cat.objects._proof_2}
Any isomorphism in Cat induces an equivalence of the underlying categories.
Equations
- category_theory.Cat.equiv_of_iso γ = {functor := γ.hom, inverse := γ.inv, unit_iso := category_theory.eq_to_iso _, counit_iso := category_theory.eq_to_iso _, functor_unit_iso_comp' := _}