Lemma rassociator_rassociator {a b c d e : C} (f : C ⟦ a, b ⟧) (g : C ⟦ b, c ⟧) (h : C ⟦ c, d ⟧) (i : C ⟦ d, e ⟧) : ((rassociator f g h ▹ i) • rassociator f (g · h) i) • (f ◃ rassociator g h i) = rassociator (f · g) h i • rassociator f g (h · i). Proof. apply (vcomp_lcancel (lassociator (f · g) h i)). { apply is_invertible_2cell_lassociator. } apply (vcomp_lcancel (lassociator f g (h · i))). { apply is_invertible_2cell_lassociator. } etrans. { apply vassocr. } etrans. { apply maponpaths_2, pathsinv0. apply lassociator_lassociator. } etrans. { apply vassocl. } etrans. { apply maponpaths. etrans. { apply maponpaths, vassocl. } etrans. { apply vassocr. } apply maponpaths_2. etrans. { apply rwhisker_vcomp. } apply maponpaths, lassociator_rassociator. } apply pathsinv0. etrans. { apply maponpaths. etrans. { apply vassocr. } etrans. { apply maponpaths_2, lassociator_rassociator. } apply id2_left. } etrans. { apply lassociator_rassociator. } apply pathsinv0. etrans. { apply maponpaths. etrans. { apply vassocr. } apply maponpaths_2. etrans. { apply maponpaths_2, id2_rwhisker. } apply id2_left. } etrans. { apply vassocl. } etrans. { apply maponpaths. etrans. { apply vassocr. } etrans. { apply maponpaths_2. apply lassociator_rassociator. } apply id2_left. } etrans. { apply lwhisker_vcomp. } etrans. { apply maponpaths. apply lassociator_rassociator. } apply lwhisker_id2. 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.