open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Pullback
open import Cat.Diagram.Initial
open import Cat.Diagram.Zero
open import Cat.Univalent
open import Cat.Prelude

open import Data.Dec

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.

import Cat.Reasoning C as C
private variable
  o' ℓ' : Level
  Idx : Type ℓ'
  A B S : C.Ob

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 record where
    from   = match
    rinv x = funext λ i → commute
    linv x = sym (unique _ λ _ → refl)

A category $\mathcal{C}$ admits indexed coproducts (of level $\ell \text{)}$ if, for any type $I:\mathrm{Type}\ell$ and family $F:I\to \mathcal{C}\text{,}$ there is an indexed coproduct of $F\text{.}$

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

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 ⊙ lower)
  → Indexed-coproduct F
Lift-Indexed-coproduct _ = Indexed-coproduct-≃ (Lift-≃ e⁻¹)

is-indexed-coproduct-is-prop
  : ∀ {ℓ'} {Idx : Type ℓ'}
  → {F : Idx → C.Ob} {ΣF : C.Ob} {ι : ∀ idx → C.Hom (F idx) ΣF}
  → is-prop (is-indexed-coproduct F ι)
is-indexed-coproduct-is-prop {Idx = Idx} {F} {ΣF} {ι} P Q = path where
  open is-indexed-coproduct

  p : ∀ {X} → (f : ∀ i → C.Hom (F i) X) → P .match f ≡ Q .match f
  p f = Q .unique f (λ i → P .commute)

  path : P ≡ Q
  path i .match f = p f i
  path i .commute {i = idx} {f = f} =
    is-prop→pathp (λ i → C.Hom-set _ _ (p f i C.∘ ι idx) (f idx))
      (P .commute)
      (Q .commute) i
  path i .unique {h = h} f q =
    is-prop→pathp (λ i → C.Hom-set _ _ h (p f i))
      (P .unique f q)
      (Q .unique f q) i

module _ {ℓ'} {Idx : Type ℓ'} {F : Idx → C.Ob} {P P' : Indexed-coproduct F} where
  private
    module P = Indexed-coproduct P
    module P' = Indexed-coproduct P'

