As a Warm-up, we prove (A→X)→X is isomorphic to A

[sassa_nf]

well... under assumption of parametricity:

https://homepages.inf.ed.ac.uk/wadler/papers/leibniz/leibniz.pdf

Comments

[juan_gandhi]

So weird.

[sassa_nf]

To be fair, they prove not isomorphism of A and its double negation, but (X:Type)→(A→X)→X, which is not a double negation.

[juan_gandhi]

Still weird; I'm trying to read it, but it seems like without having a decent knowledge of Agda, it's hardly possible to understand.

[sassa_nf]

I can help with syntactic things. The rest seems to be just intuitionistic logic.

This paper is referenced from the pfla book you are reading, in the chapter on equality. I thought, what's the hard bit that deserved a paper - Leibniz vs Martin-Löf equality looks trivial. But then proving their isomorphism is the tricky business.

[sassa_nf]

How about Yoneda Lemma?

It basically amounts to a claim that Yo f a is isomorphic to f a, when f is a Functor:

data Yo f a = Yo {unYo :: ∀r . (a → r) → f r }

Then for Functor Id we get ∀r . (a → r) → r is isomorphic to a.

[juan_gandhi]

Right; later I figured that it's basically all about Yoneda.