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_ι_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_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_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

@[deprecated CategoryTheory.Limits.Types.hasColimit_iff_small_colimitType (since := "2025-06-22")]

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

Alias of CategoryTheory.Limits.Types.hasColimit_iff_small_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

@[deprecated CategoryTheory.Limits.Types.small_colimitType_of_hasColimit (since := "2025-06-22")]

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

Alias of CategoryTheory.Limits.Types.small_colimitType_of_hasColimit.

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.

@[deprecated CategoryTheory.Functor.ColimitTypeRel (since := "2025-06-22")]

def CategoryTheory.Limits.Types.Quot.Rel {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) : (j : J) × F.obj j → (j : J) × F.obj j → Prop

Alias of CategoryTheory.Functor.ColimitTypeRel.

---

Given F : J ⥤ Type w₀, this is the relation Σ j, F.obj j which generates an equivalence relation such that the quotient identifies to the colimit type of F.

Equations

• @CategoryTheory.Limits.Types.Quot.Rel = @CategoryTheory.Functor.ColimitTypeRel

@[deprecated CategoryTheory.Functor.ColimitType (since := "2025-06-22")]

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

Alias of CategoryTheory.Functor.ColimitType.

---

The colimit type of a functor F : J ⥤ Type w₀. (It may not be in Type w₀.)

Equations

• @CategoryTheory.Limits.Types.Quot = @CategoryTheory.Functor.ColimitType

@[deprecated CategoryTheory.Functor.ιColimitType (since := "2025-06-22")]

def CategoryTheory.Limits.Types.Quot.ι {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) (j : J) (x : F.obj j) : F.ColimitType

Alias of CategoryTheory.Functor.ιColimitType.

---

The canonical maps F.obj j → F.ColimitType.

Equations

• @CategoryTheory.Limits.Types.Quot.ι = @CategoryTheory.Functor.ιColimitType

@[deprecated CategoryTheory.Functor.ιColimitType_jointly_surjective (since := "2025-06-22")]

theorem CategoryTheory.Limits.Types.Quot.jointly_surjective {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) (t : F.ColimitType) : ∃ (j : J) (x : F.obj j), F.ιColimitType j x = t

Alias of CategoryTheory.Functor.ιColimitType_jointly_surjective.

@[deprecated CategoryTheory.Functor.descColimitType (since := "2025-06-22")]

def CategoryTheory.Limits.Types.Quot.desc {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) (c : F.CoconeTypes) : F.ColimitType → c.pt

Alias of CategoryTheory.Functor.descColimitType.

---

An heterogeneous universe version of the universal property of the colimit is satisfied by F.ColimitType together the maps F.ιColimitType j.

Equations

• @CategoryTheory.Limits.Types.Quot.desc = @CategoryTheory.Functor.descColimitType

@[deprecated CategoryTheory.Functor.descColimitType_comp_ι (since := "2025-06-22")]

theorem CategoryTheory.Limits.Types.Quot.ι_desc {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) (c : F.CoconeTypes) (j : J) : F.descColimitType c ∘ F.ιColimitType j = c.ι j

Alias of CategoryTheory.Functor.descColimitType_comp_ι.

@[deprecated CategoryTheory.Functor.ιColimitType_map (since := "2025-06-22")]

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

Alias of CategoryTheory.Functor.ιColimitType_map.

@[deprecated CategoryTheory.Limits.Types.isColimit_iff_coconeTypesIsColimit (since := "2025-06-22")]

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

Alias of CategoryTheory.Limits.Types.isColimit_iff_coconeTypesIsColimit.

@[deprecated CategoryTheory.Limits.Types.colimitEquivColimitType (since := "2025-06-22")]

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

Alias of CategoryTheory.Limits.Types.colimitEquivColimitType.

---

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

Equations

• @CategoryTheory.Limits.Types.colimitEquivQuot = @CategoryTheory.Limits.Types.colimitEquivColimitType

@[deprecated CategoryTheory.Limits.Types.colimitEquivColimitType_symm_apply (since := "2025-06-22")]

theorem CategoryTheory.Limits.Types.colimitEquivQuot_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

Alias of CategoryTheory.Limits.Types.colimitEquivColimitType_symm_apply.

@[deprecated CategoryTheory.Limits.Types.colimitEquivColimitType_apply (since := "2025-06-22")]

theorem CategoryTheory.Limits.Types.colimitEquivQuot_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⟩

Alias of CategoryTheory.Limits.Types.colimitEquivColimitType_apply.