proposition: Lemma lassociator_to_rassociator_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 : x = lassociator f g h • y) : rassociator f g h • x = y.
proof: Proof. use lhs_left_invert_cell. - apply is_invertible_2cell_rassociator. - exact p. 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