Definition bincoproducts_in_product_category (HC₁ : BinCoproducts C₁) (HC₂ : BinCoproducts C₂) : BinCoproducts (category_binproduct C₁ C₂). Proof. intros x y. use make_BinCoproduct. - simple refine (_ ,, _). + exact (BinCoproductObject (HC₁ (pr1 x) (pr1 y))). + exact (BinCoproductObject (HC₂ (pr2 x) (pr2 y))). - simple refine (_ ,, _). + exact (BinCoproductIn1 (HC₁ (pr1 x) (pr1 y))). + exact (BinCoproductIn1 (HC₂ (pr2 x) (pr2 y))). - simple refine (_ ,, _). + exact (BinCoproductIn2 (HC₁ (pr1 x) (pr1 y))). + exact (BinCoproductIn2 (HC₂ (pr2 x) (pr2 y))). - use isBinCoproduct_in_product_category. + apply isBinCoproduct_BinCoproduct. + apply isBinCoproduct_BinCoproduct. 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.