proposition: Lemma isweq_slice_isBinProduct_to_isPullback {A B Z P : C} {f : A --> Z} {g : B --> Z} {l : P --> A} {r : P --> B} {e : l · f = r · g} : isweq (@slice_isBinProduct_to_isPullback A B Z P f g l r e).
proof: Proof. apply isweqimplimpl. + intros isPull. now apply isPullback_to_isBinProduct. + now apply isaprop_isBinProduct. + now apply isaprop_isPullback. 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