Is the category of finite dimensional vector spaces isomorphic to the category of double duals of them? I am studying the category theory and I have a question about it.
Let $\mathcal{V}_k$ be the category of all finite dimensional $k$-vector spaces and $\mathcal{V}_k^{**}$ be the category of all double duals for all finite dimensional $k$-vector spaces. Since we know that the double dual functor is naturally equivalent to the identity functor, we can deduce that $\mathcal{V}_k^{**}$ is equivalent to $\mathcal{V}_k$.
And I think that $\mathcal{V}_k$ and $\mathcal{V}_k^{**}$ are not isomorphic. But I can't prove it directly since there is no equipment to determine it. Is my intuition correct?
 A: For most if not all reasonable set-theoretic constructions of these categories, the double dual functor $\mathcal{V}_k\to\mathcal{V}^{**}_k$ should be an isomorphism.  Here is one such way to do the set-theoretic constructions.  An object of $\mathcal{V}_k$ is an ordered triple $(V,+_V,\cdot_V)$ where $V$ is a set, $+_V:V\times V\to V$ is a map, and $\cdot_V:k\times V\to V$ is a map, satisfying certain axioms.  The dual of such an object is a certain ordered triple $(V^*, +_{V^*},\cdot_{V^*})$, where $V^*$ is the set of maps $V\to k$ which are linear.  The category $\mathcal{V}^{**}_k$ is the full subcategory of $\mathcal{V}_k$ consisting of objects which are obtained from an object $(V,+_V,\cdot_V)$ by applying the dual construction twice.
In particular, given an object $(W,+_W,\cdot_W)$ of $\mathcal{V}^{**}_k$, there is a unique object $(V,+_V,\cdot_V)$ of $\mathcal{V}_k$ that it is the double dual of: each element of the set $W$ is a function whose domain is a certain set $V'$, and then every element of $V'$ is a function whose domain is $V$.  The operations $+_V$ and $\cdot_V$ are then uniquely determined by the set $V'$ (exercise: the operations on a vector space $V$ are determined by the set of maps $V\to k$ which are linear).
It follows that the double dual functor $\mathcal{V}_k\to \mathcal{V}^{**}_k$ is bijective on objects, and so since it is an equivalence, it is actually an isomorphism.
More generally (assuming an appropriate version of the axiom of choice), an equivalence $F:\mathcal{C}\to\mathcal{D}$ between two categories is naturally isomorphic to an isomorphism iff for each object $C$ of $\mathcal{C}$, the cardinality of the isomorphism class of $C$ is equal to the cardinality of the isomorphism class of $F(C)$.  For in that case we can choose bijections between all the corresponding isomorphism classes, as well as isomorphisms from each object to a chosen representative of its isomorphism class, and use these to construct an isomorphism.  In most "natural" cases of large categories (including the ones considered above), all the isomorphism classes (except possibly the isomorphism class of an "empty" object) are proper classes, and (assuming global choice) any two proper classes are in bijection, so any equivalence can be turned into an isomorphism.
