fact: Definition fundamental_bigroupoid_1cell_adj_equiv {x y : fundamental_bigroupoid} (p : fundamental_bigroupoid⟦x,y⟧) : left_adjoint_equivalence p := equiv_to_isadjequiv p (fundamental_bigroupoid_1cell_equivalence p).
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Univalence UniMath.Bicategories.Morphisms.Adjunctions UniMath.Bicategories.Core.EquivToAdjequiv UniMath.Bicategories.Core.AdjointUnique