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 Aβ†’PA \to P, Bβ†’PB \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 Pβ†’QP \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 _)