Definition fullsub_left_adjoint_equivalence_is_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. use make_weq. - exact (fullsub_left_adjoint_equivalence_to_bicat_left_adjoint_equivalence f). - use isweq_iso. + exact (bicat_left_adjoint_equivalence_to_fullsub_left_adjoint_equivalence f). + intros x. use subtypePath. * intro. do 2 apply isapropdirprod. ** apply fullsubbicat. ** apply fullsubbicat. ** apply isaprop_is_invertible_2cell. ** apply isaprop_is_invertible_2cell. * induction x as [a hx]. induction a as [r uc]. induction uc as [η ε]. induction r as [r x]. induction x. induction η as [η x]. induction x. induction ε as [ε x]. induction x. cbn in *. reflexivity. + intros x. use subtypePath. * intro. do 2 apply isapropdirprod ; try (apply C) ; apply isaprop_is_invertible_2cell. * reflexivity. 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.