Definition disp_J_2_0_help_on_paths {B : bicat} {D : disp_bicat B} (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} (p : xx = yy) : P x x (internal_adjoint_equivalence_identity x) xx yy (disp_idtoiso_2_0 D (idpath x) xx yy p). Proof. induction p. apply P_id. 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.