**A Relationally Parametric Model of the Calculus of Constructions**

In this paper, we give the first relationally parametric model of the (extensional) calculus of constructions. Our model remains as simple as traditional PER models of dependent types, but unlike them, our model additionally permits relating terms atInsofar as anything having to do with dependent types can be, the key idea in this paper is really, really simple. There's a really beautiful, simple generalization of partial equivalence relations (aka PERs) (calleddifferentimplementation types. Using this model, we can validate the soundness of quotient types, as well as derive strong equality axioms for Church-encoded data, such as the eta-law for strong dependent pair types.

*quasi-PERs*) that let us give a parametric model without having to jump through the hoops the usual methods does.