fact: Definition internal_right_adjoint {a b : B} (f : adjunction a b) : b --> a := left_adjoint_right_adjoint f.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells