Definition isBinCoproduct_in_product_category {x y z : category_binproduct C₁ C₂} (i₁ : x --> z) (i₂ : y --> z) (H₁ : isBinCoproduct _ (pr1 x) (pr1 y) (pr1 z) (pr1 i₁) (pr1 i₂)) (H₂ : isBinCoproduct _ (pr2 x) (pr2 y) (pr2 z) (pr2 i₁) (pr2 i₂)) : isBinCoproduct _ x y z i₁ i₂. Proof. pose (P₁ := make_BinCoproduct _ _ _ _ _ _ H₁). pose (P₂ := make_BinCoproduct _ _ _ _ _ _ H₂). intros w f g. use iscontraprop1. - abstract (use invproofirrelevance ; intros φ₁ φ₂ ; use subtypePath ; [ intro ; apply isapropdirprod ; apply homset_property | ] ; use pathsdirprod ; [ exact (BinCoproductArrowsEq _ _ _ P₁ _ _ _ (maponpaths pr1 (pr12 φ₁) @ !(maponpaths pr1 (pr12 φ₂))) (maponpaths pr1 (pr22 φ₁) @ !(maponpaths pr1 (pr22 φ₂)))) | exact (BinCoproductArrowsEq _ _ _ P₂ _ _ _ (maponpaths dirprod_pr2 (pr12 φ₁) @ !(maponpaths dirprod_pr2 (pr12 φ₂))) (maponpaths dirprod_pr2 (pr22 φ₁) @ !(maponpaths dirprod_pr2 (pr22 φ₂)))) ]). - simple refine ((_ ,, _) ,, _ ,, _). + exact (BinCoproductArrow P₁ (pr1 f) (pr1 g)). + exact (BinCoproductArrow P₂ (pr2 f) (pr2 g)). + abstract (use pathsdirprod ; [ apply (BinCoproductIn1Commutes _ _ _ P₁) | apply (BinCoproductIn1Commutes _ _ _ P₂)]). + abstract (use pathsdirprod ; [ apply (BinCoproductIn2Commutes _ _ _ P₁) | apply (BinCoproductIn2Commutes _ _ _ P₂)]). 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.