Is lambda calculus polymorphism a type of generalized monad?

Question

Let $\mathbf{C}$ be a Cartesian closed category. Then simply typed lambda calculus in $\mathbf{C}$ in one type variable can be interpreted as a category $\mathbf{STLC}_{\mathbf C}$ where the objects are functors from $\mathbf{C}^\text{op} \times \mathbf{C}$ to $\mathbf{C}$ and the morphisms are dinatural transformations between the functors, see for example “Normal Forms and Cut-Free Proofs as Natural Transformations” by Girard, Scedrov, and Scott. I am looking at lambda polymorphism in this category. Say we have the Church numeral $n$ with signature $\Pi x . (x \rightarrow x) \rightarrow x \rightarrow x$ and want to apply this to a second Church numeral $m$ with signature $\Pi y . (y \rightarrow y) \rightarrow y \rightarrow y$.

$$n\ m$$

In simply typed lambda calculus, this is not allowed, because $m$ does not have a type that $n$ accepts as input. In order to evaluate this expression, we have to “lift” $n$ by $(y \rightarrow y)$ to a new variable $n'$ with the signature

$$(\Pi x . (x \rightarrow x) \rightarrow x \rightarrow x)) (y \rightarrow y) = ((y \rightarrow y) \rightarrow (y \rightarrow y)) \rightarrow (y \rightarrow y) \rightarrow (y \rightarrow y)$$

so that every $x$ in the signature is replaced with $(y \rightarrow y)$. Then, $n'\ m$ has correct types for the application.

This “lifting” seems to me like a monoid in $\mathbf{STLC}_{\mathbf C}$ with identity $\Pi x . x$, the identity functor. Is that correct?

Also, one could call the lambda calculus terms a special type of endofunctors, of mixed variance, that are the objects of a category where the arrows are dinatural transformations that do compose, as proved in the paper mentioned above. A monoid in this endofunctor-category-like thing looks very much like a generalization of a monad in $\mathbf{C}$ . Does this concept have a name?

Answer 1

Short answer: Unfortunately, no.

Long answer: It would seem the author of this question (me) has confused the concepts monoids and monoidal structures in a category. Given a Category $\mathbf{C}$ and the category $\mathbf{C}^\mathbf{C}$ of $\mathbf{C}$ endofunctors, composition $\operatorname{F} \circ \operatorname{G}$ of two endofunctors $\operatorname{F}$ and $\operatorname{G}$ define a monoidal structure in $\mathbf{C}^\mathbf{C}$, with $\circ$ as tensor product and the identity functor $\operatorname{Id}$ as neutral element. The "lifting" in the question seems related to this concept.

A monoid in $\mathbf{C}^\mathbf{C}$ can be defined as an object $\operatorname{T}$ of $\mathbf{C}^\mathbf{C}$, (i. e. a specific $\mathbf{C}$ endofunctor) and two morphisms in $\mathbf{C}^\mathbf{C}$, $\eta : \operatorname{Id} \rightarrow \operatorname{T}$ and $\mu : \operatorname{T} \circ \operatorname{T} \to \operatorname{T}$, that is two natural transformations, one from the functor $\operatorname{T}$ composed with itself to $\operatorname{T}$, and one from the identity functor to $\operatorname{T}$. If the lifting mentioned in the question is seen as a kind of composition, then a monad would be a certain simply typed lambda signature $s$, with some mapping $\eta$ (dinatural transformation?) from the identity functor to $s$ and one mapping $\mu$ from $s$ lifted by $s$ to $s$. These operators should of course adhere to some generalization of the usual monad laws, which are readily available online.