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_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) : (F.coconeTypesEquiv c).ι.app j = TypeCat.ofHom (c.ι j)

@[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_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 = (ConcreteCategory.hom (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 TypeCat 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⟩) = (ConcreteCategory.hom (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) ((ConcreteCategory.hom (colimit.ι F j)) x) = Quot.mk F.ColimitTypeRel ⟨j, x⟩

@[simp]

theorem CategoryTheory.Limits.colimit.ι_desc_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimit F] (c : Cocone 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 (F.obj j)) : (ConcreteCategory.hom (desc F c)) ((ConcreteCategory.hom (ι F j)) x) = (ConcreteCategory.hom (c.ι.app j)) x

@[simp]

theorem CategoryTheory.Limits.colimit.ι_map_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} [HasColimitsOfShape J C] {G : Functor J C} (α : 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 (F.obj j)) : (ConcreteCategory.hom (colimMap α)) ((ConcreteCategory.hom (ι F j)) x) = (ConcreteCategory.hom (CategoryStruct.comp (α.app j) (ι G j))) x

@[simp]

theorem CategoryTheory.Limits.colimit.w_apply {J : Type u₁} [Category.{v₁, u₁} J] {C : Type u} [Category.{v, u} C] (F : Functor J C) [HasColimit 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 (F.obj j)) : (ConcreteCategory.hom (ι F j')) ((ConcreteCategory.hom (F.map f)) x) = (ConcreteCategory.hom (ι F j)) x

@[deprecated CategoryTheory.Limits.colimit.w_apply (since := "2026-03-06")]

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') : (ConcreteCategory.hom (colimit.ι F j')) ((ConcreteCategory.hom (F.map f)) x) = (ConcreteCategory.hom (colimit.ι F j)) x

@[deprecated CategoryTheory.Limits.colimit.ι_desc_apply (since := "2026-03-06")]

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) : (ConcreteCategory.hom (colimit.desc F s)) ((ConcreteCategory.hom (colimit.ι F j)) x) = (ConcreteCategory.hom (s.ι.app j)) x

@[deprecated CategoryTheory.Limits.colimit.ι_map_apply (since := "2026-03-06")]

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) : (ConcreteCategory.hom (colim.map α)) ((ConcreteCategory.hom (colimit.ι F j)) x) = (ConcreteCategory.hom (colimit.ι G j)) ((ConcreteCategory.hom (α.app 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'} (f : j ⟶ j') (w : (ConcreteCategory.hom (F.map f)) x = x') : (ConcreteCategory.hom (colimit.ι F j)) x = (ConcreteCategory.hom (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 : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x') : (ConcreteCategory.hom (colimit.ι F j)) x = (ConcreteCategory.hom (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 : (ConcreteCategory.hom (colimit.ι F j)) x = (ConcreteCategory.hom (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 : (fun (X : Type u) => X) (F.obj j)), (ConcreteCategory.hom (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), (ConcreteCategory.hom (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), (ConcreteCategory.hom (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.