Simply typed lambda calculus in one type variable in a Cartesian closed category $\mathbf{C}$ can be interpreted as a family of Cartesian closed functors (described below, do they have a name?) from the Cartesian closed category $\mathbf{STLC_1}$ of simply typed lambda calculus signatures with products with one type variable and all terms between them (also described below and does this category have a name?). I will loosely prove that when these functors are endofunctors, they are not monads, and if they were, $\mathbf{STLC_1}$ would be strong enough to interpret untyped lambda calculus. My question is if there is some other category, similar to $\mathbf{STLC_1}$ where the (similar) family of endofunctors are monads, so that untyped lambda calculus can be interpreted in that category.

The objects $s$ of $\mathbf{STLC_1}$ are defined recursively as

$$s \leftarrow a$$ $$s \leftarrow s_1 \times s_2$$ $$s \leftarrow s_2^{s_1}$$

where $a$ denotes the single generator of the lambda calculus, $\times$ denotes categorical product and superscript denotes exponentials in $\mathbf{STLC_1}$.

According to the well known functorial interpretation of simply typed lambda calculus, each pair of signatures $s_1, s_2 \in \mathbf{STLC_1}$ and each term $t : s_1 \to s_2$ corresponds to a pair of functors $F_1, F_2 \in \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{C}$ and a dinatural transformation between them, typically depicted as a commuting hexagon.

This can be turned into a functor $\operatorname{I} : \mathbf{STLC_1} \times \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{C}$. For each pair of objects $a, b \in \mathbf{C}$, each arrow $f : b \to a$, each pair of signatures $s_1, s_2 \in \mathbf{STLC_1}$ and each term $t : s_1 \to s_2$, the functor indicates a commuting hexagon in $\mathbf{C}$. With a little imagination (or some kind hearted editor who masters the LaTeX array environment) it can be depicted:

$$ \operatorname{I}\ s_1\ a\ b \stackrel{\operatorname{I} s_1\ f\ b}{\to} \operatorname{I}\ s_1\ b\ b \stackrel{\operatorname{I}\ t\ b\ b}{\to} \operatorname{I}\ s_2\ b\ b \stackrel{\operatorname{I}\ s_2\ b\ f}{\to} \operatorname{I}\ s_2\ b\ a $$

$$ \operatorname{I}\ s_1\ a\ b \stackrel{\operatorname{I}\ s_1\ a\ f}{\to} \operatorname{I}\ s_1\ a\ a \stackrel{\operatorname{I}\ t\ a\ a}{\to} \operatorname{I}\ s_2\ a\ a \stackrel{\operatorname{I}\ s_2\ f\ a}{\to} \operatorname{I}\ s_2\ b\ a $$

Objects in a position where an arrow is expected denotes the identity morphism of that object, e. g. $\operatorname{I}\ s_1\ f\ b = \operatorname{I}\ id_{s_1}\ f\ id_b$. If we set $b = a$ and $f = id_a$, the hexagon is collapsed into two objects $a_{s_1} = \operatorname{I}\ a\ a\ s_1$ and $a_{s_2} = \operatorname{I}\ a\ a\ s_2$ an arrow $f_{a, t} = \operatorname{I}\ t\ a\ a : (\operatorname{I}\ s_2\ a\ a) \to (\operatorname{I}\ s_2 \ a\ a)$. For each choice of $a$ in this way, we get a Cartesian closed functor functor $\operatorname{T_a} \in \mathbf{STLC_1} \to \mathbf{C}$.

Since $\mathbf{STLC_1}$ is also Cartesian closed, each signature $s$ can be used to indicate an endofunctor $\operatorname{T_s} \in \mathbf{STLC_1}\to \mathbf{STLC_1}$. Capital $\operatorname{T}$ is usually reserved for endofunctors that are monads, but the functors $\operatorname{T_s}$ are not, or at least not in general. The existence of such a family of monads would imply $\mathbf{STLC_1}$ would be strong enough to interpret untyped lambda calculus. Since the Cartesian closed category $\mathbf{C}$ by definition has all the structure of $\mathbf{STLC_1}$, such monads would imply $\mathbf{C}$, in general, could also implement untyped lambda calculus (I think). Since this is clearly not the case, the endofunctors $\operatorname{T_s}& are not monads (I think).

