$ v \rightarrow \textless v , o \textgreater$

This just seems ... wrong to me. I prefer because of its possibility to handle more complex ideas:

$ \lambda v. \lambda x. \textless v, x \textgreater $

More commonplace is to see this definition of the tensor product:

$ \tau \oplus \theta(v,w) = (\tau v) (\theta w) $

where i feel more comfortable writing in my notes:

$\oplus = \lambda \tau, \theta. (\lambda v, w. (\tau w) (\theta w)) $

Truth be told, I would write both, but trust the lambda notation more. The ideas are defined much more concretely. For pullbacks:

$ F* = \lambda p. p \circ f $

Then of course we have an easy way to talk about the function that makes a pullback:

$ \lambda f. \lambda p. p \circ f $

Iono, maybe Im crazy for mixing different notation like this, but it makes things clear to me.

This all ties back with earlier content in this blog -- Good notation concerns me alot. The symbols used for math reflect the content of the framework we are working in and can be seen as agents of them. Not only do concretely defined notations that are intuitive make learning and recording content easier, they may as I have argued free us from unintended psycholinguistic effects.

This all ties back with earlier content in this blog -- Good notation concerns me alot. The symbols used for math reflect the content of the framework we are working in and can be seen as agents of them. Not only do concretely defined notations that are intuitive make learning and recording content easier, they may as I have argued free us from unintended psycholinguistic effects.