very nice stuff!
Marco Perone
1

Ah, but remember that X³ and X are types, not values. If X is one-dimensional, then L(X³, X) is something like the dimension of the space of values of the type X³. But at the type level, it’s just a count of how many X-shaped spaces there are in X³.