Proposition regular_epi_pb_stable_from_chosen {C : category} (PB : Pullbacks C) (H : regular_epi_chosen_pb_stable PB) : regular_epi_pb_stable C. Proof. intros pb x y z f g π₁ π₂ p HP Hf. pose (P := make_Pullback _ HP). pose (Hpb := H x y z f g Hf). use (is_regular_epi_arrow_z_iso_f _ _ _ _ _ Hpb). - exact (z_iso_from_Pullback_to_Pullback (PB _ _ _ f g) P). - exact (identity_z_iso y). - cbn. rewrite id_right. unfold from_Pullback_to_Pullback. refine (!_). apply (PullbackArrow_PullbackPr2 P). 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.