Definition all_invertible_2cell_is_disp_adjoint_equivalence (HD_2_1 : is_univalent_2_1 D) (F₀ : ps_base C D) (F₁ F₁' : map1cells_disp_bicat F₀) : (∏ (X Y : C) (f : X --> Y), invertible_2cell (F₁ X Y f) (F₁' X Y f)) ≃ disp_adjoint_equivalence (internal_adjoint_equivalence_identity F₀) F₁ F₁'. Proof. refine (make_weq (all_invertible_2cell_to_disp_adjoint_equivalence F₀ F₁ F₁') _). use isweq_iso. - exact (disp_adjoint_equivalence_to_all_invertible_2cell F₀ F₁ F₁'). - intro m. apply funextsec ; intro X. apply funextsec ; intro Y. apply funextsec ; intro f. apply subtypePath. { intro ; apply isaprop_is_invertible_2cell. } cbn. rewrite !vassocr. rewrite rinvunitor_runitor, id2_left. rewrite !vassocl. rewrite linvunitor_lunitor, id2_right. reflexivity. - intro m. use subtypePath. { intro. apply isaprop_disp_left_adjoint_equivalence. + exact (ps_base_is_univalent_2_1 _ _ HD_2_1). + apply map1cells_disp_univalent_2_1. } apply funextsec ; intro X. apply funextsec ; intro Y. apply funextsec ; intro f. apply subtypePath. { intro ; apply isaprop_is_invertible_2cell. } cbn. rewrite !vassocr. rewrite lunitor_linvunitor, id2_left. rewrite !vassocl. rewrite runitor_rinvunitor, id2_right. reflexivity. 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.CategoryTheory.DisplayedCats.Core. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Display.Base. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence.