Lemma BinProduct_OfArrows_assoc : BinProductOfArrows _ Pa_bc Pa_bc' f (BinProductOfArrows _ Pbc Pbc' g h) · (BinProduct_assoc P a b c) = (BinProduct_assoc P a' b' c') · BinProductOfArrows _ Pab_c Pab_c' (BinProductOfArrows _ Pab Pab' f g) h. Proof. unfold BinProduct_assoc, BinProduct_assoc_mor. simpl. use BinProductArrowsEq. + rewrite !assoc', (BinProductPr1Commutes), BinProductOfArrowsPr1, assoc, BinProductPr1Commutes. use BinProductArrowsEq. - now rewrite !assoc', !BinProductOfArrowsPr1, !assoc, !BinProductOfArrowsPr1, id_right, !assoc', id_left. - now rewrite !assoc', !BinProductOfArrowsPr2, !assoc, !BinProductOfArrowsPr2, !assoc', !BinProductOfArrowsPr1. + now rewrite !assoc', !BinProductOfArrowsPr2, !BinProductPr2Commutes, !assoc, !BinProductOfArrowsPr2, !BinProductPr2Commutes, !assoc', !BinProductOfArrowsPr2. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Zero. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.Combinatorics.StandardFiniteSets. Section BinProductFromIso. End BinProductFromIso. Section BinProductsFromProducts. End BinProductsFromProducts. Section ProductsFromBinProducts. End ProductsFromBinProducts.