That's close but not quite how I meant for the notation to be interpreted: f is an argument to an anonymous function. Maybe clearer is swap = f ↦ ((x, y) ↦ f(

That's close but not quite how I meant for the notation to be interpreted: f is an argument to an anonymous function. Maybe clearer is swap = f ↦ ((x, y) ↦ f(y, x)) The rule this satisfies is swap(f)(x, y) = f(y, x) and the type for swap is swap : (X × Y → Z) → (Y × X → Z) for some types/sets X, Y, and Z. (Also, note that tuples might not be anything like a vector space. For example, for String × [Int], you wouldn't usually write ("hi", [2,3]) as "hi"𝑒₁ + [2,3]𝑒₂ since there's not really a good commutative addition operation for strings or lists.)