Lemma isaprop_disp_left_adjoint_equivalence {C : bicat} {D : disp_bicat C} {a b : C} {aa : D a} {bb : D b} {f : a --> b} (Hf : left_adjoint_equivalence f) (ff : aa -->[f] bb) : is_univalent_2_1 C → disp_univalent_2_1 D → isaprop (disp_left_adjoint_equivalence Hf ff). Proof. intros HUC HUD. revert Hf. apply hlevel_total2. 2: { apply hlevelntosn. apply isaprop_left_adjoint_equivalence. assumption. } eapply isofhlevelweqf. { apply left_adjoint_equivalence_total_disp_weq. } apply isaprop_left_adjoint_equivalence. apply total_is_univalent_2_1; assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations.