proposition: 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: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monics UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Zero UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.FunctorCategory UniMath.Combinatorics.StandardFiniteSets