Definition isBinProduct_in_iso_comma_ump : w --> z. Proof. simple refine ((_ ,, _) ,, _) ; cbn. - exact (BinProductArrow _ P₁ (pr11 f) (pr11 g)). - exact (BinProductArrow _ P₂ (pr21 f) (pr21 g)). - use (BinProductArrowsEq _ _ _ (make_BinProduct _ _ _ _ _ _ (HG _ _ _ _ _ (pr2 P₂)))) ; cbn. + abstract (rewrite !assoc' ; rewrite <- functor_comp ; rewrite (BinProductPr1Commutes _ _ _ P₂) ; refine (_ @ pr2 f) ; refine (!(maponpaths (λ z, _ · z) (pr2 p₁)) @ _) ; rewrite !assoc ; rewrite <- functor_comp ; rewrite (BinProductPr1Commutes _ _ _ P₁) ; apply idpath). + abstract (rewrite !assoc' ; rewrite <- functor_comp ; rewrite (BinProductPr2Commutes _ _ _ P₂) ; refine (_ @ pr2 g) ; refine (!(maponpaths (λ z, _ · z) (pr2 p₂)) @ _) ; rewrite !assoc ; rewrite <- functor_comp ; rewrite (BinProductPr2Commutes _ _ _ P₁) ; apply idpath). 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.