Are the "natural transformations" we apply on Coyoneda to get a Functor actually "natural transformations"?

Question

I have a theoretical question about the nature of a type that is used in a lot of examples explaining the Coyoneda lemma. They are usually referred to as "natural transformations" which to my knowledge mappings between functors. What puzzles me is that in these examples they sometimes map from Set to some functor F. So it does not really semm to be a mapping between functors but something a little more relaxed.

Here is the code in question:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
module Coyo where

import           Data.Set (Set)
import qualified Data.Set as Set

data Coyoneda f a where
  Coyoneda :: (b -> a) -> f b -> Coyoneda f a

instance Functor (Coyoneda f) where
  fmap f (Coyoneda c fa) =  Coyoneda (f . c) fa

set :: Set Int
set = Set.fromList [1,2,3,4]

lift :: f a -> Coyoneda f a
lift fa = Coyoneda id fa

lower :: Functor f => Coyoneda f a -> f a
lower (Coyoneda f fa) = fmap f fa

type NatT f g = forall a. f a -> g a

coyoset :: Coyoneda Set Int
coyoset = fmap (+1) (lift set)

applyNatT :: NatT f g -> Coyoneda f a -> Coyoneda g a
applyNatT n (Coyoneda f fa) = Coyoneda f (n fa)

-- Set.toList is used as a "natural transformation" here
-- while it conforms to the type signature of NatT, it
-- is not a mapping between functors `f` and `g` since
-- `Set` is not a functor.
run :: [Int]
run = lower (applyNatT Set.toList coyoset)

What am I misunderstanding here?

EDIT: After a discussion on #haskell in freenode I think I need to clarify my question a little. It's basically: "What is Set.toList in a category theoretic sense? Since it is obviously(?) not a natural transformation".

Answer 1

For n to be a natural transfomation in Haskell it needs to obey (for all f)

(fmap f) . n == n . (fmap f)

This isn't the case for Set.toList.

fmap (const 0) . Set.toList        $ Set.fromList [1, 2, 3] = [0, 0, 0]
Set.toList     . Set.map (const 0) $ Set.fromList [1, 2, 3] = [0]

Instead it obeys a different set of laws. There is another transformation n' back the other way such that the following holds

n' . (fmap f) . n == fmap f

If we choose f = id and apply the functor law fmap id == id we can see that this implies that n' . n == id and therefore we have a similar formula:

(fmap f) . n' . n == n' . (fmap f) . n == n' . n . (fmap f)

n = Set.toList and n' = Set.fromList obey this law.

Set.map (const 0) . Set.fromList   . Set.toList        $ Set.fromList [1, 2, 3] = fromList [0]
Set.fromList      . fmap (const 0) . Set.toList        $ Set.fromList [1, 2, 3] = fromList [0]
Set.fromList      . Set.toList     . Set.map (const 0) $ Set.fromList [1, 2, 3] = fromList [0]

I don't know what we can call this other than observing that Set is an equivalence class of lists. Set.toList finds a representative member of the equivalence class and Set.fromList is the quotient.

It's probably worth noting that Set.fromList is a natural transformation. At least it is on the reasonable subcategory of Hask where a == b implies f a == f b (here == is equality from Eq) . This is also the subcategory of Hask where Set is a functor; it excludes degenerate things like this.

leftaroundabout also pointed out that Set.toList is a natural transformation on the subcategory of Hask where morphisms are restricted to injective functions where f a == f b implies a == b.