Limits in the category of types.

We show that the category of types has all limits, by providing the usual concrete models.

def CategoryTheory.Limits.Types.coneOfSection {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {s : (j : J) → F.obj j} (hs : s ∈ F.sections) : Cone F

Given a section of a functor F into Type*, construct a cone over F with PUnit as the cone point.

Equations

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

def CategoryTheory.Limits.Types.sectionOfCone {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cone F) (x : c.pt) : ↑F.sections

Given a cone over a functor F into Type* and an element in the cone point, construct a section of F.

Equations

• CategoryTheory.Limits.Types.sectionOfCone c x = ⟨fun (j : J) => (CategoryTheory.ConcreteCategory.hom (c.π.app j)) x, ⋯⟩

theorem CategoryTheory.Limits.Types.isLimit_iff {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cone F) : Nonempty (IsLimit c) ↔ ∀ s ∈ F.sections, ∃! x : c.pt, ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) x = s j

theorem CategoryTheory.Limits.Types.isLimit_iff_bijective_sectionOfCone {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cone F) : Nonempty (IsLimit c) ↔ Function.Bijective (sectionOfCone c)

noncomputable def CategoryTheory.Limits.Types.isLimitEquivSections {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {c : Cone F} (t : IsLimit c) : c.pt ≃ ↑F.sections

The equivalence between a limiting cone of F in Type u and the "concrete" definition as the sections of F.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.isLimitEquivSections_apply {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {c : Cone F} (t : IsLimit c) (j : J) (x : c.pt) : ↑((isLimitEquivSections t) x) j = (ConcreteCategory.hom (c.π.app j)) x

@[simp]

theorem CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {c : Cone F} (t : IsLimit c) (x : ↑F.sections) (j : J) : (ConcreteCategory.hom (c.π.app j)) ((isLimitEquivSections t).symm x) = ↑x j

We now provide two distinct implementations in the category of types.

The first, in the CategoryTheory.Limits.Types.Small namespace, assumes Small.{u} J and constructs J-indexed limits in Type u.

The second, in the CategoryTheory.Limits.Types.TypeMax namespace constructs limits for functors F : J ⥤ Type (max v u), for J : Type v. This construction is slightly nicer, as the limit is definitionally just F.sections, rather than Shrink F.sections, which makes an arbitrary choice of u-small representative.

Hopefully we might be able to entirely remove the TypeMax constructions, but for now they are useful glue for the later parts of the library.

noncomputable def CategoryTheory.Limits.Types.Small.limitCone {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} ↑F.sections] : Cone F

(internal implementation) the limit cone of a functor, implemented as flat sections of a pi type

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.Small.limitCone_π_app {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} ↑F.sections] (j : J) : (limitCone F).π.app j = TypeCat.ofHom fun (u : ((Functor.const J).obj (Shrink.{u, max u v} ↑F.sections)).obj j) => ↑((equivShrink ↑F.sections).symm u) j

@[simp]

theorem CategoryTheory.Limits.Types.Small.limitCone_pt {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} ↑F.sections] : (limitCone F).pt = Shrink.{u, max u v} ↑F.sections

theorem CategoryTheory.Limits.Types.Small.limitCone_pt_ext {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} ↑F.sections] {x y : (limitCone F).pt} (w : (equivShrink ↑F.sections).symm x = (equivShrink ↑F.sections).symm y) : x = y

theorem CategoryTheory.Limits.Types.Small.limitCone_pt_ext_iff {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [Small.{u, max u v} ↑F.sections] {x y : (limitCone F).pt} : x = y ↔ (equivShrink ↑F.sections).symm x = (equivShrink ↑F.sections).symm y

noncomputable def CategoryTheory.Limits.Types.Small.limitConeIsLimit {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} ↑F.sections] : IsLimit (limitCone F)

(internal implementation) the fact that the proposed limit cone is the limit

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} ↑F.sections] (s : Cone F) : (limitConeIsLimit F).lift s = TypeCat.ofHom fun (v : s.pt) => (equivShrink ↑F.sections) ⟨fun (j : J) => (ConcreteCategory.hom (s.π.app j)) v, ⋯⟩

theorem CategoryTheory.Limits.Types.hasLimit_iff_small_sections {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) : HasLimit F ↔ Small.{u, max u v} ↑F.sections

noncomputable def CategoryTheory.Limits.Types.limitCone {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) : Cone F

(internal implementation) the limit cone of a functor, implemented as flat sections of a pi type

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.limitCone_pt {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) : (limitCone F).pt = ↑F.sections

