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.

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 λ where
    .is-iso.inv → match
    .is-iso.rinv x → funext λ i → commute
    .is-iso.linv x → sym (unique _ λ _ → refl)

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

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

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

Properties🔗

Let $X : Σ A B \to C$ be a family of objects in $C .$ If the the indexed coproducts $Σ_{a, b : Σ A B} X_{a, b}$ and $Σ_{a : A} Σ_{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 $Σ_{a : A} Σ_{b : B (a)} X_{a, b}$ is an indexed product over $X,$ 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 \neq = j,$ 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,$ hence the name disjoint coproduct: If $⊥$ is an initial object, then $F_{i} \cap F_{j} = \emptyset .$

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 $⊥$ is an initial object, then it is also an indexed coproduct — for any family $⊥ \to 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 $C$ be a category with a zero object, and let $∐_{i : I} P_{i}$ be a coproduct. If $I$ is a discrete type, then every coproduct inclusion $ι_{i} : C (P_{i}, ∐_{i : I} P_{i})$ has a retract.

First, a useful lemma. Suppose that we have a coproduct $∐_{i : I} P_{i}$ indexed by a discrete type, and a map $t_{i} : C (P_{i}, X)$ for some $i : I .$ If there exists maps $f_{j} : C (P_{j}, X)$ for every $j \neq = i,$ then we can obtain a map $C (∐_{i : I} P_{i}, X) .$

  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 $∐_{i : I} P_{i};$ if $i = j$ we use $t_{i},$ otherwise we use $f_{j} .$

  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 $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 $C (∐_{I} P_{i}, P_{i}) .$

  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