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 types 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 types $s_1, s_2 \in \mathbf{STLC_1}$ (s is for signature, CS lingo for lambda types) 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 types $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 type $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 types $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 type $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 types $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?