Lemma hcomp_lassoc {a b c d : C} {f1 g1 : C ⟦ a, b ⟧} {f2 g2 : C ⟦ b, c ⟧} {f3 g3 : C ⟦ c, d ⟧} (x1 : f1 ==> g1) (x2 : f2 ==> g2) (x3 : f3 ==> g3) : x1 ⋆ (x2 ⋆ x3) • lassociator g1 g2 g3 = lassociator f1 f2 f3 • (x1 ⋆ x2) ⋆ x3. Proof. unfold hcomp. rewrite <- lwhisker_vcomp. repeat rewrite <- vassocr. rewrite lwhisker_lwhisker. repeat rewrite vassocr. apply maponpaths_2. rewrite <- vassocr. rewrite rwhisker_lwhisker. rewrite vassocr. rewrite <- rwhisker_rwhisker. rewrite <- vassocr. apply maponpaths. apply rwhisker_vcomp. 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.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.