$\newcommand{\A}{\operatorname{A}} \newcommand{\B}{\operatorname{B}} \newcommand{\Cat}{\mathcal{Cat}} \newcommand{\Cart}{\mathcal{Cart}} \newcommand{\C}{\mathbf{C}} \newcommand{\F}{\operatorname{F}} \newcommand{\from}{\leftarrow} \newcommand{\N}{\mathbf{N}} \newcommand{\obj}{\operatorname{obj}} \newcommand{\op}{\text{op}} \newcommand{\U}{\operatorname{U}} $As a software engineer, it is my experience that natural transformations between cartesian closed functors are hard to find, probably because exponentials aren’t purely covariant. I propose a new type of relationship: a parallel transformation between cartesian closed functors that is based on families of pushouts and pullbacks instead of families of arrows. This definition only makes sense if the domain category is (somehow) freely generated, so it is a (new?) kind of 2-adjunction. In structure, it is mostly a 2-adjunction extension of the adjunction defined in [Lambek], but most of the definitions are adapted from [Girard et. al.].
Given the forgetful functor $\U : \Cart \to \Cat$ that sends categories and functors in the 2-category $\Cart$ of cartesian closed categories and functors to the same categories and functors in $\Cat$, I will assume $\U$ has an adjunct free functor $\F : \Cat \to \Cart$ that, for each category $\N$ in $\Cat$ identifies the simply typed lambda calculus with product types freely generated from $\N$, similarly to the adjunction between $\mathbf{Graph}$ and $\Cart$ in [Lambek], but without natural number objects. For any cartesian closed category $\C \in \Cart$ and any (regular) category $\N \in \Cat$, the left adjunction is a bijection
$\Psi : (\N \to \U\ \C) \to (\F\ \N \to \C)$
(probably just up to isomorphism) from regular functors in $\Cat$ to cartesian closed functors in $\Cart$. I don't think it is possible to make $\Psi$ map natural transformations, and that is precisely why I needed to make a new construction.
Given a cartesian closed category $\C$, a “polymorphic type [expression] $\sigma (\alpha_1, \ldots ,\alpha_n)$, with type variables $\alpha_i$”, [Girard et. al. page 4] describes how to identify the interpretation of $\sigma$ as a functor $||\sigma|| : (\C^\op)^n \times \C^n \to \C$. For ease of comparison, I will adopt the notation in [Girard et. al.] for applying $||\sigma||$ to two vectors $\A$ and $\B$ of $n$ objects of $\C$, namely
$$||\sigma||(\A; \B).$$
For my adjunction to work, I need to replace $n$ in $\C^n$ with a category $\N$, so that that (the objects of) the functor category $(\U\ \C)^\N$ becomes the right homset of the adjunction. If $\N$ has $n$ objects and is discrete, the definitions coincide perfectly, since vectors with $n$ objects from $\C$ are in a one-to-one relationship with functors from $\N$ to $\C$. Since $\F\ \N$ is a freely generated cartesian closed category, it makes sense to use those objects as $\sigma$, see other chapters in [Lambek].
By the definitions of cartesian closed functors and $||\sigma||$, for any category $\N$, any cartesian closed category $\C$, any two functors $\A, \B : \N \to \U\ \C$ and any type $\sigma \in \F\ \N$
$$ \Psi\ \A\ \sigma = ||\sigma||(\A; \A) $$
points to the same, or at least isomorphic, objects. Note that $\Psi\ \A : \F\ \N \to \C$ is a functor from $\F\ \N$ to $\C$, so it makes sense to apply it to a type $\sigma \in \F\ \N$.
Again, if $\N$ is discrete the notion of “any vector of arrows $\operatorname{f} : \A \to \B$ from [Girard et. al. page 4] coincide perfectly with the set of natural transformations $\alpha : \A \to \B$. I will prefer the notation $\alpha$ to emphasize that it is the 2-cell of the right homset of my adjunction.
With this slight shift of notation, the main result of [Girard et. al.] is that if $\N$ is discrete and finite, the following dinaturality hexagon in $\U\ \C$ commutes for any cartesian closed category $\C$, any types $\sigma_1, \sigma_2 \in \F\ \N$, any term (arrow) $\tau : \sigma_1 \to \sigma_2$, any two functors $\A, \B : \N \to \U\ \C$, and any natural transformation $\alpha : \A \to \B$:
$$ ||\sigma_1|| (\B; \A) \stackrel{ ||\sigma_1||\ ( \B; \alpha )}{\to} \Psi\ \B\ \sigma_1 \stackrel{\Psi\ \B\ \tau}{\to} \Psi\ \B\ \sigma_2 \stackrel{||\sigma_2|| ( \alpha; \B )}{\to} ||\sigma_2|| ( \A; \B ) $$
$$ ||\sigma_1||\ ( \B; \A ) \stackrel{||\sigma_1||\ ( \alpha; \A )}{\to} \Psi\ \A\ \sigma_1 \stackrel{\Psi\ \A \tau}{\to} \Psi\ \A \sigma_2 \stackrel{||\sigma_2|| ( \A; \alpha )}{\to} ||\sigma_2|| ( \A; \B ). $$
I hope to someday prove that this is true for any category $\N$. This would include defining how the free functor $\F$ lifts arrows in $\N$ to terms in the logic $\F\ \N$ freely generated from $\N$. Such an arrow $f : a \to b$ in $\N$ means that $a$ postulates $b$, in the terminology of [Lambek].
If this is true, the 1-adjunction above can be turned into a kind of 2-adjunction, but the 2-cells on the left are not natural transformations, but something I will call “parallel transformations”. A parallel transformation is like a natural transformation, but the family of arrows is replaced by a family of pushout/pullback pairs. For any pair of functors $\A, \B: \N \to \U\ \C$, the natural transformation $\alpha: \A \to \B$ is sent by $\Psi$ to the family of pushouts and pullbacks indexed by objects $\sigma \in \F\ \N$ in the logic freely generated from $\N$:
$$ \Psi\ \A\ \sigma \stackrel{||\sigma|| (\alpha; \A)}{\from} ||\sigma|| (\B; \A) \stackrel{||\sigma|| (\B; \alpha)}{\to} \Psi\ \B\ \sigma $$
$$ \Psi\ \A\ \sigma \stackrel{||\sigma|| (\A; \alpha)}{\to} ||\sigma|| (\A; \B) \stackrel{||\sigma|| (\alpha; \B)}{\from} \Psi\ \B\ \sigma $$
Likewise, instead of using the family of arrows to lift arrows in the domain to commuting squares in the codomain, the parallel transformation lifts arrows to commuting hexagons with its family of pushout/pullback pairs.
I call it parallel because Milewski has taught me to imagine functors as pointing out parallel planes in the domain category, and natural transformations as perpendicular arrows going from the first plane to the second. My parallel transformation cannot do this, but if you compose the hexagon you get an arrow
$$ ||\sigma_1|| (\B; \A) \to ||\sigma_2|| (\A; \B) $$
that splits the hexagon horizontally, in parallel with the arrow $\tau : \sigma_1 \to \sigma_2$ lifted by $\A$ and $\B$ to the different planes
$$ \Psi\ \A\ \sigma_1 \stackrel{\Psi\ \A\ \tau}{\to} \Psi\ \A\ \sigma_2 $$
$$ \Psi\ \B\ \sigma_1 \stackrel{\Psi\ \B\ \tau}{\to} \Psi\ \B\ \sigma_2. $$
These “in between arrows” cannot be composed, because they go from the source of the pushout to the target of the pullback, but I am investigating if the bijection with natural transformations
$$ \operatorname{hom}(\A, \B) \to \operatorname{hom}(||\sigma_1|| (\B; \A), ||\sigma_2|| (\A; \B)) $$
can be used.
So, this is not much of a question, more like notes on what I’m currently working on. If you find something unclear in my description, it is probably because I have made some mistake somewhere, so please don't hesitate to point that out. If you have some paper or book in mind that might be beneficial for clarifying, proving, disproving or formalizing my concepts, I am more than interested.
[Lambek] Introduction to Higher Order Categorical Logic, section 1 chapter 4 “Free cartesian closed categories generated by graphs”
[Girard et. al.] Normal Forms and Cut-Free Proofs as Natural Transformations
