proposition: Lemma rwhisker_rwhisker_alt {a b c d : C} (f : C ⟦ b, a ⟧) (g : C ⟦ c, b ⟧) {h i : C ⟦ d, c ⟧} (x : h ==> i) : ((x ▹ g) ▹ f) • rassociator i g f = rassociator h g f • (x ▹ g · f).
proof: Proof. apply (vcomp_lcancel (lassociator h g f)). { apply is_invertible_2cell_lassociator. } etrans. { apply vassocr. } etrans. { apply maponpaths_2, rwhisker_rwhisker. } etrans. { apply vassocl. } etrans. { apply maponpaths, lassociator_rassociator. } apply pathsinv0. etrans. { apply vassocr. } etrans. { apply maponpaths_2, lassociator_rassociator. } etrans. - apply id2_left. - apply pathsinv0, id2_right. 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