Definition 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) {x y : subbicat} (f : x --> y) (Hf : left_adjoint_equivalence (B := B) (pr1 f)) : left_adjoint_equivalence f. Proof. use equiv_to_adjequiv. simple refine ((_ ,, (_ ,, _)) ,, _ ,, _). - refine (left_adjoint_right_adjoint Hf ,, tt ,, _). apply H. apply inv_left_adjoint_equivalence. - exact (left_adjoint_unit Hf ,, tt ,, tt). - exact (left_adjoint_counit Hf ,, tt ,, tt). - use is_invertible_2cell_subbicat. exact (property_from_invertible_2cell (left_equivalence_unit_iso Hf)). - use is_invertible_2cell_subbicat. exact (property_from_invertible_2cell (left_equivalence_counit_iso Hf)). 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.