# Parametricity and projective eliminations for dependent records

It's well-known that in System F, you can encode binary products with the type $$A \times B \triangleq \forall\alpha.\; (A \to B \to \alpha) \to \alpha$$ You can then define projection functions $\pi_1 : A \times B \to A$ and $\pi_2 : A \times B \to B$.

This isn't so surprising, even though the natural reading of the F type is of a pair with a let-style elimination $\mathsf{let}\;(x,y) = p \;\mathsf{in}\; e$, because the two kinds of pair are interderivable in intuitionistic logic.

Now, in a dependent type theory with impredicative quantification, you can follow the same pattern to encode a dependent record type $\Sigma x:A.\; B[x]$ as $$\Sigma x:A.\;B[x] \triangleq \forall\alpha.\; (\Pi x:A.\; B[x] \to \alpha) \to \alpha$$ But in this case, there isn't a simple way of defining the projective eliminators $\pi_1 : \Sigma x:A.\;B[x] \to A$ and $\pi_2 : \Pi p:(\Sigma x:A.\;B[x]).\; B[\pi_1\,p]$.

However, if the type theory is parametric, you can use parametricity to show that $\pi_2$ is definable. This appears to be known --- see, for example, this Agda development by Dan Doel in which he derives it without comment --- but I can't seem to find a reference for this fact.

Does anyone know a reference for the fact that parametricity allows defining projective eliminations for dependent types?

EDIT: The closest thing I've found so far is this 2001 paper by Herman Geuvers, Induction is not derivable in second order dependent type theory, in which he proves that you can't do it without parametricity.

• I can't tell from this post what the question is. (I know nothing of the area and would not know anyway, but I'd like to be able to articulate the question) Commented Jul 17, 2012 at 6:04
• I added an explicit question line above the edit. Does this help? Commented Jul 17, 2012 at 7:16
• Yes. I was just not sure initially if it was a reference request only or a request for a proof. I will ask around. Commented Jul 18, 2012 at 5:41
• I had a discussion a couple months ago on here:queuea9.wordpress.com/2012/03/28/why-not-lambda-encode-data and I believe that the parametricity->elimination principle is folklore/original work from Dan. These discussions are close to others concerning parametricity by J.-P. Bernardi. You might want to take a look at the Coq standard library developments around dependent sums:coq.inria.fr/stdlib/Coq.Init.Specif.html and maybe coq.inria.fr/stdlib/Coq.Logic.EqdepFacts.html#
– cody
Commented Jul 18, 2012 at 14:51
• @kvb: I don't think there's a positive answer, yet. In my recent draft (with Derek Dreyer) on parametricity in the Calculus of Constructions (mpi-sws.org/~neelk/internalizing-parametricity.pdf), we show that parametricity makes it sound to add axioms that let you get strong elims out of the Church encoding. However, we don't yet have a good story for how to internalize parametricity in a way that computes well (most likely we need to integrate JP Bernardy's methods into our type theory). This doesn't seem impossible, but we don't know how yet. Commented Mar 15, 2013 at 20:11