Definition disp_J_2_0 {B : bicat} {D : disp_bicat B} (HB_2_0 : is_univalent_2_0 B) (HD_2_0 : disp_univalent_2_0 D) (P : ∏ (x y : B) (f : adjoint_equivalence x y) (xx : D x) (yy : D y), disp_adjoint_equivalence f xx yy → UU) (P_id : ∏ (x : B) (xx : D x), P x x (internal_adjoint_equivalence_identity x) xx xx (disp_identity_adjoint_equivalence xx)) {x y : B} {f : adjoint_equivalence x y} {xx : D x} {yy : D y} (ff : disp_adjoint_equivalence f xx yy) : P x y f xx yy ff. Proof. revert x y f xx yy ff. use (J_2_0 HB_2_0). intros x xx yy ff. exact (disp_J_2_0_help HD_2_0 P P_id 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.