I'm reading the wikipdia entry on Heyting Algebras to try to understand what relationship it might have to Wombat. I read:
"The ordering <= on a Heyting algebra H can be recovered from the operation → as follows: for any elements a, b of H, a<=b if and only if a→b = 1."
Which is very reminiscent of the "theorems for free" rule that the only polymorphic function a=>a is id. If we say a→b in the above sense, means (in Wombat types) a closure which has no side-affects, and doesn't use any specific features of a or b (is polymorphic), then it is true that a<=b in the Wombat type ordering (isA) can only be {$} -- i.e. like the identity, but able to move values up the hierarchy.
It is quite possible that I don't understand this at all.
