Lemma rassociator_to_lassociator_pre {a b c d : C} {f : C ⟦ a, b ⟧} {g : C ⟦ b, c ⟧} {h : C ⟦ c, d ⟧} {k : C ⟦ a, d ⟧} (x : f · (g · h) ==> k) (y : (f · g) · h ==> k) (p : rassociator f g h • x = y) : x = lassociator f g h • y. Proof. apply pathsinv0. use lhs_left_invert_cell. - apply is_invertible_2cell_lassociator. - exact (!p). 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.