# Where can I learn about Cartesian closed functors between categories of simply typed lambda calculus?

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.

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?

• Is there some confusion going on between having an atomic type $a$ and considering the type $(a \to a) \to (a \to a)$, which is not a useful type to assign to Church numerals (as you've discovered when trying to define arithmetic), and between polymorphic types, such as $\forall a . (a \to a) \to (a \to a)$, which does make Church numerals work well? Aug 31, 2023 at 7:05

If I understand correctly, you are considering simple types over $$\to,\times$$ as objects, $$\beta$$-normal, $$\eta$$-long $$\lambda$$-terms as arrows, and substitution plus normalization as composition. In that case, what you denote by $$\mathbf{STLC}_n$$ is the syntactic category of the simple higher-order theory with $$n$$ sorts and nothing else (if you prefer, the "free CCC" on a set with $$n$$ elements).
Now, I don't know what you mean by "simply-typed $$\lambda$$-calculus" but the most widespread definition is that, once you take the quotient under $$\beta\eta$$, this is the same thing as $$\mathbf{STLC}_\omega$$, that is, the "free CCC" on a countable set of atomic types $$\mathcal A$$. So the interpretation of the simply-typed $$\lambda$$-calculus in $$\mathbf{STLC}_n$$ is fairly uninteresting: it amounts to choosing a type $$T_A$$ with $$n$$ free atoms for every atomic type $$A\in\mathcal A$$, and then the interpretation of a term $$t$$ is the $$\beta$$-normal, $$\eta$$-long form of $$t$$ in which every atom $$A$$ is substituted with $$T_A$$ (typing is stable under arbitrary type substitutions). In particular, if $$t$$ is $$\beta$$-normal, $$\eta$$-long, then its interpretation is itself, modulo a type substitution.
It is true that this corresponds to a Cartesian-closed functor $$\mathbf{STLC}_\omega\to\mathbf{STLC}_n$$, but I am not sure how interesting this is. In fact, by virtue of the $$\mathbf{STLC}_n$$ categories being "free", any Cartesian-closed functor $$\mathbf{STLC}_n\to\mathbf{STLC}_m$$ amounts to choosing a type with $$m$$ atoms for each of the $$n$$ atoms of $$\mathbf{STLC}_n$$. That's it: the rest is imposed by the requirement that the functor be Cartesian-closed. So functors $$\mathbf{STLC}_n\to\mathbf{STLC}_m$$ are just finite type substitutions, restricted to types with $$m$$ atoms. Similarly, a Cartesian-closed functor $$\mathbf{STLC}_\omega\to\mathbf{STLC}_\omega$$ is an arbitrary type substition (every atom is assigned to an arbitrary simple type). It may turn out to be useful to think of type substitutions this way, although right now I don't have in mind any place where I've actually seen it done in the literature.