Lemma isweq_isPullback_to_isBinProduct {Z : C} {AZ BZ PZ : C / Z} {l : PZ --> AZ} {r : PZ --> BZ} : isweq (@isPullback_to_isBinProduct Z AZ BZ PZ l r). Proof. apply isweqimplimpl. + induction AZ as [A f]. induction BZ as [B g]. induction PZ as [P h]. induction l as [l leq]. induction r as [r req]. simpl in *. induction (! leq). assert (H : leq = idpath (l · f)) by apply C. intros PisProd. apply slice_isBinProduct_to_isPullback; simpl. rewrite <- H. exact PisProd. + apply isaprop_isPullback. + apply isaprop_isBinProduct. Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks.