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. 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.
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.