fact: 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.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Isos UniMath.CategoryTheory.DisplayedCats.Fibrations UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Fiber UniMath.CategoryTheory.DisplayedCats.Univalence UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Core.Examples.BicatOfUnivCats UniMath.Bicategories.Core.Examples.FibSlice UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.PseudoFunctors.PseudoFunctor UniMath.Bicategories.PseudoFunctors.Examples.Identity UniMath.Bicategories.PseudoFunctors.Examples.Composition UniMath.Bicategories.Transformations.PseudoTransformation UniMath.Bicategories.PseudoFunctors.Biequivalence UniMath.Bicategories.Grothendieck.Biequivalence