module Cat.Diagram.Coproduct.Indexed {o β} (C : Precategory o β) where
Indexed coproductsπ
Indexed coproducts are the dual notion to indexed products, so see there for motivation and exposition.
record is-indexed-coproduct (F : Idx β C.Ob) (ΞΉ : β i β C.Hom (F i) S) : Type (o β β β level-of Idx) where no-eta-equality field match : β {Y} β (β i β C.Hom (F i) Y) β C.Hom S Y commute : β {i} {Y} {f : β i β C.Hom (F i) Y} β match f C.β ΞΉ i β‘ f i unique : β {Y} {h : C.Hom S Y} (f : β i β C.Hom (F i) Y) β (β i β h C.β ΞΉ i β‘ f i) β h β‘ match f eta : β {Y} (h : C.Hom S Y) β h β‘ match (Ξ» i β h C.β ΞΉ i) eta h = unique _ Ξ» _ β refl uniqueβ : β {Y} {g h : C.Hom S Y} β (β i β g C.β ΞΉ i β‘ h C.β ΞΉ i) β g β‘ h uniqueβ {g = g} {h} eq = eta g β ap match (funext eq) β sym (eta h) hom-iso : β {Y} β C.Hom S Y β (β i β C.Hom (F i) Y) hom-iso = (Ξ» z i β z C.β ΞΉ i) , is-isoβis-equiv Ξ» where .is-iso.inv β match .is-iso.rinv x β funext Ξ» i β commute .is-iso.linv x β sym (unique _ Ξ» _ β refl)
A category admits indexed coproducts (of level ) if, for any type and family , there is an indexed coproduct of .
record Indexed-coproduct (F : Idx β C.Ob) : Type (o β β β level-of Idx) where no-eta-equality field {Ξ£F} : C.Ob ΞΉ : β i β C.Hom (F i) Ξ£F has-is-ic : is-indexed-coproduct F ΞΉ open is-indexed-coproduct has-is-ic public has-coproducts-indexed-by : β {β} (I : Type β) β Type _ has-coproducts-indexed-by I = β (F : I β C.Ob) β Indexed-coproduct F has-indexed-coproducts : β β β Type _ has-indexed-coproducts β = β {I : Type β} β has-coproducts-indexed-by I
Indexed-coproduct-β : β {β β'} {I : Type β} {J : Type β'} β (e : I β J) β {F : I β C.Ob} β Indexed-coproduct (F β Equiv.from e) β Indexed-coproduct F Indexed-coproduct-β e {F} p = Ξ» where .Ξ£F β p .Ξ£F .ΞΉ j β p .ΞΉ (e.to j) C.β C.from (pathβiso (ap F (e.Ξ· _))) .has-is-ic .match f β p .match (f β e.from) .has-is-ic .commute {f = f} β C.pulll (p .commute) β from-pathp-to (C ^op) _ (ap f (e.Ξ· _)) .has-is-ic .unique f comm β p .unique _ Ξ» j β ap (_ C.β_) (sym (from-pathp-to (C ^op) _ (ap (p .ΞΉ) (e.Ξ΅ j))) β ap (Ξ» z β p .ΞΉ _ C.β C.from (pathβiso (ap F z))) (e.zag j)) β comm (e.from j) where open Indexed-coproduct open is-indexed-coproduct module e = Equiv e Lift-Indexed-coproduct : β {β} β' β {I : Type β} β {F : I β C.Ob} β Indexed-coproduct {Idx = Lift β' I} (F β Lift.lower) β Indexed-coproduct F Lift-Indexed-coproduct _ = Indexed-coproduct-β (Lift-β eβ»ΒΉ)
Disjoint coproductsπ
An indexed coproduct is said to be disjoint if every one of its inclusions is monic, and, for unequal , the square below is a pullback with initial apex. Since the maps are monic, the pullback below computes the intersection of and as subobjects of , hence the name disjoint coproduct: If is an initial object, then .
record is-disjoint-coproduct (F : Idx β C.Ob) (ΞΉ : β i β C.Hom (F i) S) : Type (o β β β level-of Idx) where field is-coproduct : is-indexed-coproduct F ΞΉ injections-are-monic : β i β C.is-monic (ΞΉ i) summands-intersect : β i j β Pullback C (ΞΉ i) (ΞΉ j) different-images-are-disjoint : β i j β Β¬ i β‘ j β is-initial C (summands-intersect i j .Pullback.apex)
Initial objects are disjointπ
We prove that if is an initial object, then it is also an indexed coproduct β for any family β and furthermore, it is a disjoint coproduct.
is-initialβis-disjoint-coproduct : β {β } {F : β₯ β C.Ob} {i : β i β C.Hom (F i) β } β is-initial C β β is-disjoint-coproduct F i is-initialβis-disjoint-coproduct {F = F} {i = i} init = is-disjoint where open is-indexed-coproduct is-coprod : is-indexed-coproduct F i is-coprod .match _ = init _ .centre is-coprod .commute {i = i} = absurd i is-coprod .unique {h = h} f p i = init _ .paths h (~ i) open is-disjoint-coproduct is-disjoint : is-disjoint-coproduct F i is-disjoint .is-coproduct = is-coprod is-disjoint .injections-are-monic i = absurd i is-disjoint .summands-intersect i j = absurd i is-disjoint .different-images-are-disjoint i j p = absurd i