# The category of small categories has all small limits. #

An object in the limit consists of a family of objects, which are carried to one another by the functors in the diagram. A morphism between two such objects is a family of morphisms between the corresponding objects, which are carried to one another by the action on morphisms of the functors in the diagram.

## Future work #

Can the indexing category live in a lower universe?

Equations
• CategoryTheory.Cat.HasLimits.categoryObjects = (F.obj j).str
@[simp]
theorem CategoryTheory.Cat.HasLimits.homDiagram_map {J : Type v} (X : ) (Y : ) :
∀ {X_1 Y_1 : J} (f : X_1 Y_1) (g : ), .map f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((F.map f).map g) )
@[simp]
theorem CategoryTheory.Cat.HasLimits.homDiagram_obj {J : Type v} (X : ) (Y : ) (j : J) :
.obj j = ( )
def CategoryTheory.Cat.HasLimits.homDiagram {J : Type v} (X : ) (Y : ) :

Auxiliary definition: the diagram whose limit gives the morphism space between two objects of the limit category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Cat.HasLimits.instCategoryLimitCompObjects_comp {J : Type v} {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :
@[simp]
@[simp]
theorem CategoryTheory.Cat.HasLimits.limitConeX_str {J : Type v} :
= inferInstance

Auxiliary definition: the limit category.

Equations
• = { α := , str := inferInstance }
Instances For
@[simp]
theorem CategoryTheory.Cat.HasLimits.limitCone_π_app_map {J : Type v} (j : J) :
∀ {X Y : (.obj j)} (f : X Y), (.app j).map f =
@[simp]
theorem CategoryTheory.Cat.HasLimits.limitCone_π_app_obj {J : Type v} (j : J) :
∀ (a : ), (.app j).obj a =
@[simp]

Auxiliary definition: the cone over the limit category.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Cat.HasLimits.limitConeLift_obj {J : Type v} (s : ) :
∀ (a : { pt := s.pt, π := { app := fun (j : J) => (s.app j).obj, naturality := } }.pt), a = CategoryTheory.Limits.limit.lift () { pt := s.pt, π := { app := fun (j : J) => (s.app j).obj, naturality := } } a
@[simp]
theorem CategoryTheory.Cat.HasLimits.limitConeLift_map {J : Type v} (s : ) :
∀ {X Y : s.pt} (f : X Y), f = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram (CategoryTheory.Limits.limit.lift () { pt := s.pt, π := { app := fun (j : J) => (s.app j).obj, naturality := } } X) (CategoryTheory.Limits.limit.lift () { pt := s.pt, π := { app := fun (j : J) => (s.app j).obj, naturality := } } Y)) (fun (j : J) => CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((s.app j).map f) ))

Auxiliary definition: the universal morphism to the proposed limit cone.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Cat.HasLimits.limit_π_homDiagram_eqToHom {J : Type v} (X : ) (Y : ) (j : J) (h : X = Y) :

Auxiliary definition: the proposed cone is a limit cone.

Equations
• = { lift := , fac := , uniq := }
Instances For

The category of small categories has all small limits.

Equations
Equations
• One or more equations did not get rendered due to their size.