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