In a nutshell, the question is: is it true that any explicit (not involving axiom of choice) pointwise transformation between sufficiently complicated functors is natural almost everywhere?
Let $C$ be a sufficiently big category. It should be big enough that it would be impossible to explicitly describe all its objects and morphisms. For concreteness we assume $C=Set$, but it could also be any topos over $Set$ or algebraic category over $Set$ or even something more general. Note that in this case for any cardinality $\aleph$ there is a possibly large class of objects with this cardinality, even if $\aleph$ is finite. Even if $\aleph = 1$ there is a class of such sets, since for any $x:Set$ we have $\{x\} : Set$. Let $F,G: C\to Set$ be two functors, which we could even assume representable.
By a pointwise transformation I mean a function $x:C \mapsto \mu_x : (Fx \to Gx)$. It is natural if it satisfies the usual identities and unnatural if some identities fail. The folk lore is that defining any transformation between so complicated functors is hard enough that we can't accidentally write out an unnatural one, i.e. if you manage to define some transformation then it should be natural. This obviously fails if $C$ is not complicated enough. For example, if $C$ would have a finite set of objects, then we could just explicitly pick $\mu_x$ without regard to morphisms. Similarly, if $Ob \ C$ is countable, then some induction will usually define unnatural transformation.
If we believe in the axiom of choice for classes then unnatural transformations are easy to define: apply choice to the epimorphism $\left( \coprod_x (Fx \to Gx)\right) \to Ob \ C$. However, such transformations are generally useless, since there extremely little we can say about them. I am interested in explicitly defined transformations. The simplest way is just not to assume choice, the more preferable one is to use some sort of type theory (e.g. Martin-Löf one), which doesn't allow arbitrary choice for all types. Almost all examples of unnatural transformations that I can think of use choice in one way or another.
- Any category is equivalent to its skeleton, which could have a countable set of objects, however such equivalence requires choice, thus we cannot hope to push $F,G: C\to Set$ to $\hat F, \hat G: \mathrm{sk}\ C \to Set$, choose $\hat F \to \hat G$ unnaturally by induction and lift it to $C$.
- A particular case of the previous exaample is $C=FinSet$.There is a function $C\to \mathbb{N}$ mapping $x \mapsto \# x$. We could give an "inverse" by mapping $n: \mathbb N \to [n]: FinSet$, where $[n]$ is the standard set with $n$ elements, but this doesn't define an equivalence in the absence of choice, thus we can't define $\mu_x$ unnaturally.
Essentially all examples from this question arise either for finite-object $C$ or for some arbitrary choice of equivalence with skeleton. Consider the following examples:
Eric Wofsey gives the following example: consider the categories of $k$-vector spaces $Vect$ and $k$-affine spaces $Aff$, where an affine space is a $V$-torsor for $V: Vect$: a pair $(V:Vect, X: Set)$ with free and transitive $V$-action on $X$. We have $U: Aff \to Vect$ sending each affine space to its structure group $V$ and $F: Vect \to Aff$ which maps $V: Vect$ to $V$ considered as $V$-torsor. Both of these functors are defined naturally and explicitly. We have a natural isomorphism $UF \simeq 1_{Vect}$ and an unnatural isomorphism $UF \simeq 1_{Aff}$: while any $(V,X): Aff$ is isomorphic to $(V,V):Aff$, such an isomorphism requires a choice of point $x_0 : X$. The only way to choose a point simultaneously in all $A: Aff$ seems to involve the axiom of choice for classes.
- The same problem exists with unnaturalness of universal coefficient splitting: the splitting of $$0 \to \mathrm{Ext}^1_R ( H_{i-1}(X,G), G) \to H^i (X,G) \to \mathrm{Hom}_R ( H_i (X,G), G) \to 0$$ even if $H_i$ is free requires both a choice of basis in $H_i$ and a choice of lifting to $H^i$ for the dual basis.
One class of explicit examples that I can think of goes as follows: split $C$ into finitely many full subcategories $C_i$ (i.e. $Ob\ C = \coprod_i Ob\ C_i$), then choose a different natural transformation for each $C_i$. For example we could consider $F\equiv Set(A,\cdot), G\equiv Set(B,\cdot): Set \to Set$, choose $f: A\to B$, $g: A\to A$, split $Set$ into $C_1 := \{x:Set \vert x = [2] \}$ and $C_2 := \{x:Set \vert x \ne [2] \}$. Define $\mu\vert_{C_1} : F\vert_{C_1} \to G\vert_{C_1}$ as $Set(f,\cdot)$ and $\mu\vert_{C_2} : F\vert_{C_2} \to G\vert_{C_2}$ as $Set(fg,\cdot)$. Together they glue to unnatural $\mu: F \to G$.
The previous example could be generalized to a countable number of $C_i$ with $\mu\vert_{C_i} := Set( f \circ g^{i-1} , \cdot)$. Note that such $\mu$ is still natural almost everywhere. I am uncertain what "natural almost everywhere" could mean in full generality, but an ad-hoc definition could be: there is a set $B$ and a function $\pi: Ob\ C \to B$ such that isomorphic objects map to the same element, and the unnatural transformation $\mu$ is constructed as a coproduct of natural $\mu_i: F\vert_{C_i} \to G\vert_{C_i}$ for $i: B$, where $C_i$ are full subcategories with $Ob\ C_i := \{x: C \vert \pi(x)=i \}$.
I feel as if any definable pointwise transformation would be natural almost everywhere, but I can't see how could one even hope to prove it. In particular, unnatural transformations should be defined by explicit case analysis, thus if we give a definition uniformly (in some sense) over $x: C$ then it will automatically be natural. Can this intuition be made explicit?
Thus I seek either for an unnatural transformation not involving choice and not natural almost everywhere or for some proof (or way to proof) that it does not exist.
