I was recently talking vector spaces with someone with a thorough grasp on functional theory and its notation. We came to a point of confusion which I think in retrospect stemmed from a natural isomorphism that I, and most mathematicians, take as an identity. The isomorphism is between a finite dimensional vector space and the dual of its dual.

In type theory (x⨯y) is the Cartesian product and (x → y) is the set of functions from set x to set y. This set of functions from x to y is written yx is some math contexts. The arrow notation is used in mathematical type theory and much modern computer science. We use the arrow notation here but always with some linearity limmitation.

Let V be some vector space over some field F. In that page we give no name for the vector space or the field. In this annex we call them V and F respectively. The Latin letters range over V and the Greek over F.

Both field operators + and * can be typed as F⨯F → F. (The * is actually omitted in the equations!)
The new operators + and * can be typed as V⨯V → V and F⨯V → V respectively.
It should be remarked that deducing the type of an expression happens in the same order as evaluation, from subexpression to expression. This always suffices to figure out which operation the overloaded + or * refers to.

We omit universal quantifiers conventionally. Each of the axioms, except the first, should have enough of them prepended to cover all the letters in the axiom.

In the section “Functions as vector space” we have some arbitrary set D as the domain. We introduce a new vector space by defining + and * where (D → V) serves in place of V.

In the section “Linear Operators” for a vector space V, we introduce V* which is the dual vector space to V as (V → F), qualified by linearity, by defining + and * again. It is straight forward and confusing to go on to the dual of the dual V** of V: ((V → F) → F). For any x ∊ V we can point to a unique x' in V** with the property that:
for all k in V*, k(x) = x'(k).

Note that it is not necessary to refer to some coördinate system to connect x and x'. There is no such unique and ‘natural’ connection between the members of V and V*. This forms the unique natural isomorphism between V and V** and inspired the term “dual”. I and many mathematicians confuse a vector space and its double dual. In many contexts either k(x) or x'(k) are written xk. Dirac was onto this with his notation ⟨k|x⟩. The type of this new operation is (V* ⨯ V) → F. It is symmetric for many fields. For the complex field xk is the complex conjugate of kx.