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 Ξ» where
    .is-iso.inv β†’ match
    .is-iso.rinv x β†’ funext Ξ» i β†’ commute
    .is-iso.linv x β†’ sym (unique _ Ξ» _ β†’ refl)

A category admits indexed coproducts (of level if, for any type and family there is an indexed coproduct of 

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 be a family of objects in If the the indexed coproducts and 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 is an indexed product over 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 is said to be disjoint if every one of its inclusions is monic, and, for unequal the square below is a pullback with initial apex. Since the maps are monic, the pullback below computes the intersection of and as subobjects of hence the name disjoint coproduct: If is an initial object, then 

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 β€” 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 be a category with a zero object, and let be a coproduct. If is a discrete type, then every coproduct inclusion 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 indexed by a discrete type, and a map for some If there exists maps for every then we can obtain a map 

  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 when invoking the universal property of if we use otherwise we use 

  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 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 

  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