  Indexed-coproduct-path
    : (p : P.ΣF ≡ P'.ΣF)
    → (∀ idx → PathP (λ i → C.Hom (F idx) (p i)) (P.ι idx) (P'.ι idx))
    → P ≡ P'
  Indexed-coproduct-path p q i .Indexed-coproduct.ΣF = p i
  Indexed-coproduct-path p q i .Indexed-coproduct.ι idx = q idx i
  Indexed-coproduct-path p q i .Indexed-coproduct.has-is-ic =
    is-prop→pathp (λ i → is-indexed-coproduct-is-prop {ΣF = p i} {ι = λ idx → q idx i})
      P.has-is-ic
      P'.has-is-ic i

Uniqueness🔗

As universal constructions, indexed coproducts are unique up to isomorphism. The proof follows the usual pattern: we use the universal morphisms to construct morphisms in both directions, and uniqueness ensures that these maps form an isomorphism.

is-indexed-coproduct→iso
  : ∀ {ℓ'} {Idx : Type ℓ'} {F : Idx → C.Ob}
  → {ΣF ΣF' : C.Ob}
  → {ι : ∀ i → C.Hom (F i) ΣF} {ι' : ∀ i → C.Hom (F i) ΣF'}
  → is-indexed-coproduct F ι
  → is-indexed-coproduct F ι'
  → ΣF C.≅ ΣF'
is-indexed-coproduct→iso {ι = ι} {ι' = ι'} ΣF-coprod ΣF'-coprod =
  C.make-iso (ΣF.match ι') (ΣF'.match ι)
    (ΣF'.unique₂ (λ i → C.pullr ΣF'.commute ∙ ΣF.commute ∙ sym (C.idl _)))
    (ΣF.unique₂ (λ i → C.pullr ΣF.commute ∙ ΣF'.commute ∙ sym (C.idl _)))
  where
    module ΣF = is-indexed-coproduct ΣF-coprod
    module ΣF' = is-indexed-coproduct ΣF'-coprod

Indexed-coproduct→iso
  : ∀ {ℓ'} {Idx : Type ℓ'} {F : Idx → C.Ob}
  → (P P' : Indexed-coproduct F)
  → Indexed-coproduct.ΣF P C.≅ Indexed-coproduct.ΣF P'
Indexed-coproduct→iso P P' =
  is-indexed-coproduct→iso
    (Indexed-coproduct.has-is-ic P)
    (Indexed-coproduct.has-is-ic P')

Properties🔗

Let $X:\Sigma AB\to \mathcal{C}$ be a family of objects in $\mathcal{C}\text{.}$ If the the indexed coproducts ${\Sigma }_{a,b:\Sigma AB}{X}_{a,b}$ and ${\Sigma }_{a:A}{\Sigma }_{b:B(a)}{X}_{a,b}$ exists, then they are isomorphic.

The formal statement of this is a bit of a mouthful, but all of these arguments are just required to ensure that the various coproducts actually exist.

is-indexed-coproduct-assoc
  : ∀ {κ κ'} {A : Type κ} {B : A → Type κ'}
  → {X : Σ A B → C.Ob}
  → {ΣᵃᵇX : C.Ob} {ΣᵃΣᵇX : C.Ob} {ΣᵇX : A → C.Ob}
  → {ιᵃᵇ : (ab : Σ A B) → C.Hom (X ab) ΣᵃᵇX}
  → {ιᵃ : ∀ a → C.Hom (ΣᵇX a) ΣᵃΣᵇX}
  → {ιᵇ : ∀ a → (b : B a) → C.Hom (X (a , b)) (ΣᵇX a)}
  → is-indexed-coproduct X ιᵃᵇ
  → is-indexed-coproduct ΣᵇX ιᵃ
  → (∀ a → is-indexed-coproduct (λ b → X (a , b)) (ιᵇ a))
  → ΣᵃᵇX C.≅ ΣᵃΣᵇX

Luckily, the proof of this fact is easier than the statement! Indexed coproducts are unique up to isomorphism, so it suffices to show that ${\Sigma }_{a:A}{\Sigma }_{b:B(a)}{X}_{a,b}$ is an indexed product over $X\text{,}$ which follows almost immediately from our hypotheses.

is-indexed-coproduct-assoc {A = A} {B} {X} {ΣᵃΣᵇX = ΣᵃΣᵇX} {ιᵃ = ιᵃ} {ιᵇ} Σᵃᵇ ΣᵃΣᵇ Σᵇ =
  is-indexed-coproduct→iso Σᵃᵇ Σᵃᵇ'
  where
    open is-indexed-coproduct

    ιᵃᵇ' : ∀ (ab : Σ A B) → C.Hom (X ab) ΣᵃΣᵇX
    ιᵃᵇ' (a , b) = ιᵃ a C.∘ ιᵇ a b

    Σᵃᵇ' : is-indexed-coproduct X ιᵃᵇ'
    Σᵃᵇ' .match f = ΣᵃΣᵇ .match λ a → Σᵇ a .match λ b → f (a , b)
    Σᵃᵇ' .commute = C.pulll (ΣᵃΣᵇ .commute) ∙ Σᵇ _ .commute
    Σᵃᵇ' .unique {h = h} f p =
      ΣᵃΣᵇ .unique _ λ a →
      Σᵇ _ .unique _ λ b →
      sym (C.assoc _ _ _) ∙ p (a , b)

Categories with all indexed coproducts🔗

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

module Indexed-coproducts-by
  {κ : Level} {Idx : Type κ}
  (has-ic : has-coproducts-indexed-by Idx)
  where
  module ∐ (F : Idx → C.Ob) = Indexed-coproduct (has-ic F)

  open ∐ renaming (commute to ι-commute; unique to match-unique) public


module Indexed-coproducts
  {κ : Level}
  (has-ic : has-indexed-coproducts κ)
  where
  module ∐ {Idx : Type κ} (F : Idx → C.Ob) = Indexed-coproduct (has-ic F)

  open ∐ renaming (commute to ι-commute; unique to match-unique) public

Disjoint coproducts🔗

An indexed coproduct $\sum F$ is said to be disjoint if every one of its inclusions $F_i\to \sum F$ is monic, and, for unequal $i\ne j\text{,}$ the square below is a pullback with initial apex. Since the maps $F_i\to \sum F\leftarrow F_j$ are monic, the pullback below computes the intersection of $F_i$ and $F_j$ as subobjects of $\sum F\text{,}$ hence the name disjoint coproduct: If $\perp$ is an initial object, then $F_i\cap F_j=\varnothing \text{.}$

record is-disjoint-coproduct (F : Idx → C.Ob) (ι : ∀ i → C.Hom (F i) S)
  : Type (o ⊔ ℓ ⊔ level-of Idx) where
  field
    has-is-ic            : 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 $\perp$ is an initial object, then it is also an indexed coproduct — for any family $\perp \to \mathcal{C}$ — 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 .has-is-ic = 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

Coproducts and zero objects🔗

Let $\mathcal{C}$ be a category with a zero object, and let ${\coprod }_{i:I}{P}_i$ be a coproduct. If $I$ is a discrete type, then every coproduct inclusion ${\iota }_i:\mathcal{C}(P_i,{\coprod }_{i:I}{P}_i)$ has a retract.

module _
  {κ} {Idx : Type κ}
  {P : Idx → C.Ob} {∐P : C.Ob} {ι : ∀ i → C.Hom (P i) ∐P}
  (coprod : is-indexed-coproduct P ι)
  where
  open is-indexed-coproduct coprod

First, a useful lemma. Suppose that we have a coproduct ${\coprod }_{i:I}{P}_i$ indexed by a discrete type, and a map $t_i:\mathcal{C}(P_i,X)$ for some $i:I\text{.}$ If there exists maps $f_j:\mathcal{C}(P_j,X)$ for every $j\ne i\text{,}$ then we can obtain a map $\mathcal{C}({\coprod }_{i:I}{P}_i,X)\text{.}$

  detect
    : ∀ {X} ⦃ Idx-Discrete : Discrete Idx ⦄
    → (i : Idx) → C.Hom (P i) X
    → (∀ (j : Idx) → ¬ i ≡ j → C.Hom (P j) X)
    → C.Hom ∐P X

The key idea here is to check if $i=j$ when invoking the universal property of ${\coprod }_{i:I}{P}_i\text{;}$ if $i=j$ we use $t_i\text{,}$ otherwise we use $f_j\text{.}$

  detect {X = X} ⦃ Idx-Discrete ⦄ i tᵢ fⱼ = match probe
    module detect where
      probe : ∀ (j : Idx) → C.Hom (P j) X
      probe j with i ≡? j
      ... | yes i=j = subst _ i=j tᵢ
      ... | no ¬i=j = fⱼ j ¬i=j

      probe-yes : probe i ≡ tᵢ
      probe-yes with i ≡? i
      ... | yes i=i =
        is-set→subst-refl
          (λ j → C.Hom (P j) X)
          (Discrete→is-set Idx-Discrete)
          i=i tᵢ
      ... | no ¬i=i = absurd (¬i=i refl)

      probe-no : ∀ j → (¬i=j : ¬ (i ≡ j)) → probe j ≡ fⱼ j ¬i=j
      probe-no j ¬i=j with i ≡? j
      ... | yes i=j = absurd (¬i=j i=j)
      ... | no _ = ap (fⱼ j) prop!

Moreover, we observe that our newly created map interacts nicely with the inclusions into the coproduct.

  detect-yes
    : ∀ {X} ⦃ Idx-Discrete : Discrete Idx ⦄
    → {i : Idx} → {tᵢ : C.Hom (P i) X}
    → {fⱼ : ∀ (j : Idx) → ¬ i ≡ j → C.Hom (P j) X}
    → detect i tᵢ fⱼ C.∘ ι i ≡ tᵢ
  detect-yes = commute ∙ detect.probe-yes _ _ _

  detect-no
    : ∀ {X} ⦃ Idx-Discrete : Discrete Idx ⦄
    → {i : Idx} → {tᵢ : C.Hom (P i) X}
    → {fⱼ : ∀ (j : Idx) → ¬ i ≡ j → C.Hom (P j) X}
    → ∀ j → (¬i=j : ¬ i ≡ j) → detect i tᵢ fⱼ C.∘ ι j ≡ fⱼ j ¬i=j
  detect-no j ¬i=j = commute ∙ detect.probe-no _ _ _ j ¬i=j

Refocusing our attention back to our original claim, suppose that $\mathcal{C}$ has a zero object. This means that there is a canonical choice of morphism between any two objects, so we can apply our previous lemma to obtain a retract $\mathcal{C}({\coprod }_I{P}_i,P_i)\text{.}$

  zero→ι-has-retract
    : ∀ ⦃ Idx-Discrete : Discrete Idx ⦄
    → Zero C
    → ∀ i → C.has-retract (ι i)
  zero→ι-has-retract z i =
    C.make-retract (detect i C.id (λ _ _ → zero→)) detect-yes
    where open Zero z