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?

instance CategoryTheory.Cat.HasLimits.categoryObjects {J : Type v} [SmallCategory J] {F : Functor J Cat} {j : J} : SmallCategory ((F.comp objects).obj j)

def CategoryTheory.Cat.HasLimits.homDiagram {J : Type v} [SmallCategory J] {F : Functor J Cat} (X Y : Limits.limit (F.comp objects)) : Functor J (Type v)

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

@[simp]

theorem CategoryTheory.Cat.HasLimits.homDiagram_map {J : Type v} [SmallCategory J] {F : Functor J Cat} (X Y : Limits.limit (F.comp objects)) {X✝ Y✝ : J} (f : X✝ ⟶ Y✝) (g : Limits.limit.π (F.comp objects) X✝ X ⟶ Limits.limit.π (F.comp objects) X✝ Y) : (homDiagram X Y).map f g = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((F.map f).toFunctor.map g) (eqToHom ⋯))

@[simp]

theorem CategoryTheory.Cat.HasLimits.homDiagram_obj {J : Type v} [SmallCategory J] {F : Functor J Cat} (X Y : Limits.limit (F.comp objects)) (j : J) : (homDiagram X Y).obj j = (Limits.limit.π (F.comp objects) j X ⟶ Limits.limit.π (F.comp objects) j Y)

instance CategoryTheory.Cat.HasLimits.instCategoryLimitCompObjects {J : Type v} [SmallCategory J] (F : Functor J Cat) : Category.{v, v} (Limits.limit (F.comp objects))

@[simp]

theorem CategoryTheory.Cat.HasLimits.comp_def {J : Type v} [SmallCategory J] (F : Functor J Cat) {X Y Z : Limits.limit (F.comp objects)} (f : Limits.limit (homDiagram X Y)) (g : Limits.limit (homDiagram Y Z)) : CategoryStruct.comp f g = Limits.Types.Limit.mk (homDiagram X Z) (fun (j : J) => CategoryStruct.comp (Limits.limit.π (homDiagram X Y) j f) (Limits.limit.π (homDiagram Y Z) j g)) ⋯

@[simp]

theorem CategoryTheory.Cat.HasLimits.id_def {J : Type v} [SmallCategory J] (F : Functor J Cat) (X : Limits.limit (F.comp objects)) : CategoryStruct.id X = Limits.Types.Limit.mk (homDiagram X X) (fun (x : J) => CategoryStruct.id (Limits.limit.π (F.comp objects) x X)) ⋯

def CategoryTheory.Cat.HasLimits.limitConeX {J : Type v} [SmallCategory J] (F : Functor J Cat) : Cat

Auxiliary definition: the limit category.

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitConeX_α {J : Type v} [SmallCategory J] (F : Functor J Cat) : ↑(limitConeX F) = Limits.limit (F.comp objects)

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitConeX_str {J : Type v} [SmallCategory J] (F : Functor J Cat) : (limitConeX F).str = inferInstance

def CategoryTheory.Cat.HasLimits.limitCone {J : Type v} [SmallCategory J] (F : Functor J Cat) : Limits.Cone F

Auxiliary definition: the cone over the limit category.

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitCone_π_app {J : Type v} [SmallCategory J] (F : Functor J Cat) (j : J) : (limitCone F).π.app j = { obj := Limits.limit.π (F.comp objects) j, map := fun {X Y : Limits.limit (F.comp objects)} (f : X ⟶ Y) => Limits.limit.π (homDiagram X Y) j f, map_id := ⋯, map_comp := ⋯ }.toCatHom

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitCone_pt {J : Type v} [SmallCategory J] (F : Functor J Cat) : (limitCone F).pt = limitConeX F

def CategoryTheory.Cat.HasLimits.limitConeLift {J : Type v} [SmallCategory J] (F : Functor J Cat) (s : Limits.Cone F) : s.pt ⟶ limitConeX F

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

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitConeLift_toFunctor {J : Type v} [SmallCategory J] (F : Functor J Cat) (s : Limits.Cone F) : (limitConeLift F s).toFunctor = { obj := Limits.limit.lift (F.comp objects) { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).toFunctor.obj, naturality := ⋯ } }, map := fun {X Y : ↑s.1} (f : X ⟶ Y) => Limits.Types.Limit.mk (homDiagram (Limits.limit.lift (F.comp objects) { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).toFunctor.obj, naturality := ⋯ } } X) (Limits.limit.lift (F.comp objects) { pt := ↑s.pt, π := { app := fun (j : J) => (s.π.app j).toFunctor.obj, naturality := ⋯ } } Y)) (fun (j : J) => CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp ((s.π.app j).toFunctor.map f) (eqToHom ⋯))) ⋯, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Cat.HasLimits.limit_π_homDiagram_eqToHom {J : Type v} [SmallCategory J] {F : Functor J Cat} (X Y : Limits.limit (F.comp objects)) (j : J) (h : X = Y) : Limits.limit.π (homDiagram X Y) j (eqToHom h) = eqToHom ⋯

def CategoryTheory.Cat.HasLimits.limitConeIsLimit {J : Type v} [SmallCategory J] (F : Functor J Cat) : Limits.IsLimit (limitCone F)

Auxiliary definition: the proposed cone is a limit cone.

instance CategoryTheory.Cat.instHasLimits : Limits.HasLimits Cat

The category of small categories has all small limits.

instance CategoryTheory.Cat.instPreservesLimitsObjects : Limits.PreservesLimits objects