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. 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.
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.Bicategories.Core.Bicat. Import Bicat.Notations.