proposition: Lemma isPullback_up_to_z_iso {a' a b c d : C} (f : b --> a) (g : c --> a) (p1 : d --> b) (p2 : d --> c) (H : p1 · f = p2 · g) (i : z_iso a a') (iPb : isPullback (isPullback_up_to_z_iso_eq f g p1 p2 H i)) : isPullback H.
proof: Proof. set (Pb := make_Pullback _ iPb). use make_isPullback. intros e h k Hk. use unique_exists. - use (PullbackArrow Pb). + exact h. + exact k. + use isPullback_up_to_z_iso_eq. exact Hk. - split. + exact (PullbackArrow_PullbackPr1 Pb e h k (isPullback_up_to_z_iso_eq f g h k Hk i)). + exact (PullbackArrow_PullbackPr2 Pb e h k (isPullback_up_to_z_iso_eq f g h k Hk i)). - intros y. apply isapropdirprod; apply C. - intros y X. cbn in X. eapply PullbackArrowUnique. + exact (dirprod_pr1 X). + exact (dirprod_pr2 X). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Monics