nLab walking adjoint equivalence

Idea

The walking adjoint equivalence (as in “walking structure”) or free-standing adjoint equivalence is the 2-category (in fact a (2,1)-category) which ‘represents’ adjoint equivalences in a 2-category. It is a categorification of the free-standing adjoint isomorphism?.

Definition

Definition

The free-standing adjoint equivalence is the unique (up to isomorphism) 2-category $\mathcal{AE}$ with exactly two objects $0$ and $1$, 1-morphisms freely generated by an arrow $i: 0 \rightarrow 1$, and an arrow $j: 1 \rightarrow 0$, and 2-morphisms generated by 2-isomorphisms $\iota_{0}: j \circ i \cong id(0)$ and $\iota_{1}: i \circ j \cong id(1)$, subject to the equalities

$$id(i) = (\iota_1 i)\circ (i \iota_0^{-1}), id(j) =(\iota_0^{-1} j) \circ (j \iota_1)$$

Remark

The arrow $i: 0 \rightarrow 1$ is an adjoint equivalence.

Remark

The free-standing adjoint equivalence is a (2,1)-category.

Representing of adjoint equivalences

$\mathcal{AE}$ is the model for all adjoint equivalences in all 2-categories. In other words, any adjoint equivalence in a 2-category $\mathcal{A}$ is just a 2-functor from $\mathcal{AE}$:

Proposition

Let $\mathcal{C}$ be a 2-category (weak or strict). Let $f$ be a 1-arrow of $\mathcal{C}$ which is part of an adjoint equivalence. Then there is a 2-functor $F: \mathcal{AE} \rightarrow \mathcal{C}$ such that the arrow $i:0 \rightarrow 1$ of $\mathcal{I}$ maps under $F$ to $f$.

Proof

Immediate from the definitions.

Related entries

• Adj

• walking structure

  • the boolean domain $2 \coloneqq \partial \Delta^1$; i.e. the walking pair of objects

  • the directed interval category $I \coloneqq \Delta^1$; i.e. the walking morphism

  • the (2,0)-horn category $\Lambda_0^2$; i.e. the walking cospan

  • the (2,1)-horn category $\Lambda_1^2$; i.e. the walking composable pair

  • the (2,2)-horn category $\Lambda_2^2$; i.e. the walking span

  • the 2-simplex category $\Delta^2$; i.e. the walking commutative triangle

  • the walking parallel pair

  • the walking isomorphism

  • Adj; i.e. the walking adjunction

  • the walking equivalence

  • the walking adjoint equivalence

  • the walking 2-isomorphism with trivial boundary

  • the syntactic category of a theory $T$; i.e. the walking $T$-model

• In dependent type theory, many higher inductive types can be considered to be walking structures:

  • the unit type is the walking element

  • the boolean type is the walking pair of elements

  • the interval type is the walking identification

  • one definition of the circle type is the walking self-identification

  • another definition of the circle type is the walking parallel pair of identifications.

  • the suspension type of a type $I$ is the walking parallel $I$-indexed family of identifications.

  • the natural numbers type is the walking sequence

  • the integers type is the walking bi-infinite sequence

  • the walking bridge

  • the directed interval type is the walking morphism in the sense of element of a hom type