- k:b'->o
- [N]:(a'->o)->o
- m:((a'->o)->o)->(b'->o)->o
- m[N]:(b'->o)->o
- m[N]k:o
- [M]:((a->b)'->o)->o = ((((a'->o)->o)->(b'->o)->o)->o)->o
- [M](\m.m[N]k):o
- [MN]:(b'->o)->o
-
-Note that even though the transform uses the same symbol for the
-translation of a variable, in general it will have a different type in
-the transformed term.
-
+ k:b'->σ
+ [N]:(a'->σ)->σ
+ m:((a'->σ)->σ)->(b'->σ)->σ
+ m[N]:(b'->σ)->σ
+ m[N]k:σ
+ [M]:((a->b)'->σ)->σ = ((((a'->σ)->σ)->(b'->σ)->σ)->σ)->σ
+ [M](\m.m[N]k):σ
+ [MN]:(b'->σ)->σ
+
+Be aware that even though the transform uses the same symbol for the
+translation of a variable (i.e., `[x] = x`), in general the variable
+in the transformed term will have a different type than in the source
+term.
+
+Excercise: what should the function ' be for the CBV xform? Hint:
+see the Meyer and Wand abstract linked above for the answer.