A syntactic approach to eta equality in type theory

Abstract

This paper outlines an elementary approach for showing the decidability of type checking for type theories with βη-equality, relevant to foundations for modules systems and type theory-based proof systems. The key to the approach is a syntactic translation mapping terms in the βη presentation into their full η-expansions in the β presentation. Decidability of type checking is lifted from the target β presentation to the βη presentation. The approach extends to other inductive kinds with a single constructor, and is demonstrated for singletons and dependent pairs.