proposition: Lemma pullback_to_slice_binprod_inv {A B : C} {f : A --> Z} {g : B --> Z} (P : Pullback f g) : slice_binprod_to_pullback C (pullback_to_slice_binprod C P) = P.
proof: Proof. induction P as [[P [l r]] [Peq PisPull]]. apply (invmaponpathsincl pr1). { apply isinclpr1. intro. apply isofhleveltotal2. + apply C. + intro. apply isaprop_isPullback. } reflexivity. 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