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. apply isweqimplimpl. + intros isPull. now apply isPullback_to_isBinProduct. + now apply isaprop_isBinProduct. + now apply isaprop_isPullback. 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.