$\require{AMScd}$ Note: I have already seen this question, which asks about a specific aspect of the construction – here I am trying to construct this functor and failing at a very different stage.
We are trying to show that the two functors $\sf Id:FDVec_k\to FDVec_k$ and $(\cdot)^{\vee\vee}:\sf FDVec_k\to FDVec_k$ are naturally isomorphic. I've never seen such an argument before, and working through the linear algebra is giving me some problems.
An element of $V^{\vee\vee}$ is defined to be a linear map from $V^{\vee}$ to $k$, so it takes linear maps $V\to k$ to elements of $k$. For a natural isomorphism we need isomorphisms $$m_V:V\to V^{\vee\vee}.$$ We input a vector and output a map $\operatorname{Hom}(V,k)\to k$: $$m_V(v)(f:V\to k)=f(v)\in k.$$ We then need to show that diagrams $$
\begin{CD}
V @>\phi>> W\\
@V{m_V}VV @VV{m_W}V\\
V^{\vee\vee} @>>\phi^{\vee\vee}> W^{\vee\vee}
\end{CD}
$$
commute if $\phi$ is a linear map of finite-dimensional vector spaces, so $$m_W\circ\phi=\phi^{\vee\vee}\circ m_V.$$
However, my problem ultimately ends up being that I can't interpret $\phi^{\vee\vee}$ sufficiently well. It should take linear maps $\operatorname{Hom}(V,k)\to k$ to linear maps $\operatorname{Hom}(W,k)\to k$ in a way that is somehow induced by $\phi$, but I'm not sure what this way is. My attempt:
$$[\phi^{\vee\vee}(f:V^{\vee}\to k)](g:W\to k)\in k$$
but I get no further than this. I ask purely for clarification as to what a double dual map really is (the several layers of abstraction present in the problem are quite hard for my beginner's mind to handle).
Best Answer
You only need to understand what the first dual map $\phi^\vee$ is, as $(\phi^\vee)^\vee=\phi^{\vee\vee}$. The map $\phi^\vee$ is defined by $\phi^\vee(f)=f\circ\phi$. This is just a special case of the contravariant hom functor. To check that the diagram is commutative, notice that for $v\in V$ and $f\in W^\vee$ we have $$(\phi^{\vee\vee}\circ m_V)(v)(f)=(\phi^{\vee\vee}(m_V(v))(f)=(m_V(v)\circ\phi^\vee)(f) \\ =m_V(v)(f\circ\phi)=f(\phi(v))=m_W(\phi(v))(f).$$