Proposition is_regular_epi_arrow_z_iso_f {C : category} {x₁ x₂ y₁ y₂ : C} (f₁ : x₁ --> y₁) (f₂ : x₂ --> y₂) (i₁ : z_iso x₁ x₂) (i₂ : z_iso y₁ y₂) (p : f₁ · i₂ = i₁ · f₂) : is_regular_epi f₁ → is_regular_epi f₂. Proof. assert (inv_from_z_iso i₁ · f₁ = f₂ · inv_from_z_iso i₂) as p'. { use z_iso_inv_on_left. rewrite !assoc'. refine (!_). use z_iso_inv_on_right. exact p. } use factor_through_squash. { apply isaprop_is_regular_epi. } intros ( w & g₁ & g₂ & q & H ). pose (Coeq := make_Coequalizer _ _ _ _ H). use hinhpr. simple refine (w ,, g₁ · i₁ ,, g₂ · i₁ ,, _ ,, _). - abstract (rewrite !assoc' ; rewrite <- !p ; rewrite !assoc ; rewrite q ; apply idpath). - intros z h r. use iscontraprop1. + use invproofirrelevance. intros φ₁ φ₂. use subtypePath. { intro. apply homset_property. } use (cancel_z_iso' i₂). use (CoequalizerOutsEq Coeq). cbn. rewrite !assoc. rewrite !p. rewrite !assoc'. apply maponpaths. exact (pr2 φ₁ @ !(pr2 φ₂)). + simple refine (_ ,, _). * simple refine (inv_from_z_iso i₂ · CoequalizerOut Coeq _ _ _). ** exact (i₁ · h). ** abstract (rewrite !assoc ; exact r). * cbn. refine (assoc _ _ _ @ _). rewrite <- p'. rewrite !assoc'. etrans. { apply maponpaths. apply (CoequalizerCommutes Coeq). } rewrite !assoc. rewrite z_iso_after_z_iso_inv. apply id_left. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Limits.Coequalizers. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Epis.