Lemma adjunction_total_disp_weq {a b : B} (aa : D a) (bb : D b) : @adjunction E (a,,aa) (b,,bb) ≃ ∑ (f : adjunction a b), disp_adjunction f aa bb. Proof. unfold adjunction. cbn. eapply weqcomp. { apply weqinvweq. apply weqtotal2asstol. } eapply weqcomp. 2: { apply weqtotal2asstol. } eapply weqfibtototal. intros f. unfold disp_adjunction. cbn. eapply weqcomp. 2: { apply weqtotal2comm. } eapply weqfibtototal. intros ff. unfold left_adjoint. eapply weqcomp. { pose (Q:=λ (w : (∑ αd, disp_left_adjoint_data αd ff)), (∑ l, disp_left_adjoint_axioms (pr1 w,,l) (pr2 w))). eapply (weqbandf (left_adjoint_data_total_weq ff) _ Q). intros td. unfold Q; cbn. apply left_adjoint_axioms_total_weq. } cbn. eapply weqcomp. { apply weqinvweq. apply weqtotal2asstol. } cbn. eapply weqcomp. 2: { apply weqtotal2asstol. } cbn. eapply weqfibtototal. intros αd. eapply weqcomp. { apply weqtotal2comm. } cbn. apply idweq. 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.