Internalization of extensional equality

TL;DR

This paper introduces a type system with a universe of types closed under extensional equality reflection, advancing the formal understanding of extensionality in type theory.

Contribution

It presents a stratified type system extending lambda-*, incorporating internalized extensional equality, and provides a set-theoretic model for it.

Findings

Universe inconsistency is resolved by stratification.

A set-theoretic model for the stratified system is constructed.

Conjecture that strong normalization holds for the system.

Abstract

We give a type system in which the universe of types is closed by reflection into it of the logical relation defined externally by induction on the structure of types. This contribution is placed in the context of the search for a natural, syntactic construction of the extensional equality type (Tait [1995], Altenkirch [1999], Coquand [2011], Licata and Harper [2012], Martin-Lof [2013]). The system is presented as an extension of lambda-*, the terminal pure type system in which the universe of all types is a type. The universe inconsistency is then removed by the usual method of stratification into levels. We give a set-theoretic model for the stratified system. We conjecture that Strong Normalization holds as well.