Definition disp_idtoiso_2_1 {a b : C} {f g : C⟦a, b⟧} (p : f = g) {aa : D a} {bb : D b} (ff : aa -->[ f ] bb) (gg : aa -->[ g ] bb) (pp : transportf (λ z, _ -->[ z ] _) p ff = gg) : disp_invertible_2cell (idtoiso_2_1 f g p) ff gg. Proof. induction p. induction pp. exact (disp_id2_invertible_2cell ff). Defined.
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.