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.
The most obvious way of describing an adjunction in the internal logic of a 2-category is via the unit-counit-triangle identities definition.
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 and and 2-cells and satisfying the triangle identities.
It is proven in
that to give an internal adjunction in a lex 2-category it is equivalent to give an isomorphism of two-sided discrete fibrations from to . With this in hand, it is easy to see that the following theory also defines an adjunction.
Note that the naturality of the isomorphism is assured automatically; the theory doesn’t have to assert it separately.