SeriesCategory Theory for AIPart 2
What Happens to Currying When Beta and Eta Become Computations?
A worked path through Seely's 2-categorical lambda calculus: from one term with two beta reductions to interchange, laxity, and the adjunction between currying and uncurrying.
Fix a type $O$, a closed function $f:O\Rightarrow O$, and one free input $y:O$. Consider the term $$ T(y) = (\lambda u:O.\,u) \big((\lambda v:O.\,v)(f\,y)\big). $$ It contains two beta redexes. We can contract the outer one first, $$ T(y) \...