Lemma Pullback_eq (P : Pullbacks C) {x x' y y' z z' : ob C} {f : C⟦x, z⟧} {g : C⟦y, z⟧} {f' : C⟦x', z'⟧} {g' : C⟦y', z'⟧} (i_x : x' = x) (i_y : y' = y) (i_z : z = z') (p1 : idtoiso i_x · f · idtoiso i_z = f') (p2 : idtoiso i_y · g · idtoiso i_z = g') : z_iso (P _ _ _ f g) (P _ _ _ f' g'). Proof. induction i_x, i_y, i_z, p1, p2. cbn. rewrite ! id_left, ! id_right. apply identity_z_iso. 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.