module Cat.Diagram.Coproduct {o h} (C : Precategory o h) where
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} (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 and 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
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 _)
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 ]