It is well known that the dinatural transformations between multivariant functors defined in Functorial polymorphism don't form a category, because they do not compose in general, but some do. For any Cartesian closed category $\mathbf{C}$ and any natural number $n$, there are a subclass of dinatural transformations, called the definable dinatural transformations between so called definable multivariant functors $\operatorname{M_1}, \operatorname{M_2} \in (\mathbf{C}^\text{op})^n \times \mathbf{C}^n \to \mathbf{C}$. It has been shown that definable dinatural transformations do compose, see Normal Forms and Cut-Free Proofs as Natural Transformations. Since definable dinatural transformations compose, they should form a category. I postulate that these categories are exactly the Cartesian closed categories freely generated from discrete graphs with $n$ nodes, using the adjunction defined in Introduction to Higher Order Categorical Logic.

Let $g_n$ be a discrete graph with $n$ nodes, and $\mathbf{C}$ any Cartesian closed category. According to the aforementioned adjunction there is exactly one Cartesian closed functor $\operatorname{G} = \Psi\ h : \operatorname{F}\ g_n \to \mathbf{C}$ for each graph homomorphism $h : g_n \to \operatorname{U}\ \mathbf{C}$, where $\operatorname{F}$ and $\operatorname{U}$ are the free and forgetful functors of the adjunction. Since $g_n$ is discrete, there are no edges to consider when making valid graph homomorphisms, so a graph homomorphism $h_\boldsymbol{A} : g_n \to \operatorname{U}\ \mathbf{C}$ is allowed to pick out exactly the nodes in $\operatorname{U}\ \mathbf{C}$ corresponding to a $n$-tuple of objects $\boldsymbol{A} \in \mathbf{C}^n$.

I propose that each object $m \in \operatorname{F}\ g_n$ indicates a definable, multivariant functor $\operatorname{M} \in (\mathbf{C}^\text{op})^n \times \mathbf{C}^n \to \mathbf{C}$

that takes diagonal objects

$$\operatorname{M}\ \boldsymbol{A}\ \boldsymbol{A} = \Psi\ h_\boldsymbol{A}\ m.$$

Note that $\Psi\ h_\boldsymbol{A}$ is a functor $\operatorname{F}\ g_n \to \mathbf{C}$, so $\Psi\ h_\boldsymbol{A}\ m$ is an object in $\mathbf{C}$. I leave out the general definition of $\operatorname{M}\ \boldsymbol{A}\ \boldsymbol{B}$ and its action on arrows for the sake of space, but they can be provided if you want. For each pair of objects $m_1, m_2 \in \operatorname{F}\ g_n$ and each arrow $t \in m_1 \to m_2$, there is a definable dinatural transformation $\alpha^t : \operatorname{M_1} \to \operatorname{M_2}$ with components

$${\alpha^t}_ \boldsymbol{A} = \Psi\ h_\boldsymbol{A}\ t$$

I hope this is clear, but feel free to ask for clarifications.

I’m mainly looking for literature on the subject or counter-examples, but if anyone can prove that $\alpha^t$ is really a dinatural transformation, that would be great.

It is well known that the dinatural transformations between multivariant functors defined in Functorial polymorphism don't form a category, because they do not compose in general, but some do. For any Cartesian closed category $\mathbf{C}$ and any natural number $n$, there are a subclass of dinatural transformations, called the definable dinatural transformations between so called definable multivariant functors $\operatorname{M_1}, \operatorname{M_2} \in (\mathbf{C}^\text{op})^n \times \mathbf{C}^n \to \mathbf{C}$. It has been shown that definable dinatural transformations do compose, see Normal Forms and Cut-Free Proofs as Natural Transformations. Since definable dinatural transformations compose, they should form a category. I postulate that these categories are exactly the Cartesian closed categories freely generated from discrete graphs with $n$ nodes, using the adjunction defined in Introduction to Higher Order Categorical Logic.

Let $g_n$ be a discrete graph with $n$ nodes, and $\mathbf{C}$ any Cartesian closed category. According to the aforementioned adjunction there is exactly one Cartesian closed functor $\operatorname{G} = \Psi\ h : \operatorname{F}\ g_n \to \mathbf{C}$ for each graph homomorphism $h : g_n \to \operatorname{U}\ \mathbf{C}$, where $\operatorname{F}$ and $\operatorname{U}$ are the free and forgetful functors of the adjunction. Since $g_n$ is discrete, there are no edges to consider when making valid graph homomorphisms, so a graph homomorphism $h_\boldsymbol{A} : g_n \to \operatorname{U}\ \mathbf{C}$ is allowed to pick out exactly the nodes in $\operatorname{U}\ \mathbf{C}$ corresponding to a $n$-tuple of objects $\boldsymbol{A} \in \mathbf{C}^n$.

I propose that each object $m \in \operatorname{F}\ g_n$ indicates a definable, multivariant functor $\operatorname{M} \in (\mathbf{C}^\text{op})^n \times \mathbf{C}^n \to \mathbf{C}$

that takes diagonal objects

$$\operatorname{M}\ \boldsymbol{A}\ \boldsymbol{A} = \Psi\ h_\boldsymbol{A}\ m.$$

Note that $\Psi\ h_\boldsymbol{A}$ is a functor $\operatorname{F}\ g_n \to \mathbf{C}$, so $\Psi\ h_\boldsymbol{A}\ m$ is an object in $\mathbf{C}$. I leave out the general definition of $\operatorname{M}\ \boldsymbol{A}\ \boldsymbol{B}$ and its action on arrows for the sake of space, but they can be provided if you want. For each pair of objects $m_1, m_2 \in \operatorname{F}\ g_n$ and each arrow $t \in m_1 \to m_2$, there is a definable dinatural transformation $\alpha^t : \operatorname{M_1} \to \operatorname{M_2}$ with components

$${\alpha^t}_ \boldsymbol{A} : \operatorname{M}_1 \ \boldsymbol{A}\ \boldsymbol{A} \to \operatorname{M}_2 \ \boldsymbol{A}\ \boldsymbol{A} = \Psi\ h_\boldsymbol{A}\ t$$

I hope this is clear, but feel free to ask for clarifications.

I’m mainly looking for literature on the subject or counter-examples, but if anyone can prove that $\alpha^t$ is really a dinatural transformation, that would be great.

It is well known that the dinatural transformations between multivariant functors defined in Functorial polymorphism don't form a category, because they do not compose in general, but some do. For any Cartesian closed category $\mathbf{C}$ and any natural number $n$, there are a subclass of dinatural transformations, called the definable dinatural transformations between so called definable multivariant functors $\operatorname{M_1}, \operatorname{M_2} \in (\mathbf{C}^\text{op})^n \times \mathbf{C}^n \to \mathbf{C}$. It has been shown that definable dinatural transformations do compose, see Normal Forms and Cut-Free Proofs as Natural Transformations. Since definable dinatural transformations compose, they should form a category. I postulate that these categories are exactly the Cartesian closed categories freely generated from discrete graphs with $n$ nodes, using the adjunction defined in Introduction to Higher Order Categorical Logic.

Let $g_n$ be a discrete graph with $n$ nodes, and $\mathbf{C}$ any Cartesian closed category. According to the aforementioned adjunction there is exactly one Cartesian closed functor $\operatorname{G} : \operatorname{F}\ g_n \to \mathbf{C}$ for each graph homomorphism $h : g_n \to \operatorname{U}\ \mathbf{C}$, where $\operatorname{F}$ and $\operatorname{U}$ are the free and forgetful functors of the adjunction. Since $g_n$ is discrete, there are no edges to consider when making valid graph homomorphisms, so a graph homomorphism $h_\boldsymbol{A} : g_n \to \operatorname{U}\ \mathbf{C}$ is allowed to pick out exactly the nodes in $\operatorname{U}\ \mathbf{C}$ corresponding to a $n$-tuple of objects $\boldsymbol{A} \in \mathbf{C}^n$.

I propose that each object $m \in \operatorname{F}\ g_n$ indicates a definable, multivariant functor $\operatorname{M} \in (\mathbf{C}^\text{op})^n \times \mathbf{C}^n \to \mathbf{C}$

that takes diagonal objects

