Suppose I have a term $a :\alpha$ of the Simply-Typed Lambda Calculus (in the following, $\alpha, \beta, \gamma$ stand for arbitrary types) and I want to lift it to a term $\lambda x_{\beta}. \;(x, \, a)$ I could use a function $\lambda z_{\alpha}, x. \;(x,\, z)$. Suppose we then form $(b, a) : \...

The bounty above should read 'I would like to know whether the example I discuss is a com-monad and why (why not).' Suppose we set $\mathbb{M} \alpha := r \to \alpha$, where $r$ is some fixed type, and $\alpha$ an arbitrary type, of the STLC (Simply-Typed Lambda Calculus) Suppose we want to defin...