System F defines the data type pair as: $$X\times Y := \Pi Z. (X\to Y \to Z)\to Z$$ with: $$\langle x,y \rangle := \Lambda Z. \lambda p^{X\to Y\to Z}.p \text{ }x\text{ } y$$ Projections are defined: $$\pi^1 p := pX(\lambda x^X.\lambda y^Y.x)$$ $$\pi^2 p := pY(\lambda x^X.\lambda y^Y.y)$$

It is easy to prove that: $$\pi^1 \langle x,y \rangle=x$$ $$\pi^2 \langle x,y \rangle=y$$ But I do not know how to prove the following $$\langle \pi^1 p, \pi^2 p\rangle=p$$

I suppose that I will need the parametricity theorem...



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.