Eta-expansions in dependent type theory the calculus of constructions

Abstract

Although the use of expansionary η-rewrite has become increasingly common in recent years, one area where η-contractions have until now remained the only possibility is in the more powerful type theories of the λ-cube. This paper rectifies this situation by applying η-expansions to the Calculus of Constructions - we discuss some of the difficulties posed by the presence of dependent types, prove that every term rewrites to a unique long βη-normal form and deduce the decidability of βη-equality, typeability and type inhabitation as corollaries.