$$\operatorname{M}\ \boldsymbol{A}\ \boldsymbol{A} = \operatorname{F}\ h_\boldsymbol{A}\ m.$$

Note that $\operatorname{F}\ h_\boldsymbol{A}$ is a functor $\operatorname{F}\ g_n \to \mathbf{C}$, so $\operatorname{F}\ h_\boldsymbol{A}\ m$ is an object in $\mathbf{C}$. I leave out the general definition of $\operatorname{M}\ \boldsymbol{A}\ \boldsymbol{B}$ and its action on arrows for the sake of space, but they can be provided if you want. For each pair of objects $m_1, m_2 \in \operatorname{F}\ g_n$ and each arrow $t \in m_1 \to m_2$, there is a definable dinatural transformation $\alpha^t : \operatorname{M_1} \to \operatorname{M_2}$ with components

$${\alpha^t}_ \boldsymbol{A} = \operatorname{F}\ h_\boldsymbol{A}\ t$$

I hope this is clear, but feel free to ask for clarifications.

I’m mainly looking for literature on the subject or counter-examples, but if anyone can prove that $\alpha^t$ is really a dinatural transformation, that would be great.

It is well known that the dinatural transformations between multivariant functors defined in Functorial polymorphism don't form a category, because they do not compose in general, but some do. For any Cartesian closed category $\mathbf{C}$ and any natural number $n$, there are a subclass of dinatural transformations, called the definable dinatural transformations between so called definable multivariant functors $\operatorname{M_1}, \operatorname{M_2} \in (\mathbf{C}^\text{op})^n \times \mathbf{C}^n \to \mathbf{C}$. It has been shown that definable dinatural transformations do compose, see Normal Forms and Cut-Free Proofs as Natural Transformations. Since definable dinatural transformations compose, they should form a category. I postulate that these categories are exactly the Cartesian closed categories freely generated from discrete graphs with $n$ nodes, using the adjunction defined in Introduction to Higher Order Categorical Logic.

Let $g_n$ be a discrete graph with $n$ nodes, and $\mathbf{C}$ any Cartesian closed category. According to the aforementioned adjunction there is exactly one Cartesian closed functor $\operatorname{G} = \Psi\ h : \operatorname{F}\ g_n \to \mathbf{C}$ for each graph homomorphism $h : g_n \to \operatorname{U}\ \mathbf{C}$, where $\operatorname{F}$ and $\operatorname{U}$ are the free and forgetful functors of the adjunction. Since $g_n$ is discrete, there are no edges to consider when making valid graph homomorphisms, so a graph homomorphism $h_\boldsymbol{A} : g_n \to \operatorname{U}\ \mathbf{C}$ is allowed to pick out exactly the nodes in $\operatorname{U}\ \mathbf{C}$ corresponding to a $n$-tuple of objects $\boldsymbol{A} \in \mathbf{C}^n$.

I propose that each object $m \in \operatorname{F}\ g_n$ indicates a definable, multivariant functor $\operatorname{M} \in (\mathbf{C}^\text{op})^n \times \mathbf{C}^n \to \mathbf{C}$

that takes diagonal objects

$$\operatorname{M}\ \boldsymbol{A}\ \boldsymbol{A} = \Psi\ h_\boldsymbol{A}\ m.$$

Note that $\Psi\ h_\boldsymbol{A}$ is a functor $\operatorname{F}\ g_n \to \mathbf{C}$, so $\Psi\ h_\boldsymbol{A}\ m$ is an object in $\mathbf{C}$. I leave out the general definition of $\operatorname{M}\ \boldsymbol{A}\ \boldsymbol{B}$ and its action on arrows for the sake of space, but they can be provided if you want. For each pair of objects $m_1, m_2 \in \operatorname{F}\ g_n$ and each arrow $t \in m_1 \to m_2$, there is a definable dinatural transformation $\alpha^t : \operatorname{M_1} \to \operatorname{M_2}$ with components

$${\alpha^t}_ \boldsymbol{A} = \Psi\ h_\boldsymbol{A}\ t$$

I hope this is clear, but feel free to ask for clarifications.

I’m mainly looking for literature on the subject or counter-examples, but if anyone can prove that $\alpha^t$ is really a dinatural transformation, that would be great.