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. 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.
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.