Definition disp_depprod_bicat_disp_adjequiv_weq {a : B} (aa bb : disp_depprod_bicat a) : (∏ x : I, disp_adjoint_equivalence (internal_adjoint_equivalence_identity a) (aa x) (bb x)) ≃ disp_adjoint_equivalence (internal_adjoint_equivalence_identity a) aa bb. Proof. use make_weq. - exact (disp_depprod_bicat_disp_adjequiv_map aa bb). - use isweq_iso. + exact (disp_depprod_bicat_disp_adjequiv_inv aa bb). + intros f. use funextsec. intros i. use subtypePath. { intro ; apply isaprop_disp_left_adjoint_equivalence ; [ exact HB | exact (HD_2_1 i) ]. } apply idpath. + intros f. use subtypePath. { intro ; apply isaprop_disp_left_adjoint_equivalence ; [ exact HB | exact (disp_depprod_univalent_2_1 HD_2_1) ]. } apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence.