Coproducts in Type

If F : J → Type max v u (with J : Type v), we show that the coproduct of F exists in Type max v u and identifies to the sigma type Σ j, F j. Similarly, the binary coproduct of two types X and Y identifies to X ⊕ Y, and the initial object of Type u if PEmpty.

@[reducible, inline]

abbrev CategoryTheory.Limits.CofanTypes {C : Type u} (F : C → Type v) : Type (max (max u v) (w + 1))

Given a functor F : Discrete C ⥤ Type v, this is a "cofan" for F, but we allow the point to be in Type w for an arbitrary universe w.

Equations

• CategoryTheory.Limits.CofanTypes F = (CategoryTheory.Discrete.functor F).CoconeTypes

@[reducible, inline]

abbrev CategoryTheory.Limits.CofanTypes.inj {C : Type u} {F : C → Type v} (c : CofanTypes F) (i : C) : F i → c.pt

The injection map for a cofan of a functor to types.

Equations

• c.inj i = c.ι { as := i }

def CategoryTheory.Limits.CofanTypes.sigma {C : Type u} (F : C → Type v) : CofanTypes F

The cofan given by a sigma type.

Equations

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

@[simp]

theorem CategoryTheory.Limits.CofanTypes.sigma_ι_snd {C : Type u} (F : C → Type v) (x✝ : Discrete C) (x : (Discrete.functor F).obj x✝) : ((sigma F).ι x✝ x).snd = x

@[simp]

theorem CategoryTheory.Limits.CofanTypes.sigma_ι_fst {C : Type u} (F : C → Type v) (x✝ : Discrete C) (x : (Discrete.functor F).obj x✝) : ((sigma F).ι x✝ x).fst = x✝.as

@[simp]

theorem CategoryTheory.Limits.CofanTypes.sigma_pt {C : Type u} (F : C → Type v) : (sigma F).pt = ((i : C) × F i)

@[simp]

theorem CategoryTheory.Limits.CofanTypes.sigma_inj {C : Type u} {F : C → Type v} (i : C) (x : F i) : (sigma F).inj i x = ⟨i, x⟩

theorem CategoryTheory.Limits.CofanTypes.isColimit_mk {C : Type u} {F : C → Type v} (c : CofanTypes F) (h₁ : ∀ (x : c.pt), ∃ (i : C) (y : F i), c.inj i y = x) (h₂ : ∀ (i : C), Function.Injective (c.inj i)) (h₃ : ∀ (i j : C) (x : F i) (y : F j), c.inj i x = c.inj j y → i = j) : Functor.CoconeTypes.IsColimit c

theorem CategoryTheory.Limits.CofanTypes.isColimit_sigma {C : Type u} (F : C → Type v) : Functor.CoconeTypes.IsColimit (sigma F)

def CategoryTheory.Limits.CofanTypes.fromSigma {C : Type u} (F : C → Type v) (c : CofanTypes F) (x : (i : C) × F i) : c.pt

Given a cofan of a functor to types, this is a canonical map from the Sigma type to the point of the cofan.

Equations

• CategoryTheory.Limits.CofanTypes.fromSigma F c x = c.inj x.fst x.snd

theorem CategoryTheory.Limits.CofanTypes.isColimit_iff_bijective_fromSigma {C : Type u} {F : C → Type v} (c : CofanTypes F) : Functor.CoconeTypes.IsColimit c ↔ Function.Bijective (fromSigma F c)

theorem CategoryTheory.Limits.CofanTypes.bijective_fromSigma_of_isColimit {C : Type u} {F : C → Type v} {c : CofanTypes F} (hc : Functor.CoconeTypes.IsColimit c) : Function.Bijective (fromSigma F c)

noncomputable def CategoryTheory.Limits.CofanTypes.equivOfIsColimit {C : Type u} {F : C → Type v} {c : CofanTypes F} (hc : Functor.CoconeTypes.IsColimit c) : (i : C) × F i ≃ c.pt

The bijection from the sigma type to the point of a colimit cofan of a functor to types.

Equations

• CategoryTheory.Limits.CofanTypes.equivOfIsColimit hc = Equiv.ofBijective (CategoryTheory.Limits.CofanTypes.fromSigma F c) ⋯

@[simp]

theorem CategoryTheory.Limits.CofanTypes.equivOfIsColimit_apply {C : Type u} {F : C → Type v} {c : CofanTypes F} (hc : Functor.CoconeTypes.IsColimit c) (i : C) (x : F i) : (equivOfIsColimit hc) ⟨i, x⟩ = c.inj i x

@[simp]

theorem CategoryTheory.Limits.CofanTypes.equivOfIsColimit_symm_apply {C : Type u} {F : C → Type v} {c : CofanTypes F} (hc : Functor.CoconeTypes.IsColimit c) (i : C) (x : F i) : (equivOfIsColimit hc).symm (c.inj i x) = ⟨i, x⟩

theorem CategoryTheory.Limits.CofanTypes.inj_jointly_surjective_of_isColimit {C : Type u} {F : C → Type v} {c : CofanTypes F} (hc : Functor.CoconeTypes.IsColimit c) (x : c.pt) : ∃ (i : C) (y : F i), c.inj i y = x

theorem CategoryTheory.Limits.CofanTypes.inj_injective_of_isColimit {C : Type u} {F : C → Type v} {c : CofanTypes F} (hc : Functor.CoconeTypes.IsColimit c) (i : C) : Function.Injective (c.inj i)

theorem CategoryTheory.Limits.CofanTypes.eq_of_inj_apply_eq_of_isColimit {C : Type u} {F : C → Type v} {c : CofanTypes F} (hc : Functor.CoconeTypes.IsColimit c) {i₁ i₂ : C} (y₁ : F i₁) (y₂ : F i₂) (h : c.inj i₁ y₁ = c.inj i₂ y₂) : i₁ = i₂

def CategoryTheory.Limits.Cofan.cofanTypes {C : Type u} {F : C → Type v} (c : Cofan F) : CofanTypes F

If F : C → Type v, then the data of a "type-theoretic" cofan of F with a point in Type v 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.Limits.Cofan.cofanTypes_ι {C : Type u} {F : C → Type v} (c : Cofan F) (x✝ : Discrete C) (a✝ : (Discrete.functor F).obj x✝) : c.cofanTypes.ι x✝ a✝ = (match (motive := (x : Discrete C) → (Discrete.functor F).obj x → c.pt) x✝ with | { as := j } => c.inj j) a✝

@[simp]

theorem CategoryTheory.Limits.Cofan.cofanTypes_pt {C : Type u} {F : C → Type v} (c : Cofan F) : c.cofanTypes.pt = c.pt

theorem CategoryTheory.Limits.Cofan.isColimit_cofanTypes_iff {C : Type u} {F : C → Type v} (c : Cofan F) : Functor.CoconeTypes.IsColimit c.cofanTypes ↔ Nonempty (IsColimit c)

theorem CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_bijective_fromSigma {C : Type u} {F : C → Type v} (c : Cofan F) : Nonempty (IsColimit c) ↔ Function.Bijective (CofanTypes.fromSigma F c.cofanTypes)

theorem CategoryTheory.Limits.Cofan.inj_jointly_surjective_of_isColimit {C : Type u} {F : C → Type v} {c : Cofan F} (hc : IsColimit c) (x : c.pt) : ∃ (i : C) (y : F i), c.inj i y = x

theorem CategoryTheory.Limits.Cofan.inj_injective_of_isColimit {C : Type u} {F : C → Type v} {c : Cofan F} (hc : IsColimit c) (i : C) : Function.Injective (c.inj i)

theorem CategoryTheory.Limits.Cofan.eq_of_inj_apply_eq_of_isColimit {C : Type u} {F : C → Type v} {c : Cofan F} (hc : IsColimit c) {i₁ i₂ : C} (y₁ : F i₁) (y₂ : F i₂) (h : c.inj i₁ y₁ = c.inj i₂ y₂) : i₁ = i₂

def CategoryTheory.Limits.Types.initialColimitCocone : ColimitCocone (Functor.empty (Type u))

The category of types has PEmpty as an initial object.

Equations

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

noncomputable def CategoryTheory.Limits.Types.initialIso : ⊥_ Type u ≅ PEmpty.{u + 1}

The initial object in Type u is PEmpty.

Equations

• CategoryTheory.Limits.Types.initialIso = CategoryTheory.Limits.colimit.isoColimitCocone CategoryTheory.Limits.Types.initialColimitCocone

noncomputable def CategoryTheory.Limits.Types.isInitialPEmpty : IsInitial PEmpty.{u + 1}

The initial object in Type u is PEmpty.

Equations

• CategoryTheory.Limits.Types.isInitialPEmpty = CategoryTheory.Limits.initialIsInitial.ofIso CategoryTheory.Limits.Types.initialIso

@[deprecated CategoryTheory.Limits.Types.isInitialPEmpty (since := "2026-02-08")]

def CategoryTheory.Limits.Types.isInitialPunit : IsInitial PEmpty.{u + 1}

Alias of CategoryTheory.Limits.Types.isInitialPEmpty.

---

The initial object in Type u is PEmpty.

Equations

• CategoryTheory.Limits.Types.isInitialPunit = CategoryTheory.Limits.Types.isInitialPEmpty

theorem CategoryTheory.Limits.Types.initial_iff_empty (X : Type u) : Nonempty (IsInitial X) ↔ IsEmpty X

An object in Type u is initial if and only if it is empty.

def CategoryTheory.Limits.Types.binaryCoproductCocone (X Y : Type u) : Cocone (pair X Y)

The sum type X ⊕ Y forms a cocone for the binary coproduct of X and Y.

Equations

• CategoryTheory.Limits.Types.binaryCoproductCocone X Y = CategoryTheory.Limits.BinaryCofan.mk Sum.inl Sum.inr

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductCocone_pt (X Y : Type u) : (binaryCoproductCocone X Y).pt = (X ⊕ Y)

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductCocone_ι_app (X Y : Type u) (x✝ : Discrete WalkingPair) (a✝ : (pair X Y).obj x✝) : (binaryCoproductCocone X Y).ι.app x✝ a✝ = (match x✝.as with | WalkingPair.left => Sum.inl | WalkingPair.right => Sum.inr) a✝

