Foundational types

Sort u

The type of types, one level at a time. Every type in Lean belongs to some Sort u, where the universe level u is a natural number or a variable standing for one. A term of Sort u is itself a type, whose own terms are the values.

The hierarchy is strict: Sort u : Sort (u+1), and there is no Sort ∞. That is what keeps the system consistent — a single type of all types would contain itself.

Prop

Prop is Sort 0, the sort of propositions. A term of a proposition is a proof of it, and Prop is proof-irrelevant: any two proofs of the same proposition are definitionally equal, so a proof can never be inspected to produce data. This is why theorems can be erased at compile time and why they are shown apart from definitions in this documentation.

Type u

Type u abbreviates Sort (u+1), and Type on its own means Type 0. These are the sorts data lives in: Nat, List α and every structure declared in this package are terms of some Type u. Unlike Prop, distinct terms of a type stay distinct.

Dependent function types

(x : α) → β x is the type of functions whose result type may mention the argument. When β does not use x it is written α → β, the ordinary function type. Binders in the signatures on these pages are the same thing in another spelling: ∀ (x : α), β x is the dependent function type when the result is a proposition, and {x : α} or [Inst α] mark an argument the elaborator is expected to supply.

For the rules behind any of this, see Lean's own documentation — this page only names the things a signature on this site can link to.