Lemma adjoint_equivalence_total_disp_weq {a b : B} (aa : D a) (bb : D b) : @adjoint_equivalence E (a,,aa) (b,,bb) ≃ ∑ (f : adjoint_equivalence a b), disp_adjoint_equivalence f aa bb. Proof. unfold adjoint_equivalence, disp_adjoint_equivalence. cbn. eapply weqcomp. { apply weqinvweq. apply weqtotal2asstol. } eapply weqcomp. 2: { apply weqtotal2asstol. } eapply weqfibtototal. intros f. cbn. eapply weqcomp. 2: { apply weqtotal2comm. } eapply weqfibtototal. intros ff. apply left_adjoint_equivalence_total_disp_weq. 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.Bicategories.Core.EquivToAdjequiv. 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.AdjointUnique. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.Core.Univalence.