Our goal here is to show that all the equivalent ways of defining an adjunction in ordinary naive category theory are still valid in the internal logic of a 2-category, and all produce the usual internal notion of adjunction in a 2-category.

It is evident that a model of this theory in any lex 2-category is precisely an internal adjunction in the usual sense, consisting of two 1-cells $f\colon A\to B$ and $g\colon B\to A$ and 2-cells $\eta$ and $\varepsilon$ satisfying the triangle identities.

Bijection on hom-sets

It is proven in

Street, Fibrations and Yoneda’s lemma in a 2-category

that to give an internal adjunction $f\dashv g$ in a lex 2-category it is equivalent to give an isomorphism $(f/B) \cong (A/g)$ of two-sided discrete fibrations from $B$ to $A$. With this in hand, it is easy to see that the following theory also defines an adjunction.