Epi.lean

-- Notes on regular, exact and additive categories
-- Marino Gran


import Mathlib

open CategoryTheory
open Limits

#check Balanced
#check StrongEpi
#check CommSq.HasLift

class strongEpi [Category 𝓒] {P Q : 𝓒} (f : P ⟶ Q) where
  llp {X Y : 𝓒} (z : X ⟶ Y) [Mono z] : HasLiftingProperty f z


#check diag -- : C ⟶ C ⨯ C := prod.lift (𝟙 C) (𝟙 C)
instance diag_mono [Category 𝓒] [HasBinaryProducts 𝓒] (C : 𝓒) :
  Mono (diag C)
:= by
  exact prod.mono_lift_of_mono_left (𝟙 C) (𝟙 C)


instance strongEpi.epi [Category 𝓒] {A B : 𝓒} (f : A ⟶ B) [strongEpi f] [HasBinaryProducts 𝓒] :
  Epi f
:= by
  constructor; intro C u v E
  have H := strongEpi.llp (f := f) (diag C)
  have Sq : CommSq (f ≫ u) f (diag C) (prod.lift u v) := by
    constructor; unfold autoParam; simp [diag]; rw [E]
  have HQ := (H.sq_hasLift) Sq
  have := HQ.exists_lift.some
  rcases this with ⟨t, E1, E2⟩
  simp [diag] at E2
  have El := prod.lift_fst u v
  have Er := prod.lift_snd u v
  rw [<- E2] at El Er; simp at El Er
  rw [<- El, <- Er]


lemma strongEpi.isIso [Category 𝓒] {P Q : 𝓒} (f : P ⟶ Q) [mono : Mono f] [epi : strongEpi f] :
  IsIso f
:= by
  constructor
  have E : CommSq (𝟙 P) f f (𝟙 Q) := by simp
  have H :=  ((epi.llp f).sq_hasLift (f := 𝟙 P) (g := 𝟙 Q) (by simp)).exists_lift.some
  rcases H with ⟨inv, f_inv, inv_f⟩
  use inv, f_inv, inv_f

instance IsIso._strongEpi [Category 𝓒] {P Q : 𝓒} (f : P ⟶ Q) (Hf : IsIso f) :
  strongEpi f
:= by
  constructor; intro X Y g Hg
  constructor; intro h k ⟨E⟩
  constructor; constructor
  have f_inv := Hf.out.choose_spec.1
  have inv_f := Hf.out.choose_spec.2
  set inv:= Hf.out.choose
  refine ⟨inv ≫ h, ?_, ?_⟩
  · rw [<- Category.assoc, f_inv]; simp
  · simp; rw [E, <- Category.assoc, inv_f]; simp


instance strongEpi.comp [Category 𝓒] {P Q R : 𝓒} (f : P ⟶ Q) (g : Q ⟶ R) [Hf : strongEpi f] [Hg : strongEpi g] :
  strongEpi (f ≫ g)
:= by
  constructor; intro X Y m Hm
  constructor; intro h k ⟨E⟩
  constructor; constructor
  have sq : CommSq h f m (g ≫ k) := by
    constructor; rw [E]; simp
  rcases ((Hf.llp m).sq_hasLift sq).exists_lift.some with ⟨l, E1, E2⟩
  rcases ((Hg.llp m).sq_hasLift ⟨E2⟩).exists_lift.some with ⟨o, E3, E4⟩
  refine ⟨o, ?_, ?_⟩
  · simp; rw [E3, E1]
  · rw [E4]


instance strongEpi.decomp [Category 𝓒] {P Q R : 𝓒} (f : P ⟶ Q) (g : Q ⟶ R) (H : strongEpi (f ≫ g)) :
  strongEpi g
:= by
  constructor; intro X Y m Hm
  constructor; intro h k ⟨E⟩
  have sq : CommSq (f ≫ h) (f ≫ g) m k := by
    constructor; simp; rw [E]
  rcases ((H.llp m).sq_hasLift  sq).exists_lift.some with ⟨l, E1, E2⟩
  constructor; constructor
  refine ⟨l, ?_, ?_⟩
  · rw [<- E2, <- Category.assoc] at E
    rw [Hm.right_cancellation _ _ E]
  · rw [E2]

instance strongEpi.decomp_iso [Category 𝓒] {P Q R : 𝓒} (g : P ⟶ Q) (i : Q ⟶ R) (H : strongEpi (g ≫ i)) [Hi : Mono i] :
  IsIso i
:= by
  haveI Hf := decomp _ _ H
  apply isIso


#check RegularEpi
#check RegularEpi.W
#check RegularEpi.left
#check RegularEpi.right
#check RegularEpi.w
#check RegularEpi.isColimit
#check RegularEpi.epi

example [Category 𝓒] (X Y : 𝓒) (f : X ⟶ Y) [Hf : RegularEpi f] :
  Epi f
:= by
  constructor; intro Z g h E
  have Hw := Hf.w
  let c :  Cofork RegularEpi.left RegularEpi.right := by
    apply Cofork.ofπ (f ≫ g)
    rw [<- Category.assoc, Hf.w]; simp
  have Hg := Hf.isColimit.uniq c g; simp [c] at Hg
  have Hh := Hf.isColimit.uniq c h; simp [c] at Hh
  rw [Hg, Hh]
  all_goals (intro j; cases j<;> simp<;> rw [E])


#check SplitEpi
#check SplitEpi.section_
#check SplitEpi.id


section

variable [Category 𝓒] [HasBinaryProducts 𝓒] {X Y : 𝓒} (f : X ⟶ Y)

instance SplitEpi.regularEpi (H : SplitEpi f) :
  RegularEpi f
:= by
  rcases H with ⟨inv, inv_f⟩
  refine {
   W := X
   left := f ≫ inv
   right := 𝟙 X
   w := by simp; rw [inv_f]; simp
   isColimit := {
    desc s := inv ≫ Cofork.π s
    fac s j := by
      rcases j<;> simp
      · slice_lhs 2 3 => rw [inv_f]
        simp
      · change Cofork _ _ at s
        have := s.condition; simp at this
        rw [this]
    uniq s m Hm := by
      simp at m Hm
      have H1 := Hm WalkingParallelPair.one
      simp at H1
      rw [<- H1, <- Category.assoc inv]
      conv => arg 2; arg 1; rw [inv_f]
      simp
   }
  }

instance RegularEpi.isStrongEpi (H : RegularEpi f) :
  strongEpi f
:= by
  have epi := H.epi
  rcases H with ⟨W, left, right, E, H⟩
  constructor; intro A B m Hm
  constructor; intro g h ⟨sq⟩
  constructor; constructor
  let c : Cofork left right := by
    apply Cofork.ofπ g
    apply Hm.right_cancellation; simp
    rw [sq, <- Category.assoc, E]; simp
  have H1 := H.fac c WalkingParallelPair.one; simp at H1
  have H2 := H.fac c WalkingParallelPair.zero; simp at H2
  set k := (H.desc) c; simp [c] at k
  simp [c] at H1 H2
  refine ⟨k, H1, ?_⟩
  apply epi.left_cancellation
  rw [<- sq, <- H1]; simp

end

Regular.lean

import Mathlib
import Category.Regular.SS_1_1_Epi

open CategoryTheory
open Limits

#check strongEpi


#check IsKernelPair
#check RegularEpi


#check IsKernelPair
class HasKernelPair [Category 𝓒] {X Y : 𝓒} (f : X ⟶ Y) where
  has_pullback : HasPullback f f

instance HasKernelPair.hasPullback [Category 𝓒] {X Y : 𝓒} (f : X ⟶ Y) [Hf : HasKernelPair f] :
  HasPullback f f
:= Hf.has_pullback

#check HasCoequalizer
lemma HasKernelPair.hasCoequalizer [Category 𝓒] {X Y : 𝓒} (f : X ⟶ Y) [Hker : HasKernelPair f] [Hreg : RegularEpi f] :
  HasCoequalizer (pullback.fst f f) (pullback.snd f f)
