proposition: 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: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct