open import Cat.Prelude

module Cat.Diagram.Coproduct {o h} (C : Precategory o h) where


# Coproducts🔗

The coproduct $P$ of two objects $A$ and $B$ (if it exists), is the smallest object equipped with “injection” maps $A \to P$, $B \to P$. It is dual to the product.

We witness this notion of “smallest object” with a universal property; Given any other $Q$ that also admits injection maps from $A$ and $B$, we must have a unique map $P \to Q$ that factors the injections into $Q$. This is best explained by a commutative diagram:

record is-coproduct {A B P} (in₀ : Hom A P) (in₁ : Hom B P) : Type (o ⊔ h) where
field
[_,_]      : ∀ {Q} (inj0 : Hom A Q) (inj1 : Hom B Q) → Hom P Q
in₀∘factor : ∀ {Q} {inj0 : Hom A Q} {inj1} → [ inj0 , inj1 ] ∘ in₀ ≡ inj0
in₁∘factor : ∀ {Q} {inj0 : Hom A Q} {inj1} → [ inj0 , inj1 ] ∘ in₁ ≡ inj1

unique : ∀ {Q} {inj0 : Hom A Q} {inj1}
→ (other : Hom P Q)
→ other ∘ in₀ ≡ inj0
→ other ∘ in₁ ≡ inj1
→ other ≡ [ inj0 , inj1 ]

unique₂ : ∀ {Q} {inj0 : Hom A Q} {inj1}
→ ∀ o1 (p1 : o1 ∘ in₀  ≡ inj0) (q1 : o1 ∘ in₁ ≡ inj1)
→ ∀ o2 (p2 : o2 ∘ in₀  ≡ inj0) (q2 : o2 ∘ in₁ ≡ inj1)
→ o1 ≡ o2
unique₂ o1 p1 q1 o2 p2 q2 = unique o1 p1 q1 ∙ sym (unique o2 p2 q2)


A coproduct of $A$ and $B$ is an explicit choice of coproduct diagram:

record Coproduct (A B : Ob) : Type (o ⊔ h) where
field
coapex : Ob
in₀ : Hom A coapex
in₁ : Hom B coapex
has-is-coproduct : is-coproduct in₀ in₁

open is-coproduct has-is-coproduct public

open Coproduct


## Uniqueness🔗

The uniqueness argument presented here is dual to the argument for the Product.

+-Unique : (c1 c2 : Coproduct A B) → coapex c1 ≅ coapex c2
+-Unique c1 c2 = make-iso c1→c2 c2→c1 c1→c2→c1 c2→c1→c2
where
module c1 = Coproduct c1
module c2 = Coproduct c2

c1→c2 : Hom (coapex c1) (coapex c2)
c1→c2 = c1.[ c2.in₀ , c2.in₁ ]

c2→c1 : Hom (coapex c2) (coapex c1)
c2→c1 = c2.[ c1.in₀ , c1.in₁ ]

    c1→c2→c1 : c1→c2 ∘ c2→c1 ≡ id
c1→c2→c1 =
c2.unique₂ _
(pullr c2.in₀∘factor ∙ c1.in₀∘factor)
(pullr c2.in₁∘factor ∙ c1.in₁∘factor)
id (idl _) (idl _)

c2→c1→c2 : c2→c1 ∘ c1→c2 ≡ id
c2→c1→c2 =
c1.unique₂ _
(pullr c1.in₀∘factor ∙ c2.in₀∘factor)
(pullr c1.in₁∘factor ∙ c2.in₁∘factor)
id (idl _) (idl _)