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

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 C\mathcal{C} admits indexed coproducts (of level ℓ\ell) if, for any type I:Type ℓI : \mathrm{Type}\ \ell and family F:I→CF : I \to \mathcal{C}, there is an indexed coproduct of FF.

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

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

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 βŠ™ Lift.lower)
  β†’ Indexed-coproduct F
Lift-Indexed-coproduct _ = Indexed-coproduct-≃ (Lift-≃ e⁻¹)

Disjoint coproductsπŸ”—

An indexed coproduct βˆ‘F\sum F is said to be disjoint if every one of its inclusions Fiβ†’βˆ‘FF_i \to \sum F is monic, and, for unequal iβ‰ ji \ne j, the square below is a pullback with initial apex. Since the maps Fiβ†’βˆ‘F←FjF_i \to \sum F \leftarrow F_j are monic, the pullback below computes the intersection of FiF_i and FjF_j as subobjects of βˆ‘F\sum F, hence the name disjoint coproduct: If βŠ₯\bot is an initial object, then Fi∩Fj=βˆ…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
    is-coproduct         : 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 βŠ₯\bot is an initial object, then it is also an indexed coproduct β€” for any family βŠ₯β†’C\bot \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 .is-coproduct = 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