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