open import Cat.Diagram.Coproduct.Indexed
open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Colimit.Base
open import Cat.Instances.Shape.Two
open import Cat.Instances.Discrete
open import Cat.Diagram.Coproduct
open import Cat.Functor.Constant
open import Cat.Functor.Kan.Base
open import Cat.Prelude

open is-coproduct
open Coproduct
open Functor
open _=>_

module Cat.Diagram.Colimit.Coproduct {o h} (C : Precategory o h) where

open import Cat.Reasoning C

private variable
o' β' : Level


# Coproducts are colimitsπ

We first establish the correspondence between binary coproducts and colimits over the functor out of which maps to and to dualising products as limits.

is-coproductβis-colimit
: β {x} {F : Functor 2-object-category C} {eta : F => Const x}
β is-coproduct C (eta .Ξ· true) (eta .Ξ· false)
β is-colimit {C = C} F x eta
is-coproductβis-colimit {x = x} {F} {eta} coprod =
to-is-colimitp mc Ξ» where
{true} β refl
{false} β refl
where
module coprod = is-coproduct coprod
open make-is-colimit

mc : make-is-colimit F x
mc .Ο j = eta .Ξ· j
mc .commutes f = eta .is-natural _ _ _ β idl _
mc .universal eta _ = coprod.[ eta true , eta false ]
mc .factors {true} eta _ = coprod.[]βΞΉβ
mc .factors {false} eta _ = coprod.[]βΞΉβ
mc .unique eta p other q = coprod.unique (q true) (q false)

is-colimitβis-coproduct
: β {a b} {K : Functor β€Cat C}
β {eta : 2-object-diagram a b => K Fβ !F}
β is-lan !F (2-object-diagram a b) K eta
β is-coproduct C (eta .Ξ· true) (eta .Ξ· false)
is-colimitβis-coproduct {a} {b} {K} {eta} colim = coprod where
module colim = is-colimit colim

D : Functor 2-object-category C
D = 2-object-diagram a b

copair
: β {y} β Hom a y β Hom b y
β β (j : Bool) β Hom (D .Fβ j) y
copair p1 p2 true = p1
copair p1 p2 false = p2

copair-commutes
: β {y} {p1 : Hom a y} {p2 : Hom b y}
β {i j : Bool}
β (p : i β‘ j)
β copair p1 p2 j β D .Fβ p β‘ copair p1 p2 i
copair-commutes {p1 = p1} {p2 = p2} =
J (Ξ» _ p β copair p1 p2 _ β D .Fβ p β‘ copair p1 p2 _)
(elimr (D .F-id))

coprod : is-coproduct C (eta .Ξ· true) (eta .Ξ· false)
coprod .[_,_] f g = colim.universal (copair f g) copair-commutes
coprod .[]βΞΉβ {_} {p1'} {p2'} = colim.factors (copair p1' p2') copair-commutes
coprod .[]βΞΉβ {_} {p1'} {p2'} = colim.factors (copair p1' p2') copair-commutes
coprod .unique p q = colim.unique _ _ _ Ξ» where
true β p
false β q

CoproductβColimit : β {F : Functor 2-object-category C} β Coproduct C (F # true) (F # false) β Colimit F
CoproductβColimit coprod = to-colimit (is-coproductβis-colimit {eta = 2-object-nat-trans _ _} (has-is-coproduct coprod))

ColimitβCoproduct : β {a b} β Colimit (2-object-diagram a b) β Coproduct C a b
ColimitβCoproduct colim .coapex = Colimit.coapex colim
ColimitβCoproduct colim .ΞΉβ = Colimit.cocone colim .Ξ· true
ColimitβCoproduct colim .ΞΉβ = Colimit.cocone colim .Ξ· false
ColimitβCoproduct colim .has-is-coproduct =
is-colimitβis-coproduct (Colimit.has-colimit colim)


## 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}
β {eta : Disc-adjunct {iss = i-is-grpd} F => K Fβ !F}
β is-lan !F (Disc-adjunct F) K eta
β is-indexed-coproduct C F (eta .Ξ·)
is-colimitβis-indexed-coprduct {K = K} {eta} colim = ic where
module colim = is-colimit colim
open is-indexed-coproduct hiding (eta)

ic : is-indexed-coproduct C F (eta .Ξ·)
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)