proposition: Lemma adjequiv_base_adjequiv_tot {B : bicat} (HB : is_univalent_2_0 B) {D : disp_bicat B} {a b : B} : adjoint_equivalence a b → ∏ (aa : D a), ∑ (bb : D b), @adjoint_equivalence (total_bicat D) (a ,, aa) (b ,, bb).
proof: Proof. use (J_2_0 HB (λ _ _ _, _)). intros c aa. exact (aa ,, internal_adjoint_equivalence_identity _). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.Univalence