If I understand correctly, the category in question can be characterized as follows: (0) For every type X in the language, there is an object X of values (not

If I understand correctly, the category in question can be characterized as follows: (0) For every type X in the language, there is an object X of values (not arbitrary terms!) of that type. (1) For every type X in the language, there is an object TX of closed programs (containing no free variables) of type X. T is the monad in question. (2) A morphism “f : X -> TY” is an arbitrary program of type Y containing a single free variable of type X. (3) (This is the part where I'm the least sure!) A morphism “f : X -> Y” is a pure terminating program containing a single free variable of type X. Also, I should've been more careful. If the language is pure and terminating, the monad in question is an equivalence of the category in question with itself. Not necessarily the identity functor.