Definition binproducts_in_product_category (HC₁ : BinProducts C₁) (HC₂ : BinProducts C₂) : BinProducts (category_binproduct C₁ C₂). Proof. intros x y. use make_BinProduct. - simple refine (_ ,, _). + exact (BinProductObject _ (HC₁ (pr1 x) (pr1 y))). + exact (BinProductObject _ (HC₂ (pr2 x) (pr2 y))). - simple refine (_ ,, _). + exact (BinProductPr1 _ (HC₁ (pr1 x) (pr1 y))). + exact (BinProductPr1 _ (HC₂ (pr2 x) (pr2 y))). - simple refine (_ ,, _). + exact (BinProductPr2 _ (HC₁ (pr1 x) (pr1 y))). + exact (BinProductPr2 _ (HC₂ (pr2 x) (pr2 y))). - use isBinProduct_in_product_category. + apply isBinProduct_BinProduct. + apply isBinProduct_BinProduct. 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.