Lemma regular_epi_pb_stable_to_pb_preserves_pb_sqr : isPullback regular_epi_pb_stable_to_pb_preserves_pb_sqr_eq. Proof. intros w l l' q. use iscontraprop1. - use invproofirrelevance. intros ζ₁ ζ₂. use subtypePath. { intro. apply isapropdirprod ; apply homset_property. } use (MorphismsIntoPullbackEqual (isPullback_Pullback P₁)). + exact (pr12 ζ₁ @ !(pr12 ζ₂)). + pose (maponpaths (λ z, z · PullbackPr2 P₂) (pr22 ζ₁ @ !(pr22 ζ₂))) as qr. cbn in qr. rewrite !assoc' in qr. unfold k in qr. rewrite !PullbackArrow_PullbackPr2 in qr. exact qr. - simple refine (_ ,, _ ,, _). + use PullbackArrow. * exact l. * exact (l' · ρ₂). * refine (maponpaths (λ z, _ · z) (!(mor_eq hp)) @ _). rewrite !assoc. refine (maponpaths (λ z, z · _) q @ _). rewrite !assoc'. apply maponpaths. apply PullbackSqrCommutes. + apply PullbackArrow_PullbackPr1. + use (MorphismsIntoPullbackEqual (isPullback_Pullback P₂)). * unfold k. refine (assoc' _ _ _ @ _). rewrite PullbackArrow_PullbackPr1. refine (assoc _ _ _ @ _). rewrite PullbackArrow_PullbackPr1. exact q. * unfold k. refine (assoc' _ _ _ @ _). rewrite !PullbackArrow_PullbackPr2. apply idpath. 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.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis. Require Import UniMath.CategoryTheory.EpiFacts. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpi. Require Import UniMath.CategoryTheory.RegularAndExact.RegularCategory. Require Import UniMath.CategoryTheory.RegularAndExact.RegularEpiFacts. Require Import UniMath.CategoryTheory.RegularAndExact.ExactCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.FiberCod. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodColimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodMorphisms. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodLimits. Require Import UniMath.CategoryTheory.DisplayedCats.Codomain.CodFunctor. Section PreservesFromStable. End PreservesFromStable.