Definition disp_id2_invertible_2cell {C : bicat} {D : disp_prebicat C} {a b : C} {f : C⟦a, b⟧} {aa : D a} {bb : D b} (ff : aa -->[ f ] bb) : disp_invertible_2cell (id2_invertible_2cell f) ff ff. Proof. use tpair. - exact (disp_id2 ff). - use tpair. + cbn. exact (disp_id2 ff). + split ; cbn. * exact (disp_id2_left (disp_id2 ff)). * exact (disp_id2_left (disp_id2 ff)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.Invertible_2cells.