Definition fullsub_left_adjoint_equivalence_to_bicat_left_adjoint_equivalence {X Y : fullsubbicat} (f : X --> Y) : left_adjoint_equivalence f → @left_adjoint_equivalence C (pr1 X) (pr1 Y) (pr1 f). Proof. intros Hf. use tpair. - use tpair. + exact (pr1 (left_adjoint_right_adjoint Hf)). + split. * exact (pr1 (left_adjoint_unit Hf)). * exact (pr1 (left_adjoint_counit Hf)). - split ; split. + exact (base_paths _ _ (internal_triangle1 Hf)). + exact (base_paths _ _ (internal_triangle2 Hf)). + cbn. apply (fullsub_is_invertible_2cell_to_bicat_is_invertible_2cell (left_adjoint_unit (pr1 Hf))). apply Hf. + cbn. apply (fullsub_is_invertible_2cell_to_bicat_is_invertible_2cell (left_adjoint_counit (pr1 Hf))). 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.