:= by
  rcases Hreg with ⟨W, l, r, E, H⟩
  let mkCofork (s : Cofork (pullback.fst f f) (pullback.snd f f)) : Cofork l r := by
    apply Cofork.ofπ s.π
    have El := pullback.lift_fst  _ _ E
    have Er := pullback.lift_snd  _ _ E
    conv => arg 1; rw [<- El, Category.assoc, s.condition]
    conv => arg 2; rw [<- Er, Category.assoc]
  apply HasColimit.mk ?_
  refine {
    cocone := {
      pt := Y
      ι := {
        app i := by
          cases i<;> simp
          · exact pullback.fst f f ≫ f
          . exact f
        naturality i i' g := by
          rcases g<;> simp
          rw [pullback.condition]
      }
    }
    isColimit := {
      desc s := H.desc (mkCofork s)
      fac s j := by
        have H1 := H.fac (mkCofork s) WalkingParallelPair.one; simp at H1
        simp; rcases j<;> simp
        · rw [H1]; simp [mkCofork]
        · rw [H1]; simp [mkCofork]
      uniq s m Hm := by
        simp at m Hm
        have H1 := Hm WalkingParallelPair.one; simp at H1
        have E := H.uniq (mkCofork s) m; simp [mkCofork] at E
        simp [mkCofork]
        rw [E]
        intro j; cases j<;> simp<;> rw [H1]
    }
  }

lemma IsKernelPair.Mono_iff [Category 𝓒] {A B E : 𝓒} {p : A ⟶ B} {p₁ p₂ : E ⟶ A} (Hp : IsKernelPair p p₁ p₂) :
   Mono p ↔ p₁ = p₂
:= by
  constructor<;> intro H
  · exact H.right_cancellation _ _ Hp.w
  · constructor; intro Z g h Ep
    let k := Hp.lift _ _ Ep
    have := Hp.w
    subst p₁
    rw [<- Hp.lift_fst _ _ Ep, Hp.lift_snd _ _ Ep]

class RegularCategory 𝓒 [Category 𝓒] extends HasFiniteLimits 𝓒 where
  kernelPair_hasCoequalizer {X Y Z : 𝓒} (l r : X ⟶ Y) (f : Y ⟶ Z) :
    IsKernelPair f l r → HasCoequalizer l r
  regularEpi_stable_under_pullback {X Y A B: 𝓒} (f : X ⟶ Y) (g : X ⟶ A) (h : Y ⟶ B) (k : A ⟶ B) :
    IsPullback f g h k → RegularEpi k → RegularEpi f

lemma RegularCategory.self_kernelPair [Category 𝓒] [RegularCategory 𝓒] {X Y : 𝓒} (f : X ⟶ Y) :
  IsKernelPair f (pullback.fst f f) (pullback.snd f f)
:= by
  apply IsPullback.of_hasPullback

instance RegularCategory.kernelPiar_HasCoequalizer [Category 𝓒] [RegularCategory 𝓒] {A X Y : 𝓒} (l r : A ⟶ X) (f : X ⟶ Y) (H : IsKernelPair f l r) :
  HasCoequalizer l r
:= RegularCategory.kernelPair_hasCoequalizer _ _ _ H

instance RegularCategory.pullback_HasCoequalizer [Category 𝓒] [RegularCategory 𝓒] {A B: 𝓒} (f : A ⟶ B) :
  HasCoequalizer (pullback.fst f f) (pullback.snd f f)
:= kernelPiar_HasCoequalizer _ _ f (self_kernelPair f)

noncomputable def RegularCategory.Im  [Category 𝓒] [RegularCategory 𝓒] {A B : 𝓒} (f : A ⟶ B) :=
  coequalizer (pullback.fst f f) (pullback.snd f f)


noncomputable def RegularCategory.image {𝓒} [Category 𝓒] [RegularCategory 𝓒] {A B : 𝓒} (f : A ⟶ B) :
  Im f ⟶ B
:= coequalizer.desc _ (self_kernelPair f).w

noncomputable def RegularCategory.coimage [Category 𝓒] [RegularCategory 𝓒] {A B : 𝓒} (f : A ⟶ B) :
  A ⟶ Im f
:= coequalizer.π (pullback.fst f f) (pullback.snd f f)

lemma RegularCategory.factorize [Category 𝓒] [RegularCategory 𝓒] {A B : 𝓒} (f : A ⟶ B) :
  f = coimage f ≫ image f
:= by simp [image, coimage]

noncomputable instance RegularCategory.coimage_regularEpi [Category 𝓒] [RegularCategory 𝓒] {A B : 𝓒} (f : A ⟶ B) :
  RegularEpi (coimage f)
where
  W := pullback f f
  left := pullback.fst f f
  right := pullback.snd f f
  w := by simp [coimage]; rw [coequalizer.condition]
  isColimit := by
    have Hc := (pullback_HasCoequalizer f).exists_colimit.some.isColimit
    set c := (pullback_HasCoequalizer f).exists_colimit.some.cocone
    change Cofork _ _ at c
    apply IsColimit.ofIsoColimit Hc c.isoCoforkOfπ


