Suppose you're working in some System-F like language, and you try to think of Leibniz equality in a propositions-as-types way, like you want to define X = Y at type τ as

eq(X,Y) = ∀ P : τ → * . P X → P Y

where * is the kind "type". In plain english, for every property that X has, Y also has it. You might ask (as someone did during PLClub) hey, isn't this definition asymmetric? Shouldn't we say also that for every property that Y has, X also has it? The speaker said, ah, well, the property of

*not*P is also a property, so we just substitute that in and we're good.

I thought to myself, gosh, that's an awfully classical way of thinking about it. Since we are bein' all propositions-as-types here, isn't there a more constructive way of doing it?

Yup. It still feels like simulating a sort of negation, but it's fully constructive for sure.

Okay, so we want to show that this definition actually is symmetric, despite appearances. So we have to build a term of type eq(X,Y) → eq(Y,X), or in other words of type

(∀ P : τ → * . P X → P Y) → (∀ Q : τ → * . Q Y → Q X)

where we are just alpha-varying P to Q in the second copy of eq to keep things separate.

The term is

λ q : (∀ P : τ → * . P X → P Y) . Λ Q : τ → * . &lambda y : Q Y. q [λz. Q z → Q X] id y

What's going on is that we instantiate the known equality "from" X to Y — that is, the implication from P X to P Y — by substituting λz. Q z → Q X for the predicate P. This plays the role of negating Q, but we're not really flat-out negating it, we're just putting it in an implication towards Q X.

Now our next obligation is to show that P X holds, which after substitution means showing Q X → Q X. But that's trivial, so we prove it with the identity function id. What we get out is P Y, or after substitution Q Y → Q X. But Q X is exactly what we want, and Q Y is what (in the form of y) we have. So we're done.

Impredicative polymorphism sure is wacky, isn't it?