Title: Type reducibility and applications

Abstract:
We report work of Statman using the notion
of reducibility among simple types:

A red B iff there is a closed term F of type
            A->B such that F is modulo beta-eta
            conversion injective.

It turns out that types become well-ordered by
this relation red with order type omega+4. Results
of Friedman, Plotkin (relating convertibility and
validity in models) follow. Also canonical term models
will be analyzed.