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