Definition disp_J_2_0_help {B : bicat} {D : disp_bicat 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 : B} {xx : D x} {yy : D x} (ff : disp_adjoint_equivalence (internal_adjoint_equivalence_identity x) xx yy) : P x x (internal_adjoint_equivalence_identity x) xx yy ff. Proof. pose (disp_J_2_0_help_on_paths P P_id (disp_isotoid_2_0 HD_2_0 ff)). refine (transportf (P x x _ xx yy) _ (disp_J_2_0_help_on_paths P P_id (disp_isotoid_2_0 HD_2_0 ff))). apply disp_idtoiso_2_0_isotoid_2_0. 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.