Definition disp_alg_bicat_disp_is_invertible_2cell {a b : C} {f : a --> b} {g : a --> b} (x : invertible_2cell f g) {aa : disp_alg_bicat a} {bb : disp_alg_bicat b} (ff : aa -->[ f ] bb) (gg : aa -->[ g ] bb) (xx : ff ==>[x] gg) : is_disp_invertible_2cell x xx. Proof. use tpair. - cbn in *. unfold alg_disp_cat_2cell in *. use vcomp_move_R_pM. { is_iso. } cbn. rewrite vassocr. use vcomp_move_L_Mp. { is_iso. refine (psfunctor_is_iso F (x ^-1 ,, _)). is_iso. } cbn. exact (!xx). - split ; apply C. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.PseudoFunctors.Display.PseudoFunctorBicat. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.