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. 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Monics. Definition UnivProductFromPullback (c d a : C) (f : a --> c) (g : a --> d): exists (UnivProductFromPullback c d a f g). Definition BinProductsFromPullbacks : BinProducts C := BinProduct_Pullback.