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

    : βˆ€ {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
      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))
      mc .universal eta p = ic.match eta
      mc .factors eta p = ic.commute
      mc .unique eta p other q = ic.unique eta q

    : βˆ€ {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

    : 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 {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)