proposition: Lemma inverse_of_assoc {C : bicat} {W X Y Z : C} (h : C⟦Y,Z⟧) (g : C⟦X,Y⟧) (f : C⟦W,X⟧) : (is_invertible_2cell_lassociator f g h)^-1 = rassociator f g h.
proof: Proof. apply idpath. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat