module Cat.Diagram.Pushout.Properties {o β} {C : Precategory o β} where
Epimorphismsπ
is an epimorphism iff. the square below is a pushout
module _ {a b} {f : Hom a b} where is-epicβis-pushout : is-epic f β is-pushout f id f id is-epicβis-pushout epi .square = refl is-epicβis-pushout epi .universal {iββ² = iββ²} p = iββ² is-epicβis-pushout epi .iββuniversal = idr _ is-epicβis-pushout epi .iββuniversal {p = p} = idr _ β epi _ _ p is-epicβis-pushout epi .unique p q = intror refl β p is-pushoutβis-epic : is-pushout f id f id β is-epic f is-pushoutβis-epic pb g h p = sym (pb .iββuniversal {p = p}) β pb .iββuniversal
Pushout additionally preserve epimorphisms, as shown below:
is-epicβpushout-is-epic : β {x y z} {f : Hom x y} {g : Hom x z} {p} {iβ : Hom y p} {iβ : Hom z p} β is-epic f β is-pushout f iβ g iβ β is-epic iβ is-epicβpushout-is-epic {f = f} {g} {iβ = iβ} {iβ} epi pb h j p = eq where module pb = is-pushout pb q : (h β iβ) β f β‘ (j β iβ) β f q = (h β iβ) β f β‘β¨ extendr pb.square β©β‘ (h β iβ) β g β‘β¨ ap (_β g) p β©β‘ (j β iβ) β g β‘Λβ¨ extendr pb.square β©β‘Λ (j β iβ) β f β r : h β iβ β‘ j β iβ r = epi _ _ q eq : h β‘ j eq = pb.uniqueβ {p = extendr pb.square} r p refl refl