By a “structure category” I mean a concrete category that contains as objects all spaces of a particular type of structure, and as morphisms, functions that preserve that type of structure. I.e. the standard categories like Grp, Top, Cat, Ab, Vec, ... etc.
A “parametric polymorphic function” is a concept from type theory and functional programming, which says intuitively that
parametric polymorphic function: a function $f_X$ that is parameterized by type (object) $X$, but where the computation it performs is independent of $X$.
Obviously, a parametric polymorphic function is a natural transformation in a category where objects are types (if the underlying functors are also well-behaved, e.g. are also parametric polymorphic). This is because of some “theorems for free” result.
But natural transformations are defined categorically, rather than type theoretically. So in arbitrary categories, a natural transformation does not need to correspond to any parametric polymorphic function.
I am wondering whether in “structure categories”, the “naturality” of $f_X$ (i.e. of a pre-natural transformation), coincides with “parametric polymorphism”, and how this can be seen from the definition.
Are there (natural?) examples of natural transformations $f_X$ in structure categories that are not “parametrically polymorphic”? I.e. whose formula/computation depends on the object $X$?
If not, how can we see from the commuting diagram property of natural transformations $f_X$ that “they do the same computation regardless of $X$”?
Can we prove the inverse of the “theorems for free” result? i.e. Can we prove that, if a transformation is natural in the category of a ”sufficiently general” type system, then it must be somehow equivalent to a parametrically polymorphic function (possibly given some conditions on the underlying functors)?