theorems for free, polymorphic equality

[sassa_nf]

Can someone walk me through the first paragraph of the section on polymorphic equality?
The programming language Miranda provides a polymorphic equality function, with type:

(=): ∀ X, X → X → Bool

Applying parametricity to the type of (=) yields, for all a : A → A'

for all x, y ∈ A, (x =A y) = (a x =A' a y).

This is obviously false
Then they also say "This is not a contradiction to the parametricity theorem".

Smells like bullshit. If the statement they've got is the result of applying parametricity, then it is a contradiction to the theorem. But also I have my doubts about how they have applied the theorem. Everywhere else there is no "=" between "(x =_A y)" and what follows; only a "if...then".

Comments

[juan-gandhi.livejournal.com]

Is it

for all a : A → A' for all x, y ∈ A, (x =A y) = (a x =A' a y)

?

Anyway, looks totally weird to me.

But I don't believe in parametricity theorem anyway.

[sassa-nf.livejournal.com]

Yes, it is "for all a", at the end of the line above the statement. I was just copying the article.