Definition isBinCoproduct_in_iso_comma_ump : z --> w. Proof. simple refine ((_ ,, _) ,, _) ; cbn. - exact (BinCoproductArrow P₁ (pr11 f) (pr11 g)). - exact (BinCoproductArrow P₂ (pr21 f) (pr21 g)). - use (BinCoproductArrowsEq _ _ _ (make_BinCoproduct _ _ _ _ _ _ (HF _ _ _ _ _ (pr2 P₁)))) ; cbn. + abstract (rewrite !assoc ; rewrite <- functor_comp ; rewrite (BinCoproductIn1Commutes _ _ _ P₁) ; refine (pr2 f @ _) ; refine (_ @ maponpaths (λ z, z · _) (!(pr2 i₁))) ; rewrite !assoc' ; apply maponpaths ; rewrite <- functor_comp ; apply maponpaths ; refine (!_) ; apply (BinCoproductIn1Commutes _ _ _ P₂)). + abstract (rewrite !assoc ; rewrite <- functor_comp ; rewrite (BinCoproductIn2Commutes _ _ _ P₁) ; refine (pr2 g @ _) ; refine (_ @ maponpaths (λ z, z · _) (!(pr2 i₂))) ; rewrite !assoc' ; apply maponpaths ; rewrite <- functor_comp ; apply maponpaths ; refine (!_) ; 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.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.