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} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} {j : J} : CategoryTheory.SmallCategory ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j)

@[simp]

theorem CategoryTheory.Cat.HasLimits.homDiagram_map {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} (X : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) (Y : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) : ∀ {X Y : J} (f : X ⟶ Y) (g : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) X X ⟶ CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) X Y), J.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Cat.HasLimits.homDiagram X Y).toPrefunctor X Y f g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) Y X = CategoryTheory.CategoryStruct.comp (Type v) CategoryTheory.Category.toCategoryStruct (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj X) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj Y) (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) X) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).map f) X)) (CategoryTheory.CategoryStruct.comp ((F.map f).map g) (CategoryTheory.eqToHom (_ : CategoryTheory.CategoryStruct.comp (Type v) CategoryTheory.Category.toCategoryStruct (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj X) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj Y) (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) X) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).map f) Y = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) Y Y)))

@[simp]

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

def CategoryTheory.Cat.HasLimits.homDiagram {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CategoryTheory.Cat} (X : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) (Y : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) : CategoryTheory.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.instCategoryLimitTypeTypesCompCatCategoryObjectsHasLimitSmall_self_comp {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) {X : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)} {Y : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)} {Z : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram X Z) (fun j => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram X Y) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram X Y)) j f) (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram Y Z) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram Y Z)) j g)) (_ : ∀ (j j' : J) (h : j ⟶ j'), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' X = CategoryTheory.CategoryStruct.comp (Type v) CategoryTheory.Category.toCategoryStruct (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j') (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).map h) X)) (CategoryTheory.CategoryStruct.comp ((F.map h).map (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram X Y) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram X Y)) j f) (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram Y Z) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram Y Z)) j g))) (CategoryTheory.eqToHom (_ : CategoryTheory.CategoryStruct.comp (Type v) CategoryTheory.Category.toCategoryStruct (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j') (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).map h) Z = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' Z))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram X Y) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram X Y)) j' f) (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram Y Z) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram Y Z)) j' g))

@[simp]

theorem CategoryTheory.Cat.HasLimits.instCategoryLimitTypeTypesCompCatCategoryObjectsHasLimitSmall_self_id {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (X : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) : CategoryTheory.CategoryStruct.id X = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram X X) (fun j => CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j X)) (_ : ∀ (j j' : J) (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' X = CategoryTheory.CategoryStruct.comp (Type v) CategoryTheory.Category.toCategoryStruct (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j') (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).map f) X)) (CategoryTheory.CategoryStruct.comp ((F.map f).map (CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j X))) (CategoryTheory.eqToHom (_ : CategoryTheory.CategoryStruct.comp (Type v) CategoryTheory.Category.toCategoryStruct (CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).obj j') (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) j) ((CategoryTheory.Functor.comp F CategoryTheory.Cat.objects).map f) X = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' X))) = CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' X))

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

@[simp]

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

@[simp]

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

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

Auxiliary definition: the limit category.

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitCone_π_app_obj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (j : J) : ∀ (a : CategoryTheory.Limits.limit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)), ((CategoryTheory.Cat.HasLimits.limitCone F).π.app j).obj a = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j a

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitCone_π_app_map {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (j : J) : ∀ {X Y : ↑(((CategoryTheory.Functor.const J).obj (CategoryTheory.Cat.HasLimits.limitConeX F)).obj j)} (f : X ⟶ Y), ((CategoryTheory.Cat.HasLimits.limitCone F).π.app j).map f = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Cat.HasLimits.homDiagram X Y) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Cat.HasLimits.homDiagram X Y)) j f

@[simp]

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

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

Auxiliary definition: the cone over the limit category.

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitConeLift_map {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (s : CategoryTheory.Limits.Cone F) : ∀ {X Y : ↑s.pt} (f : X ⟶ Y), (CategoryTheory.Cat.HasLimits.limitConeLift F s).map f = CategoryTheory.Limits.Types.Limit.mk (CategoryTheory.Cat.HasLimits.homDiagram (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.π.app j).obj } X) (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.π.app j).obj } Y)) (fun j => CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.π.app j).obj } X) = (s.π.app j).obj X)) (CategoryTheory.CategoryStruct.comp ((s.π.app j).map f) (CategoryTheory.eqToHom (_ : (s.π.app j).obj Y = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.π.app j).obj } Y))))) (_ : ∀ (j j' : J) (h : j ⟶ j'), J.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.Cat.HasLimits.homDiagram (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.π.app j).obj } X) (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.π.app j).obj } Y)).toPrefunctor j j' h (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.π.app j).obj } X) = (s.π.app j).obj X)) (CategoryTheory.CategoryStruct.comp ((s.π.app j).map f) (CategoryTheory.eqToHom (_ : (s.π.app j).obj Y = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.π.app j).obj } Y))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.π.app j).obj } X) = (s.π.app j').obj X)) (CategoryTheory.CategoryStruct.comp ((s.π.app j').map f) (CategoryTheory.eqToHom (_ : (s.π.app j').obj Y = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) j' (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.π.app j).obj } Y)))))

@[simp]

theorem CategoryTheory.Cat.HasLimits.limitConeLift_obj {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (s : CategoryTheory.Limits.Cone F) : ∀ (a : { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.π.app j).obj }.pt), (CategoryTheory.Cat.HasLimits.limitConeLift F s).obj a = CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects) (_ : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.comp F CategoryTheory.Cat.objects)) { pt := ↑s.pt, π := CategoryTheory.NatTrans.mk fun j => (s.π.app j).obj } a

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

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

@[simp]

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

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

Auxiliary definition: the proposed cone is a limit cone.

instance CategoryTheory.Cat.instHasLimitsCatCategory : CategoryTheory.Limits.HasLimits CategoryTheory.Cat

The category of small categories has all small limits.

instance CategoryTheory.Cat.instPreservesLimitsCatCategoryTypeTypesObjects : CategoryTheory.Limits.PreservesLimits CategoryTheory.Cat.objects