Lambda the Ultimate

A draft by Takeuti Izumi

This paper defines the theories of parametricity for the system lambda-P-omega in lambda cube, and shows some of its application. These theories are defined by the axiom sets in the formal theories. These theories prove various important semantical properties in the formal systems.

Parametricity is Wadler gets his theorems for free, nad Izumi gives an example of one of these free theorems for dependent sums in the Calculus of Constructions.