proposition: Lemma isPullback_z_iso_of_morphisms (b' d' : C) (h' : C⟦d', b'⟧) (i : C⟦b', b⟧) (i' : C⟦d', d⟧) (xi : is_z_isomorphism i) (xi' : is_z_isomorphism i') (Hi : h' · i = i' · h) (H' : h' · (i · f) = (i' · k) · g) : isPullback H -> isPullback H'.
proof: Proof. intro isPb. use make_isPullback. intros e x y Hxy. set (Pb:= make_Pullback _ isPb). use tpair. - use tpair. + use ( PullbackArrow Pb _ _ _ _ · _ ). * apply (x · i). * apply y. * abstract (rewrite <- assoc; apply Hxy). * apply (inv_from_z_iso (make_z_iso' i' xi')). + cbn. split. * assert (X:= PullbackArrow_PullbackPr1 Pb e (x · i) y ). cbn in X. { match goal with |[ |- ?AA · _ · _ = _ ] => intermediate_path (AA · h · inv_from_z_iso (make_z_iso' i xi)) end. - repeat rewrite <- assoc. apply maponpaths. apply z_iso_inv_on_right. rewrite assoc. apply z_iso_inv_on_left. apply pathsinv0, Hi. - rewrite X. apply pathsinv0. apply z_iso_inv_on_left. apply idpath. } * assert (X:= PullbackArrow_PullbackPr2 Pb e (x · i) y ). cbn in X. repeat rewrite assoc. { match goal with |[|- ?AA · _ · _ · ?K = _ ] => intermediate_path (AA · K) end. - apply cancel_postcomposition. repeat rewrite <- assoc. rewrite z_iso_after_z_iso_inv. apply id_right. - apply X. } - cbn. intro t. apply subtypePath. + intro. apply isapropdirprod; apply C. + cbn. destruct t as [t Ht]; cbn in *. apply z_iso_inv_on_left. apply pathsinv0 , PullbackArrowUnique; cbn in *. * rewrite <- assoc. rewrite <- Hi. rewrite assoc. rewrite (pr1 Ht). apply idpath. * rewrite <- assoc. apply (pr2 Ht). Defined.
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