On the Definition of the Eta-long Normal Form in Type Systems of the Cube

TL;DR

This paper establishes that in the type systems of the cube, every well-typed normal term admits a unique eta-long normal form, based on a well-founded relation on terms and types.

Contribution

It defines the eta-long normal form within the type systems of the cube using a well-founded relation on terms and types.

Findings

Every well-typed normal term admits an eta-long normal form.

The relation < on terms is well-founded in the type systems of the cube.

The relation < is transitive and respects subterm structure.

Abstract

The smallest transitive relation < on well-typed normal terms such that if t is a strict subterm of u then t < u and if T is the normal form of the type of t and the term t is not a sort then T < t is well-founded in the type systems of the cube. Thus every term admits a eta-long normal form.