Definition Pullback_z_iso_of_morphisms {C:category} {a b c : C} {f : b --> a} {g : c --> a} (pb : Pullback f g) {b' pb' : C} (i : C⟦b', b⟧) (i' : C⟦pb', pb⟧) (h : C⟦pb', b'⟧) (xi : is_z_isomorphism i) (xi' : is_z_isomorphism i') (Hi : h · i = i' · (PullbackPr1 pb)) : Pullback (i · f) g. Proof. assert (H' : h · (i · f) = i' · PullbackPr2 pb · g). { rewrite assoc, Hi, !assoc'. use cancel_precomposition. use PullbackSqrCommutes. } use (make_Pullback (p1:=h) (p2:=(i' · (PullbackPr2 pb))) H'). use (isPullback_z_iso_of_morphisms (PullbackSqrCommutes pb)). - exact xi. - exact xi'. - exact Hi. - use isPullback_Pullback. 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.