A Framework for Internalizing Relations into Type Theory

This paper introduces the concept of internalization struc- ture, which can be used to incorporate certain relations into FΠ , a variant of system F, while maintaining termination of the new system. We will call this process of incorporation internalization, FΠ the base system and the new system after the incorporation the internalized system. We first specify the syntax, and then the semantics of FΠ via the Tait-Girard reducibility method. We then define internalization structure. We show that we can obtain a terminating internalized system from an internal- ization structure. Finally, as motivating examples, we demonstrate how our framework can be applied to internalize subtyping, full-beta term equality and term-type inhabitation relations.