We give the first relationally parametric model of the extensional
calculus of constructions. Our model remains as simple as traditional
PER models of types, but unlike them, it additionally permits the
relating of terms that implement abstract types in different ways.
Using our model, we can validate the soundness of quotient types, as
well as derive strong equality axioms for Church-encoded data, such as
the usual induction principles for Church naturals and booleans, and
the eta law for strong dependent pair types. Furthermore, we show
that such equivalences, justified by relationally parametric
reasoning, may soundly be internalized (i.e. added as equality axioms
to our type theory). Thus, we demonstrate that it is possible to
interpret equality in a dependently-typed setting using parametricity.
The key idea behind our approach is to interpret types as *quasi-PERs*
(or *zigzag-complete relations*), which enable us to model the
symmetry and transitivity of equality while at the same time allowing
for different representations of abstract types.