Lemma Pullback_iso_squares_uniqueness (s : ∑ hk : C ⟦ e, p' ⟧, hk · π'_x = g_x × hk · π'_y = g_y) : s = Pullback_iso_squares_existence. Proof. induction s as [s₁ [qₗ qᵣ]]. use subtypePath. { intro ; apply isapropdirprod ; apply homset_property. } cbn. use z_iso_inv_on_left. apply pathsinv0. use (base_paths _ _ (pr2 t (s₁ · i_p ,, _ ,, _))). + rewrite assoc', π_ix. rewrite assoc. now rewrite qₗ. + simpl. rewrite assoc'. rewrite <- π_iy. rewrite assoc. now rewrite qᵣ. Qed.
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.