So, I'm working on this project and I'm having some trouble with a definition. Maybe some more educated Category Theorists can help me.
The context is actually not very relevant, as I just need to frame my definition (if possible) correctly inside Category Theory.
I'm defining something that should be generic on the type it works with. My type language is composed of a few base types, fixed, and has products, coproducts and least-fixed points. Let's call this category $Hask$, of Haskell types and functions.
For any type in my language, I want to transform it, inductively on it's structure, on the following way:
$\begin{eqnarray} d\; t & = & D_t\; , \text{for }t\text{ a base type.} \\ d\;1 & = & 1\\ d\;(A \times B) & = & d \; A \times d\; B \\ d\;(A + B) & = & d\;A + d\;B + A \times B \\ d\;(\mu X . F_A \;X) & = & \mu X . 1 + (F_{d\; A}\;1 \times X) + 2\times(F_A\;1 \times X) \end{eqnarray}$
So, $d : Hask \rightarrow Hask$ If I want $d$ to be a functor, I need to define its action on arrows and prove that it preserves identity and compositions.
But it makes no sense to define $d$ on arrows that change the structure, for instance, it makes sense to define $d\;f : d (A \times B)\;\rightarrow d\;(C \times D)$, but not for $g : A \times B \rightarrow C$, for a $C$ that is not a product.
Which makes me wonder if I should frame it as a natural transformation, then. If I do that, the naturality diagrams are giving me some trouble.
Any comments or ideas are appreciated! Thanks in advance,
Victor