@[simp]

theorem CategoryTheory.Limits.Types.limitCone_π_app {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) (j : J) : (limitCone F).π.app j = TypeCat.ofHom fun (u : ((Functor.const J).obj ↑F.sections).obj j) => ↑u j

noncomputable def CategoryTheory.Limits.Types.limitConeIsLimit {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) : IsLimit (limitCone F)

(internal implementation) the fact that the proposed limit cone is the limit

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.limitConeIsLimit_lift {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) (s : Cone F) : (limitConeIsLimit F).lift s = TypeCat.ofHom fun (v : s.pt) => ⟨fun (j : J) => (ConcreteCategory.hom (s.π.app j)) v, ⋯⟩

The results in this section have a UnivLE.{v, u} hypothesis, but as they only use the constructions from the CategoryTheory.Limits.Types.UnivLE namespace in their definitions (rather than their statements), we leave them in the main CategoryTheory.Limits.Types namespace.

instance CategoryTheory.Limits.Types.hasLimit {J : Type v} [Category.{w, v} J] [Small.{u, v} J] (F : Functor J (Type u)) : HasLimit F

instance CategoryTheory.Limits.Types.hasLimitsOfShape {J : Type v} [Category.{w, v} J] [Small.{u, v} J] : HasLimitsOfShape J (Type u)

@[instance 1300]

instance CategoryTheory.Limits.Types.hasLimitsOfSize [UnivLE.{v, u}] : HasLimitsOfSize.{w, v, u, u + 1} (Type u)

The category of types has all limits.

More specifically, when UnivLE.{v, u}, the category Type u has all v-small limits.

noncomputable def CategoryTheory.Limits.Types.limitEquivSections {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] : limit F ≃ ↑F.sections

The equivalence between the abstract limit of F in Type max v u and the "concrete" definition as the sections of F.

Equations

• CategoryTheory.Limits.Types.limitEquivSections F = CategoryTheory.Limits.Types.isLimitEquivSections (CategoryTheory.Limits.limit.isLimit F)

@[simp]

theorem CategoryTheory.Limits.Types.limitEquivSections_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (x : limit F) (j : J) : ↑((limitEquivSections F) x) j = (ConcreteCategory.hom (limit.π F j)) x

@[simp]

theorem CategoryTheory.Limits.Types.limitEquivSections_symm_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (x : ↑F.sections) (j : J) : (ConcreteCategory.hom (limit.π F j)) ((limitEquivSections F).symm x) = ↑x j

noncomputable def CategoryTheory.Limits.Types.limNatIsoSectionsFunctor {J : Type v} [Category.{w, v} J] : lim ≅ Functor.sectionsFunctor J

The limit of a functor F : J ⥤ Type _ is naturally isomorphic to F.sections.

Equations

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

noncomputable def CategoryTheory.Limits.Types.Limit.mk {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j ⟶ j'), (ConcreteCategory.hom (F.map f)) (x j) = x j') : limit F

Construct a term of limit F : Type u from a family of terms x : Π j, F.obj j which are "coherent": ∀ (j j') (f : j ⟶ j'), F.map f (x j) = x j'.

Equations

• CategoryTheory.Limits.Types.Limit.mk F x h = (CategoryTheory.Limits.Types.limitEquivSections F).symm ⟨x, ⋯⟩

@[simp]

theorem CategoryTheory.Limits.Types.Limit.π_mk {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j ⟶ j'), (ConcreteCategory.hom (F.map f)) (x j) = x j') (j : J) : (ConcreteCategory.hom (limit.π F j)) (mk F x h) = x j

theorem CategoryTheory.Limits.Types.limit_ext {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (x y : limit F) (w : ∀ (j : J), (ConcreteCategory.hom (limit.π F j)) x = (ConcreteCategory.hom (limit.π F j)) y) : x = y

theorem CategoryTheory.Limits.Types.limit_ext_iff {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasLimit F] {x y : limit F} : x = y ↔ ∀ (j : J), (ConcreteCategory.hom (limit.π F j)) x = (ConcreteCategory.hom (limit.π F j)) y

theorem CategoryTheory.Limits.Types.limit_ext' {J : Type v} [Category.{w, v} J] (F' : Functor J (Type v)) (x y : limit F') (w : ∀ (j : J), (ConcreteCategory.hom (limit.π F' j)) x = (ConcreteCategory.hom (limit.π F' j)) y) : x = y

theorem CategoryTheory.Limits.Types.limit_ext'_iff {J : Type v} [Category.{w, v} J] {F' : Functor J (Type v)} {x y : limit F'} : x = y ↔ ∀ (j : J), (ConcreteCategory.hom (limit.π F' j)) x = (ConcreteCategory.hom (limit.π F' j)) y

theorem CategoryTheory.Limits.Types.limit_ext_iff' {J : Type v} [Category.{w, v} J] (F' : Functor J (Type v)) (x y : limit F') : x = y ↔ ∀ (j : J), (ConcreteCategory.hom (limit.π F' j)) x = (ConcreteCategory.hom (limit.π F' j)) y

@[simp]

theorem CategoryTheory.Limits.limit.lift_π_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasLimit F] (c : Cone F) (j : J) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F✝] (x : carrier c.pt) : (ConcreteCategory.hom (π F j)) ((ConcreteCategory.hom (lift F c)) x) = (ConcreteCategory.hom (c.π.app j)) x

@[simp]

theorem CategoryTheory.Limits.limMap_π_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} [HasLimit F] [HasLimit G] (α : F ⟶ G) (j : J) {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F✝] (x : carrier (limit F)) : (ConcreteCategory.hom (limit.π G j)) ((ConcreteCategory.hom (limMap α)) x) = (ConcreteCategory.hom (α.app j)) ((ConcreteCategory.hom (limit.π F j)) x)

@[simp]

theorem CategoryTheory.Limits.limit.w_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasLimit F] {j j' : J} (f : j ⟶ j') {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : ConcreteCategory C F✝] (x : carrier (limit F)) : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (π F j)) x) = (ConcreteCategory.hom (π F j')) x

@[deprecated CategoryTheory.Limits.limit.w_apply (since := "2026-02-17")]

theorem CategoryTheory.Limits.Types.Limit.w_apply {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasLimit F] {j j' : J} {x : limit F} (f : j ⟶ j') : (ConcreteCategory.hom (F.map f)) ((ConcreteCategory.hom (limit.π F j)) x) = (ConcreteCategory.hom (limit.π F j')) x

@[deprecated CategoryTheory.Limits.limit.lift_π_apply (since := "2026-02-17")]

theorem CategoryTheory.Limits.Types.Limit.lift_π_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (s : Cone F) (j : J) (x : s.pt) : (ConcreteCategory.hom (limit.π F j)) ((ConcreteCategory.hom (limit.lift F s)) x) = (ConcreteCategory.hom (s.π.app j)) x

@[deprecated CategoryTheory.Limits.limMap_π_apply (since := "2026-02-17")]

theorem CategoryTheory.Limits.Types.Limit.map_π_apply {J : Type v} [Category.{w, v} J] {F G : Functor J (Type u)} [HasLimit F] [HasLimit G] (α : F ⟶ G) (j : J) (x : limit F) : (ConcreteCategory.hom (limit.π G j)) ((ConcreteCategory.hom (limMap α)) x) = (ConcreteCategory.hom (α.app j)) ((ConcreteCategory.hom (limit.π F j)) x)

@[deprecated CategoryTheory.Limits.limit.w_apply (since := "2026-02-17")]

theorem CategoryTheory.Limits.Types.Limit.w_apply' {J : Type v} [Category.{w, v} J] {F' : Functor J (Type v)} {j j' : J} {x : limit F'} (f : j ⟶ j') : (ConcreteCategory.hom (F'.map f)) ((ConcreteCategory.hom (limit.π F' j)) x) = (ConcreteCategory.hom (limit.π F' j')) x

@[deprecated CategoryTheory.Limits.limit.lift_π_apply (since := "2026-02-17")]

theorem CategoryTheory.Limits.Types.Limit.lift_π_apply' {J : Type v} [Category.{w, v} J] (F' : Functor J (Type v)) (s : Cone F') (j : J) (x : s.pt) : (ConcreteCategory.hom (limit.π F' j)) ((ConcreteCategory.hom (limit.lift F' s)) x) = (ConcreteCategory.hom (s.π.app j)) x

@[deprecated CategoryTheory.Limits.limMap_π_apply (since := "2026-02-17")]

theorem CategoryTheory.Limits.Types.Limit.map_π_apply' {J : Type v} [Category.{w, v} J] {F' G' : Functor J (Type v)} (α : F' ⟶ G') (j : J) (x : limit F') : (ConcreteCategory.hom (limit.π G' j)) ((ConcreteCategory.hom (limMap α)) x) = (ConcreteCategory.hom (α.app j)) ((ConcreteCategory.hom (limit.π F' j)) x)

In this section we verify that instances are available as expected.