open import Cat.Prelude

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


The coproduct PP of two objects AA and BB (if it exists), is the smallest object equipped with “injection” maps APA \to P, BPB \to P. It is dual to the product.

We witness this notion of “smallest object” with a universal property; Given any other QQ that also admits injection maps from AA and BB, we must have a unique map PQP \to Q that factors the injections into QQ. 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
    [_,_]      :  {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 AA and BB is an explicit choice of coproduct diagram:

record Coproduct (A B : Ob) : Type (o  h) where
    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


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