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