Foundations of Functional Programming/UTT-Σ

UTT_Σ is a fairly elaborate explicitly typed λ-calculus. It can be viewed as an extension of the calculus of constructions (λPω) of the λ-cube, which is the fullest-featured system of the λ-cube, featuring dependent types, polymorphic types, and type constructors. UTT_Σ was introduced by Ulf Norell in his PhD thesis (Norell 2007), and it is the basic type theory underlying the Agda programming language.

UTT_Σ differs from the calculus of constructions in three primary ways.

• Rather than including just two sorts ${\text{Type}}_{0}$ and ${\text{Type}}_{1}$, it includes an infinite hierarchy of sorts, ${\text{Type}}_{0},{\text{Type}}_{1},{\text{Type}}_{2},...$.
• Its sorts are cumulative, meaning that when $n\leq m$, any type belonging to ${\text{Type}}_{n}$ also belongs to ${\text{Type}}_{m}$. This fact means that types are not unique up to β-conversion, and necessitates the introduction of a subtyping relation.
• It includes a wider variety of types than the calculus of constructions. It includes dependent pair types and a unit type in addition to sorts and dependent function types. The additional types are interesting primarily because of their interpretation under the Curry-Howard correspondence.