Definition disp_idtoiso_2_1_inv {B : bicat} {D : disp_bicat B} {b₁ b₂ : B} {f : b₁ --> b₂} {bb₁ : D b₁} {bb₂ : D b₂} (ff₁ ff₂ : bb₁ -->[ f ] bb₂) (p : ff₁ = ff₂) : pr1 (disp_idtoiso_2_1 _ (idpath _) _ _ (!p)) = disp_inv_cell (disp_idtoiso_2_1 _ (idpath _) _ _ p).
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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.