Proxy contains no runtime information, you can always write a natural transformation
f a -> Proxy a for any
proxy :: f a -> Proxy a proxy _ = Proxy
This is just like how any given value can always be erased to
unit :: a -> () unit _ = ()
Proxy is the terminal object in the category of functors, just like
() is the terminal object in the category of values.