🔍

Equations Inline Footnotes

open import Cat.Diagram.Coproduct.Indexed
open import Cat.Instances.Shape.Terminal
open import Cat.Instances.Discrete.Pre
open import Cat.Diagram.Colimit.Base
open import Cat.Instances.Shape.Two
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 $A+B$ and colimits over the functor out of $\mathrm{Disc}(\{0,1\})$ which maps $0$ to $A$ and $1$ to $B\text{,}$ 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} reflᵢ = 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, coproducts indexed by a type $I$ correspond to colimits of shape the fundamental pregroupoid of $I\text{.}$

module _ {I : Type ℓ'} (F : I → Ob) where
  open _=>_

  Inj→Cocone : ∀ {x} → (∀ i → Hom (F i) x) → Π₁-adjunct C F => Const x
  Inj→Cocone inj .η i = inj i
  Inj→Cocone inj .is-natural i j = elim! $
    J (λ j p → inj j ∘ subst (Hom (F i) ⊙ F) p id ≡ id ∘ inj i)
      (elimr (transport-refl id) ∙ sym (idl _))

  is-indexed-coproduct→is-colimit
    : ∀ {x} {inj : ∀ i → Hom (F i) x}
    → is-indexed-coproduct C F inj
    → is-colimit (Π₁-adjunct C 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 (Π₁-adjunct C F) x
    mc .ψ i = inj i
    mc .commutes {i} {j} = elim! $
      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

  is-colimit→is-indexed-coprduct
    : ∀ {K : Functor ⊤Cat C}
    → {eta : Π₁-adjunct C F => K F∘ !F}
    → is-lan !F (Π₁-adjunct C 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 comm where abstract
      comm : {x y : I} (h : ∥ x ≡ y ∥₀) → k y ∘ Π₁-adjunct₁ C F h ≡ k x
      comm = elim! $ J
        (λ y p → k y ∘ path→iso (ap F p) .to ≡ k _) (elimr (transport-refl _))
    ic .commute       = colim.factors _ _
    ic .unique k comm = colim.unique _ _ _ comm

  IC→Colimit : Indexed-coproduct C F → Colimit (Π₁-adjunct C F)
  IC→Colimit ic = to-colimit (is-indexed-coproduct→is-colimit has-is-ic)
    where open Indexed-coproduct ic

  Colimit→IC : Colimit (Π₁-adjunct C 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