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


The coproduct of two objects and (if it exists), is the smallest object equipped with β€œinjection” maps It is dual to the product.

We witness this notion of β€œsmallest object” with a universal property; Given any other that also admits injection maps from and we must have a unique map that factors the injections into 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 and 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


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

Categories with all binary coproductsπŸ”—

Categories with all binary coproducts are quite common, so we define a module for working with them.

has-coproducts : Type _
has-coproducts = βˆ€ a b β†’ Coproduct a b

module Binary-coproducts (all-coproducts : has-coproducts) where

  module coproduct {a} {b} = Coproduct (all-coproducts a b)

  open coproduct renaming
    (unique to []-unique; inβ‚€βˆ˜factor to inβ‚€βˆ˜[]; inβ‚βˆ˜factor to inβ‚βˆ˜[]) public
  open Functor

  infixr 7 _βŠ•β‚€_
  infix 50 _βŠ•β‚_

  _βŠ•β‚€_ : Ob β†’ Ob β†’ Ob
  a βŠ•β‚€ b = coproduct.coapex {a} {b}

  _βŠ•β‚_ : βˆ€ {a b x y} β†’ Hom a x β†’ Hom b y β†’ Hom (a βŠ•β‚€ b) (x βŠ•β‚€ y)
  f βŠ•β‚ g = [ inβ‚€ ∘ f , in₁ ∘ g ]