open import Cat.Diagram.Pushout
open import Cat.Prelude

import Cat.Reasoning

module Cat.Diagram.Pushout.Properties where

module _ {o β} {C : Precategory o β} where
open Cat.Reasoning C
open is-pushout



## 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 C 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 C 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 C 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