Definition pullbacks_in_product_category (HC₁ : Pullbacks C₁) (HC₂ : Pullbacks C₂) : Pullbacks (category_binproduct C₁ C₂). Proof. intros z x y f g. simple refine ((_ ,, _ ,, _) ,, (_ ,, _)). - refine (_ ,, _). + exact (PullbackObject (HC₁ _ _ _ (pr1 f) (pr1 g))). + exact (PullbackObject (HC₂ _ _ _ (pr2 f) (pr2 g))). - refine (_ ,, _). + apply PullbackPr1. + apply PullbackPr1. - refine (_ ,, _). + apply PullbackPr2. + apply PullbackPr2. - apply pathsdirprod. + apply PullbackSqrCommutes. + apply PullbackSqrCommutes. - use isPullback_in_product_category. + apply isPullback_Pullback. + apply isPullback_Pullback. 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.