module Cat.Diagram.Colimit.Coproduct {o h} (C : Precategory o h) where
Coproducts are colimitsπ
Indexed coproducts as colimitsπ
Similarly to the product case, when is a groupoid, indexed coproducts correspond to colimits of discrete diagrams of shape
module _ {I : Type β'} (i-is-grpd : is-groupoid I) (F : I β Ob) where open _=>_ InjβCocone : β {x} β (β i β Hom (F i) x) β Disc-adjunct {C = C} {iss = i-is-grpd} F => Const x InjβCocone inj .Ξ· i = inj i InjβCocone inj .is-natural i j p = J (Ξ» j p β inj j β subst (Hom (F i) β F) p id β‘ id β inj i) (elimr (transport-refl id) β sym (idl _)) p is-indexed-coproductβis-colimit : β {x} {inj : β i β Hom (F i) x} β is-indexed-coproduct C F inj β is-colimit (Disc-adjunct F) x (InjβCocone inj) is-indexed-coproductβis-colimit {x = x} {inj} ic = to-is-colimitp mc refl where module ic = is-indexed-coproduct ic open make-is-colimit mc : make-is-colimit (Disc-adjunct F) x mc .Ο i = inj i mc .commutes {i} {j} p = J (Ξ» j p β inj j β subst (Hom (F i) β F) p id β‘ inj i) (elimr (transport-refl id)) p mc .universal eta p = ic.match eta mc .factors eta p = ic.commute mc .unique eta p other q = ic.unique eta q is-colimitβis-indexed-coprduct : β {K : Functor β€Cat C} β {eps : Disc-adjunct {iss = i-is-grpd} F => K Fβ !F} β is-lan !F (Disc-adjunct F) K eps β is-indexed-coproduct C F (eps .Ξ·) is-colimitβis-indexed-coprduct {K = K} {eps} colim = ic where module colim = is-colimit colim open is-indexed-coproduct ic : is-indexed-coproduct C F (eps .Ξ·) ic .match k = colim.universal k (J (Ξ» j p β k j β subst (Hom (F _) β F) p id β‘ k _) (elimr (transport-refl _))) ic .commute = colim.factors _ _ ic .unique k comm = colim.unique _ _ _ comm ICβColimit : Indexed-coproduct C F β Colimit {C = C} (Disc-adjunct {iss = i-is-grpd} F) ICβColimit ic = to-colimit (is-indexed-coproductβis-colimit has-is-ic) where open Indexed-coproduct ic ColimitβIC : Colimit {C = C} (Disc-adjunct {iss = i-is-grpd} F) β Indexed-coproduct C F ColimitβIC colim .Indexed-coproduct.Ξ£F = _ ColimitβIC colim .Indexed-coproduct.ΞΉ = _ ColimitβIC colim .Indexed-coproduct.has-is-ic = is-colimitβis-indexed-coprduct (Colimit.has-colimit colim)