module Cat.Diagram.Pushout.Properties 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 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 .universal∘i₁ = idr _
    is-epicβ†’is-pushout epi .universal∘iβ‚‚ {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 .universal∘i₁ {p = p}) βˆ™ pb .universal∘iβ‚‚

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