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:Af(x):Bx:A \vdash f(x):B
  • y:Bg(x):Ay:B \vdash g(x):A
  • x:Aη x:hom A(x,g(f(x)))x:A \vdash \eta_x:hom_A(x,g(f(x)))
  • y:Bε y:hom B(f(g(y)),y)y:B \vdash \varepsilon_y:hom_B(f(g(y)),y)
  • x:Aε f(x)f(η x)=1 f(x)x:A \vdash \varepsilon_{f(x)} \circ f(\eta_x) = 1_{f(x)}
  • y:Bg(ε y)η g(y)=1 g(y)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:ABf\colon A\to B and g:BAg\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 fgf\dashv g in a lex 2-category it is equivalent to give an isomorphism (f/B)(A/g)(f/B) \cong (A/g) of two-sided discrete fibrations from BB to AA. With this in hand, it is easy to see that the following theory also defines an adjunction.

  • x:Af(x):Bx:A \vdash f(x):B
  • y:Bg(x):Ay:B \vdash g(x):A
  • x:A,y:B,α:hom A(x,g(y))i(α):hom B(f(x),y)x:A, y:B, \alpha :hom_A(x,g(y)) \vdash i(\alpha) : hom_B(f(x),y)
  • x:A,y:B,β:hom B(f(x),y)j(β):hom A(x,g(y))x:A, y:B, \beta :hom_B(f(x),y) \vdash j(\beta) : hom_A(x,g(y))
  • x:A,y:B,α:hom A(x,g(y))α=j(i(α))x:A, y:B, \alpha :hom_A(x,g(y)) \vdash \alpha = j(i(\alpha))
  • x:A,y:B,β:hom B(f(x),y)β=i(j(β))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

Created on March 26, 2010 at 04:29:27. See the history of this page for a list of all contributions to it.