Fix a field. Given a vector space $V$ it has a dual $V^\ast$, which has its own dual $V^{\ast \ast}$, which has its own dual $V^{\ast \ast \ast}$, and so on *ad infinitum*. There are lots of natural maps between these iterated duals. Most famous is the map $$ i_V \colon V \to V^{\ast \ast} $$ given by $$ i_V(v)(f) = f(v) \quad \forall v \in V, f \in V^\ast $$ but there are many others. For example, we have the map $$ i_{V^{\ast }} \colon V^{\ast } \to V^{\ast \ast \ast } $$ but we also have the map $$ i_{V}^\ast \colon V^{\ast \ast \ast } \to V^{\ast}$$ formed by taking the adjoint of $$ i_{V} \colon V \to V^{\ast \ast}. $$ And we have various equations between these maps. For example, I believe $i_{V}^\ast$ is a left inverse of $i_{V^{\ast}}$: $$ i_{V}^\ast \circ i_{V^{\ast}} = 1. $$ So it's natural to want to get to the bottom of this and ask what are *all* the natural maps between iterated duals, and *all* the equations involving these maps. To formalize this it's good to treat duality as a pair of contravariant functors $$ D \colon \mathrm{Vect} \to \mathrm{Vect}^{\rm op}$$ $$ E \colon \mathrm{Vect}^{\rm op} \to \mathrm{Vect}.$$ These are really the same functor in two disguises: namely, the contravariant functor that sends any vector space $V$ to its dual $V^\ast$, and any linear map $f\colon V \to W$ to its adjoint $f^{\ast} \colon W^\ast \to V^\ast$. Treating them as two separate functors makes it a bit easier to make sense of the fact that they are adjoint functors and thus [they define a monad](https://mathoverflow.net/questions/396182/the-bidualizing-monad) and also a comonad. A bunch of natural transformations between the powers of $$ \begin{array}{cccc} E \circ D \colon & \mathrm{Vect} &\to& \mathrm{Vect} \\ & V &\mapsto& V^{\ast \ast} \end{array} $$ and also a bunch of equations between these natural transformations, arise from the adjunction between $D$ and $E$. So, one can ask if *all* the natural transformations between the powers of $E \circ D$, and *all* the equations between these, arise from this adjunction. To give this conjecture a chance to be true, we need to interpret 'arise from' broadly enough. For example, a linear combination of natural transformations will again be a natural transformation. So, to have a chance of getting all the natural transformations, we need to start with the unit and counit of the adjunction, and build other natural transformations from these, and the functors $D$ and $E$, by taking all composites (in the 2-categorical sense), and also linear combinations. Then we can ask whether the resulting natural transformations are *all* the natural transformations between powers of $E \circ D$. We can also ask whether all equations between these natural transformations follow from the usual 'zig-zag equations' governing the unit and counit of an adjunction... where 'follow' needs to be made more precise. The slickest way to formulate the question may use a bit of 2-category theory. There is a 2-category $\mathbf{Adj}$ called the '[walking adjunction][1]', such that an adjunction in $\mathbf{Cat}$ is the same as a 2-functor from $\mathbf{Adj}$ to $\mathbf{Cat}$. The adjunction between $D$ and $E$ thus gives a particular 2-functor $$F \colon \mathbf{Adj} \to \mathbf{Cat}$$ and we can express *part* of my question as a question about this 2-functor. For example, we can ask **Question 1.** Is $F \colon \mathbf{Adj} \to \mathbf{Cat}$ **locally faithful**, meaning faithful on each hom-category? If it's not, there are additional equations involving the unit and counit of the adjunction between $D$ and $E$, that don't hold in a general adjunction. To ask whether we've found all the natural maps between iterated duals of vector spaces, we might ask if $F$ is **locally full**, meaning full on each hom-category. But we already know it's not, due the linearity issue I mentioned! So it's good to follow Peter LeFanu Lumsdaine's suggestions and work instead with something like $\mathbf{Adj}_k$, the walking additive $k$-linear adjunction. This is a locally additive $k$-linear 2-category such that a 2-functor into $\mathbf{Cat}_k$, the 2-category of additive $k$-linear categories, is the same as an adjunction in $\mathbf{Cat}_k$. The adjunction between $D$ and $E$ thus gives a particular 2-functor $$F_k \colon \mathbf{Adj}_k \to \mathbf{Cat}_k$$ and we can attempt to formulate my whole question as follows: **Question 2.** Is $F_k \colon \mathbf{Adj}_k \to \mathbf{Cat}_k$ locally full and locally faithful? I should add that the story feels different if we restrict to finite-dimensional vector spaces, because then $i_V \colon V \to V^{\ast \ast}$ is an isomorphism. I *don't* want to restrict to finite-dimensional vector spaces. [1]: https://ncatlab.org/nlab/show/Adj