Definition isPullback_in_product_category {w x y z : category_binproduct C₁ C₂} {f : x --> z} {g : y --> z} (π₁ : w --> x) (π₂ : w --> y) (p : π₁ · f = π₂ · g) (H₁ : isPullback (maponpaths pr1 p)) (H₂ : isPullback (maponpaths dirprod_pr2 p)) : isPullback p. Proof. intros q h₁ h₂ r. use iscontraprop1. - exact (isPullback_in_product_category_unique π₁ π₂ p H₁ H₂ h₁ h₂). - simple refine (_ ,, _ ,, _). + exact (isPullback_in_product_category_mor π₁ π₂ p H₁ H₂ h₁ h₂ r). + apply isPullback_in_product_category_mor_pr1. + apply isPullback_in_product_category_mor_pr2. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Preservation.