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.