For any signatures $s_1, s_2 \in \mathbf{STLC_1}$ and any two terms $t_1 : s_2^{s_1}$, $t_2 : s_1$, the universal arrow $eval_{s_1, s_2} : (s_2^{s_1} \times s_1) \to s_2$ of exponentiation in $\mathbf{STLC_1}$ evaluates application of terms. It is the uncurried version of the identity function $id_{s_1, s_2}: (s_1 \to s_2) \to s_1 \to s_2$. With $\pi_1$ and $\pi_2$ as product projections, it can be implemented as

$$\lambda p. (\pi_1 p) (\pi_2 p)$$

This is not enough to evaluate untyped lambda calculus. For example, in the exponential operator for Church numerals

$$\lambda n . \lambda m . m\ n,$$

the $m$ cannot be directly applied to $n$, because $m$ expects a first argument of type

$$a \to a$$

and $n$ has type

$$(a \to a) \to a \to a.$$

To evaluate the application $\lambda n . \lambda m . m\ n$, $m$ needs to be of the type

$$((a \to a) \to a \to a) \to (a \to a) \to a \to a = \operatorname{T_{a \to a}} ((a \to a) \to a \to a)$$

This equality implies we need a new evaluation function

$$eval_{a \to a} = \lambda p. (\operatorname{T_{a \to a}} (\pi_1\ p)) (\pi_2\ p)$$

The application $(\operatorname{T_{a \to a}} (\pi_1\ p)) (\pi_2\ p)$ will work, because $T_{a \to a}$ is Cartesian closed, so it will, in particular, preserve exponentials and their evaluation. In the example, this becomes

$$\lambda\ n : ((a \to a) \to a \to a) . \lambda\ m : ((a \to a) \to a \to a). (\operatorname{T_{a \to a}}\ m)\ n$$

which has the correct types.

In general, any signature $s$ gives a functor $\operatorname{T_s}$ with a evaluation-function:

$$\lambda p. (\operatorname{T_s} (\pi_1\ p)) (\pi_2\ p).$$

If this function existed, it would be the uncurried version of a function

$$\mu_s : s_2^{s_1} \to (\operatorname{T_s} s_2)^{\operatorname{T_s} s_2} = s_2^{s_1} \to \operatorname{T_s} (s_2^{s_1}).$$

The equality of types is due to the Cartesian closedness of $\operatorname{T_s}$.

If $\operatorname{T_s}$ was a monad and $\mu_s$ was the unit at $s_2^{s_1}$, it would behave exactly as expected. The problem is that those arrows do not exist in $\mathbf{STLC_1}$. Therefore, I am hoping to find a category very similar to $\mathbf{STLC_1}$, but one which has the required unit arrows. Hints might be if these monads arise in some bigger category as adjunctions with $\mathbf{STLC_1}$, or if arrows should be defined to also include $\operatorname{T_s}$.

The most annoying thing is that there is such a mapping, it is just a set theoretic function, not a lambda calculus one. For all signatures $s_1, s_2 \in \mathbf{STLC_1}$, $\operatorname{T_s}$ takes each term (arrow) $t : s_1 \to s_2$ to an arrow $\operatorname{T_s} t : (\operatorname{T_s}\ s_1) \to (\operatorname{T_s}\ s_2)$. These arrows correspond to points in the corresponding exponential objects $s_2^{s_1}$ and $(\operatorname{T_s}\ s_2)^{\operatorname{T_s}\ s_1}$, so $\operatorname{T_s}$ gives a mapping from points in $s_2^{s_1}$ to points in $(\operatorname{T_s}\ s_2)^{\operatorname{T_s}\ s_1}$, but $\mathbf{STLC_1}$ has no corresponding arrow.

So, what I am hoping to find is a category with similar properties as $\mathbf{STLC_1}$, but with the desired units, but really, right now any thoughts or hints are appreciated. Maybe some free category of lambda calculus/cartesian closedness?