Lemma hcomp_rassoc {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 • rassociator g1 g2 g3 = rassociator f1 f2 f3 • x1 ⋆ (x2 ⋆ x3). Proof. use lhs_right_invert_cell. { apply is_invertible_2cell_rassociator. } etrans; [ | apply vassocr ]. apply pathsinv0. use lhs_left_invert_cell. { apply is_invertible_2cell_rassociator. } apply hcomp_lassoc. 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.