proposition: 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: 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.
imports: UniMath.MoreFoundations.Tactics UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Pullbacks