proposition: Lemma slice_binprod_to_pullback_inv {AZ BZ : C / Z} (P : BinProduct (C / Z) AZ BZ) : pullback_to_slice_binprod C (slice_binprod_to_pullback C P) = P.
proof: Proof. induction AZ as [A f]. induction BZ as [B g]. induction P as [[[P h] [[l leq] [r req]]] PisProd]. apply (invmaponpathsincl pr1). { apply isinclpr1. intro. apply isaprop_isBinProduct. } simpl in *. use total2_paths2_f. + apply (total2_paths2_f (idpath _)). rewrite idpath_transportf. exact (!leq). + induction (!leq). simpl. rewrite idpath_transportf. use total2_paths2_f. - now apply (eq_mor_slicecat C). - rewrite transportf_const. now apply (eq_mor_slicecat C). 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