Lemma left_adjoint_equivalence_total_disp_weq {a b : B} {aa : D a} {bb : D b} (f : a --> b) (ff : aa -->[f] bb) : @left_adjoint_equivalence E (a,,aa) (b,,bb) (f,,ff) ≃ ∑ (αe : left_adjoint_equivalence f), disp_left_adjoint_equivalence αe ff. Proof. unfold left_adjoint_equivalence. cbn. eapply weqcomp. { pose (Q:= λ (w : (∑ αd, disp_left_adjoint_data αd ff)), (∑ l, disp_left_adjoint_axioms (pr1 w,,l) (pr2 w)) × (∑ l, disp_left_equivalence_axioms (pr1 w,,l) (pr2 w))). eapply (weqbandf (left_adjoint_data_total_weq ff) _ Q). intros td. unfold Q; cbn. apply weqdirprodf. - apply left_adjoint_axioms_total_weq. - apply left_equivalence_axioms_total_weq. } cbn. cbn. eapply weqcomp. { apply weqinvweq. apply weqtotal2asstol. } cbn. eapply weqcomp. 2: { apply weqtotal2asstol. } cbn. eapply weqfibtototal. intros αd. unfold disp_left_adjoint_equivalence. cbn. eapply weqcomp. 2: { apply weqtotal2comm. } cbn. eapply weqfibtototal. intros ααd. cbn. eapply weqcomp. 2: { apply weqtotal2asstol. } cbn. eapply weqcomp. { apply weqinvweq. apply weqtotal2asstol. } cbn. eapply weqfibtototal. intros αa. cbn. eapply weqcomp. { apply weqtotal2comm. } 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.