Definition ff_and_eso_to_adjequiv {C : univalent_category} {P₁ P₂ : fib_slice_bicat C} (F : P₁ --> P₂) (F_full : ∏ (x : C), full (fiber_functor (pr1 F) x)) (F_faithful : ∏ (x : C), faithful (fiber_functor (pr1 F) x)) (F_eso : ∏ (x : C), Functors.essentially_surjective (fiber_functor (pr1 F) x)) : left_adjoint_equivalence F. Proof. use fiberwise_equiv_to_adjequiv. intro x. use rad_equivalence_of_cats. - use is_univalent_fiber. apply (pr1 P₁). - use full_and_faithful_implies_fully_faithful. split. + exact (F_full x). + exact (F_faithful x). - exact (F_eso x). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Equivalences.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Fiber. Require Import UniMath.CategoryTheory.DisplayedCats.Univalence. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.Core.Examples.FibSlice. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.PseudoFunctors.PseudoFunctor. Import PseudoFunctor.Notations. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Identity. Require Import UniMath.Bicategories.PseudoFunctors.Examples.Composition. Require Import UniMath.Bicategories.Transformations.PseudoTransformation. Require Import UniMath.Bicategories.PseudoFunctors.Biequivalence. Require Import UniMath.Bicategories.Grothendieck.Biequivalence.