open import Cat.Instances.Product
open import Cat.Prelude

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

open import Cat.Reasoning C
private variable
A B : Ob


# Coproductsπ

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} (ΞΉβ : Hom A P) (ΞΉβ : Hom B P) : Type (o β h) where
field
[_,_] : β {Q} (inj0 : Hom A Q) (inj1 : Hom B Q) β Hom P Q
[]βΞΉβ : β {Q} {inj0 : Hom A Q} {inj1} β [ inj0 , inj1 ] β ΞΉβ β‘ inj0
[]βΞΉβ : β {Q} {inj0 : Hom A Q} {inj1} β [ inj0 , inj1 ] β ΞΉβ β‘ inj1

unique : β {Q} {inj0 : Hom A Q} {inj1}
β {other : Hom P Q}
β other β ΞΉβ β‘ inj0
β other β ΞΉβ β‘ inj1
β other β‘ [ inj0 , inj1 ]

uniqueβ : β {Q} {inj0 : Hom A Q} {inj1}
β β {o1} (p1 : o1 β ΞΉβ β‘ inj0) (q1 : o1 β ΞΉβ β‘ inj1)
β β {o2} (p2 : o2 β ΞΉβ β‘ inj0) (q2 : o2 β ΞΉβ β‘ inj1)
β o1 β‘ o2
uniqueβ p1 q1 p2 q2 = unique p1 q1 β sym (unique p2 q2)


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

record Coproduct (A B : Ob) : Type (o β h) where
field
coapex : Ob
ΞΉβ : Hom A coapex
ΞΉβ : Hom B coapex
has-is-coproduct : is-coproduct ΞΉβ ΞΉβ

open is-coproduct has-is-coproduct public


## Uniquenessπ

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

module _ where
open Coproduct

  +-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.ΞΉβ , c2.ΞΉβ ]

c2βc1 : Hom (coapex c2) (coapex c1)
c2βc1 = c2.[ c1.ΞΉβ , c1.ΞΉβ ]

      c1βc2βc1 : c1βc2 β c2βc1 β‘ id
c1βc2βc1 =
c2.uniqueβ
(pullr c2.[]βΞΉβ β c1.[]βΞΉβ)
(pullr c2.[]βΞΉβ β c1.[]βΞΉβ)
(idl _) (idl _)

c2βc1βc2 : c2βc1 β c1βc2 β‘ id
c2βc1βc2 =
c1.uniqueβ
(pullr c1.[]βΞΉβ β c2.[]βΞΉβ)
(pullr c1.[]βΞΉβ β c2.[]βΞΉβ)
(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) 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 = [ ΞΉβ β f , ΞΉβ β g ]

β-functor : Functor (C ΓαΆ C) C
β-functor .Fβ (a , b) = a ββ b
β-functor .Fβ (f , g) = f ββ g
β-functor .F-id = sym $[]-unique id-comm-sym id-comm-sym β-functor .F-β (f , g) (h , i) = sym$ []-unique
(pullr []βΞΉβ β extendl []βΞΉβ)
(pullr []βΞΉβ β extendl []βΞΉβ)

β : β {a} β Hom (a ββ a) a
β = [ id , id ]

coswap : β {a b} β Hom (a ββ b) (b ββ a)
coswap = [ ΞΉβ , ΞΉβ ]

β-assoc : β {a b c} β Hom (a ββ (b ββ c)) ((a ββ b) ββ c)
β-assoc = [ ΞΉβ β ΞΉβ , [ ΞΉβ β ΞΉβ , ΞΉβ ] ]

  β-natural : is-natural-transformation (β-functor Fβ Catβ¨ Id , Id β©Cat) Id Ξ» _ β β
β-natural x y f = uniqueβ
(pullr []βΞΉβ β cancell []βΞΉβ) (pullr []βΞΉβ β cancell []βΞΉβ)
(cancelr []βΞΉβ) (cancelr []βΞΉβ)

β-coswap : β {a} β β β coswap β‘ β {a}
β-coswap = []-unique (pullr []βΞΉβ β []βΞΉβ) (pullr []βΞΉβ β []βΞΉβ)

β-assoc : β {a} β β {a} β (β {a} ββ id) β β-assoc β‘ β β (id ββ β)
β-assoc = uniqueβ
(pullr (pullr []βΞΉβ) β (reflβ©ββ¨ pulll []βΞΉβ) β pulll (pulll []βΞΉβ) β pullr []βΞΉβ)
(pullr (pullr []βΞΉβ) β []-unique
(pullr (pullr []βΞΉβ) β extend-inner []βΞΉβ β cancell []βΞΉβ β []βΞΉβ)
(pullr (pullr []βΞΉβ) β (reflβ©ββ¨ []βΞΉβ) β cancell []βΞΉβ))
(pullr []βΞΉβ β pulll []βΞΉβ)
(pullr []βΞΉβ β cancell []βΞΉβ)