Definition bicat_left_adjoint_equivalence_to_fullsub_left_adjoint_equivalence {X Y : fullsubbicat} (f : X --> Y) : @left_adjoint_equivalence C (pr1 X) (pr1 Y) (pr1 f) → left_adjoint_equivalence f. Proof. intros Hf. use tpair. - use tpair. + exact (left_adjoint_right_adjoint Hf ,, tt). + split. * exact (left_adjoint_unit Hf ,, tt). * exact (left_adjoint_counit Hf ,, tt). - split ; split. + use subtypePath. * intro ; apply isapropunit. * exact (internal_triangle1 Hf). + use subtypePath. * intro ; apply isapropunit. * exact (internal_triangle2 Hf). + apply bicat_is_invertible_2cell_to_fullsub_is_invertible_2cell. apply Hf. + apply bicat_is_invertible_2cell_to_fullsub_is_invertible_2cell. apply Hf. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.Initial. Require Import UniMath.Bicategories.Core.Examples.Final. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Import DispBicat.Notations. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.DisplayedBicats.DispInvertibles. Require Import UniMath.Bicategories.DisplayedBicats.DispAdjunctions. Require Import UniMath.Bicategories.DisplayedBicats.DispUnivalence. Require Import UniMath.Bicategories.DisplayedBicats.Examples.DisplayedCatToBicat.