Definition bincoproducts_in_iso_comma (HC₁ : BinCoproducts C₁) (HC₂ : BinCoproducts C₂) : BinCoproducts (iso_comma F G). Proof. intros x y. pose (FP := make_BinCoproduct _ _ _ _ _ _ (HF (pr11 x) (pr11 y) _ (BinCoproductIn1 (HC₁ (pr11 x) (pr11 y))) (BinCoproductIn2 (HC₁ (pr11 x) (pr11 y))) (isBinCoproduct_BinCoproduct _ (HC₁ (pr11 x) (pr11 y))))). pose (GP := make_BinCoproduct _ _ _ _ _ _ (HG (pr21 x) (pr21 y) _ (BinCoproductIn1 (HC₂ (pr21 x) (pr21 y))) (BinCoproductIn2 (HC₂ (pr21 x) (pr21 y))) (isBinCoproduct_BinCoproduct _ (HC₂ (pr21 x) (pr21 y))))). use make_BinCoproduct. - simple refine ((_ ,, _) ,, _). + exact (BinCoproductObject (HC₁ (pr11 x) (pr11 y))). + exact (BinCoproductObject (HC₂ (pr21 x) (pr21 y))). + exact (bincoproduct_of_z_iso FP GP (pr2 x) (pr2 y)). - simple refine ((_ ,, _) ,, _). + exact (BinCoproductIn1 (HC₁ (pr11 x) (pr11 y))). + exact (BinCoproductIn1 (HC₂ (pr21 x) (pr21 y))). + exact ((BinCoproductOfArrowsIn1 _ FP GP (pr12 x) (pr12 y))). - simple refine ((_ ,, _) ,, _). + exact (BinCoproductIn2 (HC₁ (pr11 x) (pr11 y))). + exact (BinCoproductIn2 (HC₂ (pr21 x) (pr21 y))). + exact ((BinCoproductOfArrowsIn2 _ FP GP (pr12 x) (pr12 y))). - use isBinCoproduct_in_iso_comma. + 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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.IsoCommaCategory. 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.