Michael Shulman adjunctions in 2-logic

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.

Unit + Counit + Triangle identities

The most obvious way of describing an adjunction in the internal logic of a 2-category is via the unit-counit-triangle identities definition.

• $x:A \vdash f(x):B$
• $y:B \vdash g(x):A$
• $x:A \vdash \eta_x:hom_A(x,g(f(x)))$
• $y:B \vdash \varepsilon_y:hom_B(f(g(y)),y)$
• $x:A \vdash \varepsilon_{f(x)} \circ f(\eta_x) = 1_{f(x)}$
• $y:B \vdash g(\varepsilon_{y}) \circ \eta_{g(y)} = 1_{g(y)}$

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.

• $x:A \vdash f(x):B$
• $y:B \vdash g(x):A$
• $x:A, y:B, \alpha :hom_A(x,g(y)) \vdash i(\alpha) : hom_B(f(x),y)$
• $x:A, y:B, \beta :hom_B(f(x),y) \vdash j(\beta) : hom_A(x,g(y))$
• $x:A, y:B, \alpha :hom_A(x,g(y)) \vdash \alpha = j(i(\alpha))$
• $x:A, y:B, \beta :hom_B(f(x),y) \vdash \beta = i(j(\beta))$

Note that the naturality of the isomorphism is assured automatically; the theory doesn’t have to assert it separately.

Universal arrows

…