Colimits in the category of types

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

instance CategoryTheory.Functor.instSmallColimitType {J : Type v} [Category.{w, v} J] [Small.{u, v} J] (F : Functor J (Type u)) : Small.{u, max u v} F.ColimitType

def CategoryTheory.Functor.coconeTypesEquiv {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) : F.CoconeTypes ≃ Limits.Cocone F

If F : J ⥤ Type u, then the data of a "type-theoretic" cocone of F with a point in Type u is the same as the data of a cocone (in a categorical sense).

Equations

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

@[simp]

theorem CategoryTheory.Functor.coconeTypesEquiv_symm_apply_pt {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (c : Limits.Cocone F) : (F.coconeTypesEquiv.symm c).pt = c.pt

@[simp]

theorem CategoryTheory.Functor.coconeTypesEquiv_apply_pt {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (c : F.CoconeTypes) : (F.coconeTypesEquiv c).pt = c.pt

@[simp]

theorem CategoryTheory.Functor.coconeTypesEquiv_apply_ι_app {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (c : F.CoconeTypes) (j : J) (a✝ : F.obj j) : (F.coconeTypesEquiv c).ι.app j a✝ = c.ι j a✝

@[simp]

theorem CategoryTheory.Functor.coconeTypesEquiv_symm_apply_ι {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (c : Limits.Cocone F) (j : J) (a✝ : F.obj j) : (F.coconeTypesEquiv.symm c).ι j a✝ = c.ι.app j a✝

theorem CategoryTheory.Functor.CoconeTypes.isColimit_iff {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : F.CoconeTypes) : c.IsColimit ↔ Nonempty (Limits.IsColimit (F.coconeTypesEquiv c))

theorem CategoryTheory.Limits.Types.isColimit_iff_coconeTypesIsColimit {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cocone F) : Nonempty (IsColimit c) ↔ (F.coconeTypesEquiv.symm c).IsColimit

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.Types.colimitCocone {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} F.ColimitType] : Cocone F

(internal implementation) the colimit cocone of a functor, implemented as a quotient of a sigma type

Equations

• CategoryTheory.Limits.Types.colimitCocone F = F.coconeTypesEquiv (F.coconeTypes.postcomp ⇑(equivShrink F.ColimitType))

noncomputable def CategoryTheory.Limits.Types.colimitCoconeIsColimit {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} F.ColimitType] : IsColimit (colimitCocone F)

(internal implementation) the fact that the proposed colimit cocone is the colimit

Equations

• CategoryTheory.Limits.Types.colimitCoconeIsColimit F = ⋯.some

theorem CategoryTheory.Limits.Types.hasColimit_iff_small_colimitType {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) : HasColimit F ↔ Small.{u, max u v} F.ColimitType

theorem CategoryTheory.Limits.Types.small_colimitType_of_hasColimit {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] : Small.{u, max u v} F.ColimitType

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

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

@[instance 1300]

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

The category of types has all colimits.

@[reducible, inline]

abbrev CategoryTheory.Limits.Types.TypeMax.colimitCocone {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) : Cocone F

(internal implementation) the colimit cocone of a functor, implemented as a quotient of a sigma type

Equations

• CategoryTheory.Limits.Types.TypeMax.colimitCocone F = F.coconeTypesEquiv F.coconeTypes

noncomputable def CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) : IsColimit (colimitCocone F)

(internal implementation) the fact that the proposed colimit cocone is the colimit

Equations

• CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit F = ⋯.some

noncomputable def CategoryTheory.Limits.Types.colimitEquivColimitType {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] : colimit F ≃ F.ColimitType

The equivalence between the abstract colimit of F in Type u and the "concrete" definition as a quotient.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.colimitEquivColimitType_symm_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] (j : J) (x : F.obj j) : (colimitEquivColimitType F).symm (Quot.mk F.ColimitTypeRel ⟨j, x⟩) = colimit.ι F j x

@[simp]

theorem CategoryTheory.Limits.Types.colimitEquivColimitType_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] (j : J) (x : F.obj j) : (colimitEquivColimitType F) (colimit.ι F j x) = Quot.mk F.ColimitTypeRel ⟨j, x⟩

@[simp]

theorem CategoryTheory.Limits.Types.Colimit.w_apply {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {j j' : J} {x : F.obj j} (f : j ⟶ j') : colimit.ι F j' (F.map f x) = colimit.ι F j x

@[simp]

theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] (s : Cocone F) (j : J) (x : F.obj j) : colimit.desc F s (colimit.ι F j x) = s.ι.app j x

@[simp]

theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply {J : Type v} [Category.{w, v} J] {F G : Functor J (Type u)} [HasColimitsOfShape J (Type u)] (α : F ⟶ G) (j : J) (x : F.obj j) : colim.map α (colimit.ι F j x) = colimit.ι G j (α.app j x)

@[deprecated CategoryTheory.Limits.Types.Colimit.w_apply (since := "2025-08-22")]

theorem CategoryTheory.Limits.Types.Colimit.w_apply' {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {j j' : J} {x : F.obj j} (f : j ⟶ j') : colimit.ι F j' (F.map f x) = colimit.ι F j x

Alias of CategoryTheory.Limits.Types.Colimit.w_apply.

@[deprecated CategoryTheory.Limits.Types.Colimit.ι_desc_apply (since := "2025-08-22")]

theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply' {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] (s : Cocone F) (j : J) (x : F.obj j) : colimit.desc F s (colimit.ι F j x) = s.ι.app j x

Alias of CategoryTheory.Limits.Types.Colimit.ι_desc_apply.

@[deprecated CategoryTheory.Limits.Types.Colimit.ι_map_apply (since := "2025-08-22")]

theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply' {J : Type v} [Category.{w, v} J] {F G : Functor J (Type u)} [HasColimitsOfShape J (Type u)] (α : F ⟶ G) (j : J) (x : F.obj j) : colim.map α (colimit.ι F j x) = colimit.ι G j (α.app j x)

Alias of CategoryTheory.Limits.Types.Colimit.ι_map_apply.

theorem CategoryTheory.Limits.Types.colimit_sound {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} (f : j ⟶ j') (w : F.map f x = x') : colimit.ι F j x = colimit.ι F j' x'

theorem CategoryTheory.Limits.Types.colimit_sound' {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} {j'' : J} (f : j ⟶ j'') (f' : j' ⟶ j'') (w : F.map f x = F.map f' x') : colimit.ι F j x = colimit.ι F j' x'

theorem CategoryTheory.Limits.Types.colimit_eq {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} (w : colimit.ι F j x = colimit.ι F j' x') : Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', x'⟩

theorem CategoryTheory.Limits.Types.jointly_surjective_of_isColimit {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {t : Cocone F} (h : IsColimit t) (x : t.pt) : ∃ (j : J) (y : F.obj j), t.ι.app j y = x

theorem CategoryTheory.Limits.Types.jointly_surjective {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) {t : Cocone F} (h : IsColimit t) (x : t.pt) : ∃ (j : J) (y : F.obj j), t.ι.app j y = x

theorem CategoryTheory.Limits.Types.jointly_surjective' {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] (x : colimit F) : ∃ (j : J) (y : F.obj j), colimit.ι F j y = x

A variant of jointly_surjective for x : colimit F.

theorem CategoryTheory.Limits.Types.nonempty_of_nonempty_colimit {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] : Nonempty (colimit F) → Nonempty J

If a colimit is nonempty, also its index category is nonempty.