proposition: Lemma isPullback'_up_to_z_iso {M:category} {a b c d d' : M} (f : b --> a) (g : c --> a) (p1 : d --> b) (p2 : d --> c) (i : z_iso d' d) : isPullback' f g p1 p2 -> isPullback' f g (i·p1) (i·p2).
proof: Proof. intros [e pb]. use tpair. - abstract (rewrite 2 assoc'; apply maponpaths; exact e) using _P_. - cbn beta. intros T r s eq. assert (Q := pb T r s eq). use (iscontrweqf _ Q); clear Q. use weqtotal2. { apply z_iso_comp_left_weq. exact (z_iso_inv i). } { intros h. cbn beta. apply weqiff. { cbn. rewrite 2 (assoc' h). rewrite 2 (assoc _ i). rewrite z_iso_after_z_iso_inv. rewrite 2 id_left. apply isrefl_logeq. } { apply isapropdirprod; apply homset_property. } { apply isapropdirprod; apply homset_property. } } Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Kernels UniMath.CategoryTheory.Limits.Cokernels UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.BinDirectSums UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.CategoriesWithBinOps UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.PrecategoriesWithAbgrops UniMath.CategoryTheory.PreAdditive UniMath.CategoryTheory.Morphisms UniMath.CategoryTheory.Additive UniMath.CategoryTheory.Subcategory.Full UniMath.MoreFoundations.Propositions