Lemma isPullback_to_isBinProduct {Z : C} {AZ BZ PZ : C / Z} {l : PZ --> AZ} {r : PZ --> BZ} : @isPullback _ _ _ _ _ (pr2 AZ) (pr2 BZ) (pr1 l) (pr1 r) (! (pr2 l) @ (pr2 r)) → isBinProduct (C / Z) AZ BZ PZ l r. Proof. induction AZ as [A f]. induction BZ as [B g]. induction PZ as [P h]. induction l as [l leq]. induction r as [r req]. intros isPull [Y i] [j jeq] [k keq]; simpl in *. unfold isPullback in isPull. specialize isPull with Y j k. use unique_exists. + use tpair. ++ apply isPull. abstract (simpl; now rewrite <- jeq , keq). ++ abstract (simpl; now rewrite leq, assoc, (pr1 (pr2 (pr1 (isPull _)))), jeq). + abstract (split; apply (eq_mor_slicecat C); simpl; [apply (pr1 (pr2 (pr1 (isPull _)))) | apply (pr2 (pr2 (pr1 (isPull _))))]). + abstract (now intros q; apply isapropdirprod; apply (has_homsets_slice_precat C)). + abstract (intros q [H1 H2]; apply (eq_mor_slicecat C); use (maponpaths pr1 ((pr2 (isPull _)) ((pr1 q) ,, (_ ,, _)))); [apply (maponpaths pr1 H1) | apply (maponpaths pr1 H2)]). Defined.
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.