Definition pullback_to_binprod : some_pullback C Z → some_binprod (C / Z). Proof. intros [A [B [f [g P]]]]. use ((A ,, f) ,, (B ,, g) ,, pullback_to_slice_binprod C P). 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.