Definition disp_left_adjoint_equivalence_subbicat (H : ∏ (a b : B) (Ha : P₀ a) (Hb : P₀ b) (f : a --> b) (Hf : left_adjoint_equivalence f), P₁ _ _ Ha Hb f) (HB : is_univalent_2 B) {x y : B} {f : x --> y} (Hf : left_adjoint_equivalence f) {Hx : disp_subbicat x} {Hy : disp_subbicat y} (ff : Hx -->[ f ] Hy) : disp_left_adjoint_equivalence Hf ff. Proof. simple refine ((_ ,, (_ ,, _)) ,, ((_ ,, _) ,, (_ ,, _))). - refine (tt ,, _). apply H. apply inv_left_adjoint_equivalence. - exact (tt ,, tt). - exact (tt ,, tt). - abstract (apply disp_2cells_isaprop_subbicat). - abstract (apply disp_2cells_isaprop_subbicat). - abstract (apply disp_locally_groupoid_subbicat ; exact HB). - abstract (apply disp_locally_groupoid_subbicat ; exact HB). 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.Core.Unitors. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.FullSub. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat. Require Import UniMath.Bicategories.DisplayedBicats.Examples.Sigma.