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⊢f(x):B$
• $y:B⊢g(x):A$
• $x:A⊢{\eta }_x:{\mathrm{hom}}_A(x,g(f(x)))$
• $y:B⊢{\epsilon }_y:{\mathrm{hom}}_B(f(g(y)),y)$
• $x:A⊢{\epsilon }_{f(x)}\circ f({\eta }_x)=1_{f(x)}$
• $y:B⊢g({\epsilon }_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:A\to B$ and $g:B\to A$ and 2-cells $\eta$ and $\epsilon$ 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⊣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⊢f(x):B$
• $y:B⊢g(x):A$
• $x:A,y:B,\alpha :{\mathrm{hom}}_A(x,g(y))⊢i(\alpha ):{\mathrm{hom}}_B(f(x),y)$
• $x:A,y:B,\beta :{\mathrm{hom}}_B(f(x),y)⊢j(\beta ):{\mathrm{hom}}_A(x,g(y))$
• $x:A,y:B,\alpha :{\mathrm{hom}}_A(x,g(y))⊢\alpha =j(i(\alpha ))$
• $x:A,y:B,\beta :{\mathrm{hom}}_B(f(x),y)⊢\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

…