Yes for finite-dimensional spaces. For infinite-dimensional spaces you can think of 1-forms as generalizations of a partially-applied dot product (eg. the Dirac

Yes for finite-dimensional spaces. For infinite-dimensional spaces you can think of 1-forms as generalizations of a partially-applied dot product (eg. the Dirac delta function). You are asking if every covector f can be written as dot(v,—) for some v. This is true for finite-dimensional spaces (take v = f(e1)e1 + ... + f(en)en, where e1,...,en is a orthogonal basis for dot). Since v is unique, this gives an isomorphism between V and V٭ and applying the same argument to V٭ and V٭٭, those are isomorphic, so V and V٭٭ are also isomorphic. But the isomorphism depends on the choice of dot. However the map V -> V٭٭ does not depend on the choice of dot. The type is V -> (V->F) -> F so this is just (reversed) function application. You can easily show this is injective. Furthermore when V is finite-dimensional, we know from above that dim(V)=dim(V٭)=dim(V٭٭), so we know in this case it is also an iso.