Parametricity and dependent types

Reynolds\u27 abstraction theorem shows how a typingjudgement in System F can be translated into a relational statement (in second order predicate logic)about inhabitants of the type. We expose a similar result, whereterms, types, and their relations are expressed in a single typed lambda calculus (a pure type system).Working within a single system dispenses the need for aninterpretation layer, allowing for an unusually simplepresentation. While the unification puts some constraints on the type system(which we spell out), the result applies to many interesting cases, includingdependently-typed ones