def CategoryTheory.Limits.Types.binaryCoproductColimit (X Y : Type u) : IsColimit (binaryCoproductCocone X Y)

The sum type X ⊕ Y is a binary coproduct for X and Y.

Equations

• CategoryTheory.Limits.Types.binaryCoproductColimit X Y = { desc := fun (s : CategoryTheory.Limits.BinaryCofan X Y) => Sum.elim s.inl s.inr, fac := ⋯, uniq := ⋯ }

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductColimit_desc (X Y : Type u) (s : BinaryCofan X Y) (a✝ : X ⊕ Y) : (binaryCoproductColimit X Y).desc s a✝ = Sum.elim s.inl s.inr a✝

def CategoryTheory.Limits.Types.binaryCoproductColimitCocone (X Y : Type u) : ColimitCocone (pair X Y)

The category of types has X ⊕ Y, as the binary coproduct of X and Y.

Equations

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

noncomputable def CategoryTheory.Limits.Types.binaryCoproductIso (X Y : Type u) : X ⨿ Y ≅ X ⊕ Y

The categorical binary coproduct in Type u is the sum X ⊕ Y.

Equations

• CategoryTheory.Limits.Types.binaryCoproductIso X Y = CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.binaryCoproductColimitCocone X Y)

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom (X Y : Type u) : CategoryStruct.comp coprod.inl (binaryCoproductIso X Y).hom = Sum.inl

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_hom_apply (X Y : Type u) (x : X) : (binaryCoproductIso X Y).hom (coprod.inl x) = Sum.inl x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom (X Y : Type u) : CategoryStruct.comp coprod.inr (binaryCoproductIso X Y).hom = Sum.inr

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_hom_apply (X Y : Type u) (x : Y) : (binaryCoproductIso X Y).hom (coprod.inr x) = Sum.inr x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv (X Y : Type u) : CategoryStruct.comp (asHom Sum.inl) (binaryCoproductIso X Y).inv = coprod.inl

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv_apply (X Y : Type u) (x : X) : (binaryCoproductIso X Y).inv (asHom Sum.inl x) = coprod.inl x

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv (X Y : Type u) : CategoryStruct.comp (asHom Sum.inr) (binaryCoproductIso X Y).inv = coprod.inr

@[simp]

theorem CategoryTheory.Limits.Types.binaryCoproductIso_inr_comp_inv_apply (X Y : Type u) (x : Y) : (binaryCoproductIso X Y).inv (asHom Sum.inr x) = coprod.inr x

theorem CategoryTheory.Limits.Types.binaryCofan_isColimit_iff {X Y : Type u} (c : BinaryCofan X Y) : Nonempty (IsColimit c) ↔ Function.Injective c.inl ∧ Function.Injective c.inr ∧ IsCompl (Set.range c.inl) (Set.range c.inr)

noncomputable def CategoryTheory.Limits.Types.isCoprodOfMono {X Y : Type u} (f : X ⟶ Y) [Mono f] : IsColimit (BinaryCofan.mk f Subtype.val)

Any monomorphism in Type is a coproduct injection.

Equations

• CategoryTheory.Limits.Types.isCoprodOfMono f = ⋯.some

def CategoryTheory.Limits.Types.coproductColimitCocone {J : Type v} (F : J → Type (max v u)) : ColimitCocone (Discrete.functor F)

The category of types has Σ j, f j as the coproduct of a type family f : J → Type.

Equations

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

noncomputable def CategoryTheory.Limits.Types.coproductIso {J : Type v} (F : J → Type (max v u)) : ∐ F ≅ (j : J) × F j

The categorical coproduct in Type u is the type-theoretic coproduct Σ j, F j.

Equations

• CategoryTheory.Limits.Types.coproductIso F = CategoryTheory.Limits.colimit.isoColimitCocone (CategoryTheory.Limits.Types.coproductColimitCocone F)

@[simp]

theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom {J : Type v} (F : J → Type (max v u)) (j : J) : CategoryStruct.comp (Sigma.ι F j) (coproductIso F).hom = fun (x : F j) => ⟨j, x⟩

@[simp]

theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom_apply {J : Type v} (F : J → Type (max v u)) (j : J) (x : F j) : (coproductIso F).hom (Sigma.ι F j x) = ⟨j, x⟩

@[simp]

theorem CategoryTheory.Limits.Types.coproductIso_mk_comp_inv {J : Type v} (F : J → Type (max v u)) (j : J) : CategoryStruct.comp (asHom fun (x : F j) => ⟨j, x⟩) (coproductIso F).inv = Sigma.ι F j

@[simp]

theorem CategoryTheory.Limits.Types.coproductIso_mk_comp_inv_apply {J : Type v} (F : J → Type (max v u)) (j : J) (x : F j) : (coproductIso F).inv (asHom (fun (x : F j) => ⟨j, x⟩) x) = Sigma.ι F j x