[Haskell-cafe] how to factorize propagation of a function over a data type

[TP]

Andras Slemmer wrote:

> The reason you need the typeclass constraint is not in the use of 'f' but
> rather in the use of propagate and what you pass in to it (foo1/foo2
> here). If you leave away the typeclass constraint what you're left with
> is:
> 
> propagate' Bar -> (forall a. a->a) -> Bar
> 
> The implementation of this function is the same as before, however your
> use of propagate' is restricted:
> forall a. a->a is a very "strict" type, in fact the only inhabitant of
> this type is 'id' (and bottom, but disregard that here), which means the
> only way to call propagate is to pass in 'id'. Try it yourself!

Indeed I have tried, it works as you say.

> Related note: there is a proof that in fact the only inhabitant of (forall
> a. a -> a) is 'id' and it is the consequence of the "parametricity"
> property. It is a very neat result I suggest you look it up!

Interesting. I have tried to google on the topic, but I find mainly research 
articles. For example:

https://www.google.fr/search?client=ubuntu&channel=fs&q=haskell+%22parametricity+property%22&ie=utf-8&oe=utf-8&gws_rd=cr&ei=P_acUvboDse_0QX9mYDADQ#channel=fs&q=%22parametricity+property%22+haskell

Are there textbooks where a proof of this fact could be found? I'm an 
autodidact (who also benefits from help of guys like you), I don't know what 
lectures on type theory at university level could look like.

Thanks

TP