instance RegularCategory.image_Mono [Category 𝓒] [RegularCategory 𝓒] {A B : 𝓒} (f : A ⟶ B) :
  Mono (image f)
:= by
  rw [IsKernelPair.Mono_iff (p := image f) (p₁ := pullback.fst (image f) (image f)) (p₂ := pullback.snd (image f) (image f))]; swap
  · exact self_kernelPair (image f)
  ·

    set f₁ := pullback.fst f f
    set f₂ := pullback.snd f f
    set p₁ := pullback.fst (image f) (image f)
    set p₂ := pullback.snd (image f) (image f)
    have Ef₁ := factorize f₁
    have Ef₂ := factorize f₂
    let q := coimage f
    let φ₁ := pullback.fst q p₁
    let φ₂ := pullback.snd q p₁
    let π₁ := pullback.fst p₂ q
    let π₂ := pullback.snd p₂ q
    let a := pullback.fst φ₂ π₁
    let b := pullback.snd φ₂ π₁
    have Hl : IsPullback b (a ≫ φ₁) (π₁ ≫ p₁) q :=
      IsPullback.paste_vert (IsPullback.of_hasPullback _ _).flip (IsPullback.of_hasPullback _ _).flip
    have Hr : IsPullback π₂ (π₁ ≫ p₁) (q ≫ image f) (image f) :=
      IsPullback.paste_vert (IsPullback.of_hasPullback _ _).flip (IsPullback.of_hasPullback _ _).flip
    have Hf :=IsPullback.paste_horiz Hl Hr
    simp [q] at Hf
    rw [<- factorize] at Hf

    have E : (a ≫ φ₁ ≫ coimage f) ≫ image f =  (b ≫ π₂ ≫ coimage f) ≫ image f := by
      simp; rw [<- factorize, <- Category.assoc, <- Hf.w]; simp
    set h := pullback.lift  _ _ E
    have Eh : h = a ≫ φ₂ := by
      apply pullback.hom_ext<;> simp [h]
      · rw [pullback.condition]
      · rw [<- pullback.condition, <- Category.assoc, <- pullback.condition, Category.assoc]
    have Hh : Epi h := by
      rw [Eh]
      refine epi_comp' ?_ ?_
      · suffices : RegularEpi a; exact this.epi
        have : IsPullback (b ≫ π₂) a q (φ₂ ≫ p₂) :=
          IsPullback.paste_horiz (v₁₂ := π₁) (IsPullback.of_hasPullback _ _ ).flip (IsPullback.of_hasPullback _ _).flip
        apply regularEpi_stable_under_pullback _ _ _ _ this.flip (coimage_regularEpi f)
      · suffices : RegularEpi φ₂; exact this.epi
        have : IsPullback φ₁ φ₂ q p₁ := by apply IsPullback.of_hasPullback
        apply regularEpi_stable_under_pullback _ _ _ _ this.flip (coimage_regularEpi f)
    apply Hh.left_cancellation
    have E1 : h ≫ p₁ = _ := pullback.lift_fst _ _ E
    have E2 : h ≫ p₂ = _ := pullback.lift_snd _ _ E
    have E' : (a ≫ φ₁) ≫ f = (b ≫ π₂) ≫ f := by
      simp at E; rw [<- factorize f] at E; simp; rw [E]
    have E1' := pullback.lift_fst _ _ E'
    have E2' := pullback.lift_snd _ _ E'
    rw [E1, E2, <- Category.assoc, <- E1', <- Category.assoc]
    conv => arg 2; arg 1; rw [<- E2']
    rw [Category.assoc, Category.assoc]
    simp only [coimage]
    rw [coequalizer.condition (pullback.fst f f) (pullback.snd f f)]

noncomputable def RegularCategory.iso [Category 𝓒] [RegularCategory 𝓒] {A B : 𝓒}
  {f : A ⟶ B} {I : 𝓒} {e : A ⟶ I} {m : I ⟶ B} [He : RegularEpi e] [Hm : Mono m] (E : f = e ≫ m) :
  Im f ≅ I
:= by
  have Ef := factorize f
  have Mono_f := image_Mono f
  have Epi_f := (coimage_regularEpi f)
  have ⟨l, e_l, l_image⟩ := (((RegularEpi.isStrongEpi e He).llp (image f)).sq_hasLift  ⟨Ef.symm.trans E⟩).exists_lift.some
  have ⟨r, coimage_r, r_m⟩ := ((((RegularEpi.isStrongEpi _ Epi_f).llp m)).sq_hasLift ⟨E.symm.trans Ef⟩).exists_lift.some
  use r, l<;> unfold autoParam
  · apply Mono_f.right_cancellation; simp
    rw [l_image, r_m]
  · apply Hm.right_cancellation; simp
    rw [r_m, l_image]

lemma RegularCategory.coimage_uniq [Category 𝓒] [RegularCategory 𝓒] {A B : 𝓒}
  {f : A ⟶ B} {I : 𝓒} {e : A ⟶ I} {m : I ⟶ B} [He : RegularEpi e] [Hm : Mono m] (E : f = e ≫ m) :
  coimage f = e ≫ (iso E).inv
:= by
  simp [iso]
  have Ef := factorize f
  have Mono_f := image_Mono f
  have ⟨l, e_l, l_image⟩ := Classical.choice (((RegularEpi.isStrongEpi e He).llp (image f)).sq_hasLift  ⟨Ef.symm.trans E⟩).exists_lift
  simp; rw [e_l]

lemma RegularCategory.image_uniq [Category 𝓒] [RegularCategory 𝓒] {A B : 𝓒}
  {f : A ⟶ B} {I : 𝓒} {e : A ⟶ I} {m : I ⟶ B} [He : RegularEpi e] [Hm : Mono m] (E : f = e ≫ m) :
  image f = (iso E).hom ≫ m
:= by
  simp [iso]
  have Ef := factorize f
  have Mono_f := image_Mono f
  have Epi_f := (coimage_regularEpi f)
  have ⟨r, coimage_r, r_m⟩ := Classical.choice ((((RegularEpi.isStrongEpi _ Epi_f).llp m)).sq_hasLift ⟨E.symm.trans Ef⟩).exists_lift
  simp; rw [r_m]


section

variable [Category 𝓒] [RegularCategory 𝓒] {A B C : 𝓒} (f : A ⟶ B) (g : B ⟶ C)

lemma RegularCategory.regularEpi_iff_strongEpi :
  Nonempty (RegularEpi f) ↔ strongEpi f
:= by
  constructor<;> intro H
  · exact RegularEpi.isStrongEpi f H.some
  · constructor

    have sq : CommSq (coimage f) f (image f) (𝟙 B) := by
      constructor; simp; rw [<- factorize f]
    have ⟨l, El1, El2⟩:= ((H.llp (image f)).sq_hasLift sq).exists_lift.some
    apply regularEpi_stable_under_pullback f (𝟙 A) l (coimage f) ?_ (coimage_regularEpi f)
    refine ⟨?_, ?_⟩
    · constructor; unfold autoParam; simp; exact El1
    · constructor
      refine {
        lift s := PullbackCone.snd s
        fac s j := by
          change PullbackCone _ _ at s
          have Es := s.condition
          rcases j with _ | j <;> simp
          · rw [El1, Es]
          · cases j<;> simp
            · rw [<- Category.comp_id s.fst, <- El2, <- Category.assoc, Es, Category.assoc, <- factorize f]
        uniq s m Hm := by
          simp at m Hm
          change PullbackCone _ _ at s
          have Hr := Hm WalkingCospan.right; simp at Hr
          rw [Hr]
      }

noncomputable def RegularCategory.regularEpi_of_strongEpi (Hf : strongEpi f) :
  RegularEpi f
:= ((regularEpi_iff_strongEpi f).mpr Hf).some

noncomputable def RegularCategory.strongEoi_of_regularEpi (Hf : RegularEpi f) :
  strongEpi f
:= ((regularEpi_iff_strongEpi f).mp) ⟨Hf⟩


noncomputable def RegularCategory.regularEpi_decomp_right [H : RegularEpi (f ≫ g)] :
  RegularEpi g
:= by
  apply regularEpi_of_strongEpi
  constructor; intro X Y m Hm
  constructor; intro h k ⟨E⟩
  constructor; constructor
  have sq : CommSq (f ≫ h) (f ≫ g) m k := by
    constructor; simp; rw [E]
  have ⟨l, E1, E2⟩ := (((strongEoi_of_regularEpi (f ≫ g) H).llp m).sq_hasLift sq).exists_lift.some
  use l
  unfold autoParam
  apply Hm.right_cancellation; simp
  rw [E2, E]

noncomputable def RegularCategory.comp [Hf : RegularEpi f] [Hg : RegularEpi g] :
  RegularEpi (f ≫ g)
:= by
  apply regularEpi_of_strongEpi
  constructor; intro X Y m Hm
  constructor; intro h k ⟨E⟩
  constructor; constructor
  have sq : CommSq h f m (g ≫ k) := by
    constructor; rw [E]; simp
  have ⟨l, E1, E2⟩ := (((strongEoi_of_regularEpi _ Hf).llp m).sq_hasLift sq).exists_lift.some
  have ⟨r, E3, E4⟩ := (((strongEoi_of_regularEpi _ Hg).llp m).sq_hasLift ⟨E2⟩).exists_lift.some
  use r; unfold autoParam; simp
  rw [E3, E1]

lemma RegularCategory.iso_iff :
  IsIso f ↔ (Mono f ∧  Nonempty (RegularEpi f))
:= by
  rw [regularEpi_iff_strongEpi]
  constructor<;> intro H
  · rcases H with ⟨inv, f_inv, inv_f⟩
    constructor
    · constructor; intro C g h E
      rw [<- Category.comp_id g, <- f_inv, <- Category.assoc, E, Category.assoc, f_inv]; simp
    · constructor; intro X Y m Hm
      constructor; intro h k ⟨E⟩
      constructor; constructor
      use inv ≫ h<;> unfold autoParam
      · rw [<- Category.assoc, f_inv]; simp
      · simp; rw [E, <- Category.assoc, inv_f]; simp
  · rcases H with ⟨H1, ⟨H2⟩⟩
    have E := ((H2 ( f)).sq_hasLift (f := 𝟙 A) (g := 𝟙 B) (by simp)).exists_lift.some
    rcases E with ⟨inv, f_inv, inv_f⟩
    use inv

noncomputable def RegularCategory.hoge {A' B' : 𝓒} (f' : A' ⟶ B') [Hf : RegularEpi f] [Hf' : RegularEpi f'] :
  RegularEpi (prod.map f f')
:= by
  have H1 : IsPullback (prod.map f (𝟙 A')) prod.fst prod.fst f := {
    toCommSq := by
      constructor; unfold autoParam; simp
    isLimit' := by
      constructor
      refine {
        lift s := prod.lift (PullbackCone.snd s) (PullbackCone.fst s ≫ prod.snd)
        fac s j := by
          change PullbackCone _ _ at s
          have Es := s.condition
          rcases j with _ | j <;> simp
          · rw [Es]
          · cases j<;> simp
            apply Limits.prod.hom_ext<;> simp; rw [Es]
        uniq s m Hm := by
          change PullbackCone _ _ at s
          simp at m Hm
          have Hl := Hm WalkingCospan.left; simp at Hl
          have Hr := Hm WalkingCospan.right; simp at Hr
          have Es := s.condition
          apply Limits.prod.hom_ext<;> simp
          · exact Hr
          · rw [<- Hl]; simp
      }
  }
  have H2 : IsPullback (prod.map (𝟙 B) f') prod.snd prod.snd f' := {
    toCommSq := by
      constructor; unfold autoParam; simp
    isLimit' := by
      constructor
      refine {
        lift s := prod.lift (PullbackCone.fst s ≫ prod.fst) (PullbackCone.snd s)
        fac s j := by
          change PullbackCone _ _ at s
          have Es := s.condition
          rcases j with _ | j <;> simp
          · rw [Es]
          · cases j<;> simp
            apply Limits.prod.hom_ext<;> simp; rw [Es]
        uniq s m Hm := by
          change PullbackCone _ _ at s
          simp at m Hm
          have Hl := Hm WalkingCospan.left; simp at Hl
          have Hr := Hm WalkingCospan.right; simp at Hr
          have Es := s.condition
          apply Limits.prod.hom_ext<;> simp
          · rw [<- Hl]; simp
          · exact Hr
      }
  }
  have H1' := regularEpi_stable_under_pullback _ _ _ _ H1 Hf
  have H2' := regularEpi_stable_under_pullback _ _ _ _ H2 Hf'
  have := comp (prod.map f (𝟙 A')) (prod.map (𝟙 B) f'); simp at this
  exact this

end