proposition: Lemma path_inverse_2cell {C : bicat} {X Y : C} {f g : C⟦X,Y⟧} (η₁ η₂ : f ==> g) {inv_η₁ : is_invertible_2cell η₁} {inv_η₂ : is_invertible_2cell η₂} : η₁ = η₂ -> inv_η₁^-1 = inv_η₂^-1.
proof: Proof. intros p. rewrite <- (id2_left (inv_η₁^-1)). rewrite <- (id2_right (inv_η₂^-1)). rewrite <- (vcomp_linv inv_η₂). rewrite <- vassocr. apply maponpaths. rewrite <- p. apply vcomp_rinv. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.Bicategories.Core.Bicat