Definition pullback_to_slice_binprod {A B Z : C} {f : A --> Z} {g : B --> Z} : Pullback f g -> BinProduct (C / Z) (A ,, f) (B ,, g). Proof. intros P. use (((PullbackObject P ,, (PullbackPr1 P) · f) ,, (((PullbackPr1 P) ,, idpath _) ,, (((PullbackPr2 P) ,, (PullbackSqrCommutes P))))) ,, _). intros Y [j jeq] [k keq]; simpl in jeq , keq. use unique_exists. + use tpair. - apply (PullbackArrow P _ j k). abstract (rewrite <- jeq , keq; apply idpath). - abstract (cbn; rewrite assoc, PullbackArrow_PullbackPr1, <- jeq; apply idpath). + abstract (split; apply eq_mor_slicecat; simpl; [ apply PullbackArrow_PullbackPr1 | apply PullbackArrow_PullbackPr2 ]). + abstract (intros h; apply isapropdirprod; apply has_homsets_slice_precat). + abstract (intros h [H1 H2]; apply eq_mor_slicecat, PullbackArrowUnique; [ apply (maponpaths pr1 H1) | apply (maponpaths pr1 H2) ]). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis.