fact: Definition idoiso_2_0_onetypes (X Y : one_types) : X = Y ≃ adjoint_equivalence X Y := (adjequiv_to_weq X Y ∘ UA_for_HLevels 3 X Y)%weq.
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