# Foundational Types

Some of Lean's types are not defined in any Lean source files (even the `prelude`

) since they come from its foundational type theory. This page provides basic documentation for these types.

For a more in-depth explanation of Lean's type theory, refer to TPiL.

`Sort u`

`Sort u`

is the type of types in Lean, and `Sort u : Sort (u + 1)`

.

## Instances For

`Type u`

`Type u`

is notation for `Sort (u + 1)`

.

## Instances For

`Prop`

`Prop`

is notation for `Sort 0`

.

## Instances For

## Pi types, `(a : α) → β a`

The type of dependent functions is known as a pi type. Non-dependent functions and implications are a special case.

Note that these can also be written with the alternative notations:

`∀ a : α, β a`

, conventionally used where`β a : Prop`

.`(a : α) → β a`

`α → γ`

, possible only if`β a = γ`

for all`a`

.

Lean also permits ASCII-only spellings of the three variants:

`forall a : A, B a`

for`∀ a : α, β a`

`(a : A) -> B a`

, for`(a : α) → β a`

`A -> B`

, for`α → β`

Note that despite not itself being a function, `(→)`

is available as infix notation for
`fun α β, α → β`

.