proposition: Lemma wfs_closed_pullbacks {C : category} (w : wfs C) {x y z : C} {p : x --> y} {f : z --> y} (Pb : Pullback f p) : ((wfs_R w _ _) p) -> ((wfs_R w _ _) (PullbackPr1 Pb)).
proof: Proof. intro p_r. destruct Pb as [[zfx [f'p p2]] [H isPb]]. simpl in *. cbn. unfold wfs_R. rewrite (wfs_rlp w). intros a b i i_l. intros p1 g Hp1g. unfold wfs_R in p_r. rewrite (wfs_rlp w) in p_r. use (p_r _ _ i i_l (p2 ∘ p1) (f ∘ g) _). { rewrite <- assoc, <- H, assoc, Hp1g, assoc. reflexivity. } intro hl. destruct hl as [l [hl1 hl2]]. symmetry in hl2. destruct (isPb _ g l hl2) as [[gh [hgh1 hgh2]] _]. apply hinhpr. exists gh. split. - apply (MorphismsIntoPullbackEqual isPb). * rewrite <-assoc, hgh1, Hp1g. reflexivity. * rewrite <- assoc, hgh2, hl1. reflexivity. - exact hgh1. Qed.
imports: UniMath.MoreFoundations.All UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Lifting