Definition disp_depprod_bicat_disp_adjequiv_map {a : B} (aa bb : disp_depprod_bicat a) : (∏ (i : I), disp_adjoint_equivalence (internal_adjoint_equivalence_identity a) (aa i) (bb i)) → disp_adjoint_equivalence (internal_adjoint_equivalence_identity a) aa bb. Proof. intros f. use tpair. - exact (λ i, f i). - use tpair. + use tpair. * exact (λ i, disp_left_adjoint_right_adjoint _ (f i)). * split. ** exact (λ i, disp_left_adjoint_unit _ (f i)). ** exact (λ i, disp_left_adjoint_counit _ (f i)). + split. * split. ** abstract (use funextsec ; intro i ; refine (pr1 (pr122 (f i)) @ _) ; refine ((disp_depprod_prebicat_laws_help _ _ _))). ** abstract (use funextsec ; intro i ; refine (pr2 (pr122 (f i)) @ _) ; refine ((disp_depprod_prebicat_laws_help _ _ _))). * split. ** apply disp_depprod_bicat_disp_is_invertible_2cell_map. exact (λ i, pr1 (pr222 (f i))). ** apply disp_depprod_bicat_disp_is_invertible_2cell_map. exact (λ i, pr2 (pr222 (f i))). 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.