I'll try to describe the subject I am looking for literature on, or concept names that I can Google.
For each $n \geq 1$, let $\mathbf{STLC}_n$ be the category where the objects are all simply typed lambda calculus types with $n$ or fewer type variables, and the arrows are all lambda terms with the corresponding domain and codomain. For example, a Church numeral-like term (only strong enough to define composition of an arrow $a \to a$ with itself $n$ times) is a point in the type $(a \to a) \to a \to a$ in all those categories, because it has only one type variable $a$, but the object $(b \to c) \to (a \to b) \to a \to c$ (containing composition $\lambda f . \lambda g . \lambda x.f(g\ x)$ as its only point) only exists in the categories with $n \geq 3$, because there are three type variables $a$, $b$ and $c$.
These categories are Cartesian closed, so it makes sense to interpret simply typed lambda calculus in them, so that simply typed lambda calculus is interpreted over another simply typed lambda calculus. I believe this can be seen as (tuples of?) Cartesian closed functors between the categories mentioned above.
Where can I learn more about Cartesian closed functors between those categories?
I am particularly interested in their relationship with the semantics of untyped lambda calculus or some second order lambda calculus. Or do they form a Lawvere theory, or some generalization thereof?
