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. induction P as [[P [l r]] [Peq PisPull]]. apply (invmaponpathsincl pr1). { apply isinclpr1. intro. apply isofhleveltotal2. + apply C. + intro. apply isaprop_isPullback. } reflexivity. 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.