module Cat.Diagram.Pushout.Properties {o β„“} {C : Precategory o β„“} where

EpimorphismsπŸ”—

f:A→Bf : A \to B 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