Syntactic parametricity strikes again
In this blog post, reporting on a collaboration with Li-Yao Xia, I will show an example of how some results that we traditionally think of as arising from free theorems / parametricity can be established in a purely “syntactic” way, by looking at the structure of canonical derivations. More precisely, I prove that ∀α.List α→List α is isomorphic to Π(n:N).List (Fin n) where Fin n is the type of integers smaller than n, corresponding to the set {0,1,…,n−1}.