Because propositions and data are used differently and are governed by different rules, the abbreviations Type and Prop are provided to make the distinction more convenient.
Type u is an abbreviation for Sort (u + 1), so Type 0 is Sort 1 and Type 3 is Sort 4.
Type 0 can also be abbreviated Type, so Unit : Type and Type : Type 1.
Prop is an abbreviation for Sort 0.
3.3.1. Predicativity
Each universe contains dependent function types, which additionally represent universal quantification and implication.
A function type's universe is determined by the universes of its argument and return types.
The specific rules depend on whether the return type of the function is a proposition.
Predicates, which are functions that return propositions (that is, where the result of the function is some type in Prop) may have argument types in any universe whatsoever, but the function type itself remains in Prop.
In other words, propositions feature impredicative quantification, because propositions can themselves be statements about all propositions (and all other types).
Impredicativity
Proof irrelevance can be written as a proposition that quantifies over all propositions:
example : Prop := ∀ (P : Prop) (p1 p2 : P), p1 = p2
A proposition may also quantify over all types, at any given level:
example : Prop := ∀ (α : Type), ∀ (x : α), x = x
example : Prop := ∀ (α : Type 5), ∀ (x : α), x = x
For universes at level 1 and higher (that is, the Type u hierarchy), quantification is predicative.
For these universes, the universe of a function type is the least upper bound of the argument and return types' universes.
Universe levels of function types
Both of these types are in Type 2:
example (α : Type 1) (β : Type 2) : Type 2 := α → β
example (α : Type 2) (β : Type 1) : Type 2 := α → β
Predicativity of Type
This example is not accepted, because α's level is greater than 1. In other words, the annotated universe is smaller than the function type's universe:
example (α : Type 2) (β : Type 1) : Type 1 := type mismatch
α → β
has type
Type 2 : Type 3
but is expected to have type
Type 1 : Type 2α → β
type mismatch
α → β
has type
Type 2 : Type 3
but is expected to have type
Type 1 : Type 2
Lean's universes are not cumulative; a type in Type u is not automatically also in Type (u + 1).
Each type inhabits precisely one universe.
No cumulativity
This example is not accepted because the annotated universe is larger than the function type's universe:
example (α : Type 2) (β : Type 1) : Type 3 := type mismatch
α → β
has type
Type 2 : Type 3
but is expected to have type
Type 3 : Type 4α → β
type mismatch
α → β
has type
Type 2 : Type 3
but is expected to have type
Type 3 : Type 4
3.3.2. Polymorphism
Lean supports universe polymorphism, which means that constants defined in the Lean environment can take universe parameters.
These parameters can then be instantiated with universe levels when the constant is used.
Universe parameters are written in curly braces following a dot after a constant name.
Universe-polymorphic identity function
When fully explicit, the identity function takes a universe parameter u. Its signature is:
id.{u} {α : Sort u} (x : α) : α
Universe variables may additionally occur in universe level expressions, which provide specific universe levels in definitions.
When the polymorphic definition is instantiated with concrete levels, these universe level expressions are also evaluated to yield concrete levels.
Universe level expressions
In this example, Codec is in a universe that is one greater than the universe of the type it contains:
structure Codec.{u} : Type (u + 1) where
type : Type u
encode : Array UInt32 → type → Array UInt32
decode : Array UInt32 → Nat → Option (type × Nat)
Lean automatically infers most level parameters.
In the following example, it is not necessary to annotate the type as Codec.{0}, because Char's type is Type 0, so u must be 0:
def Codec.char : Codec where
type := Char
encode buf ch := buf.push ch.val
decode buf i := do
let v ← buf[i]?
if h : v.isValidChar then
let ch : Char := ⟨v, h⟩
return (ch, i + 1)
else
failure
Universe-polymorphic definitions in fact create a schematic definition that can be instantiated at a variety of levels, and different instantiations of universes create incompatible values.
Universe polymorphism and definitional equality
This can be seen in the following example, in which T is a gratuitously-universe-polymorphic function that always returns true.
Because it is marked Lean.Parser.Command.declaration : commandopaque, Lean can't check equality by unfolding the definitions.
Both instantiations of T have the parameters and the same type, but their differing universe instantiations make them incompatible.
opaque T.{u} (_ : Nat) : Bool := (fun (α : Sort u) => true) PUnit.{u}
set_option pp.universes true
def test.{u, v} : T.{u} 0 = T.{v} 0 := type mismatch
rfl.{?u.27}
has type
Eq.{?u.27} ?m.29 ?m.29 : Prop
but is expected to have type
Eq.{1} (T.{u} 0) (T.{v} 0) : Proprfl
type mismatch
rfl.{?u.27}
has type
Eq.{?u.27} ?m.29 ?m.29 : Prop
but is expected to have type
Eq.{1} (T.{u} 0) (T.{v} 0) : Prop
Auto-bound implicit arguments are as universe-polymorphic as possible.
Defining the identity function as follows:
def id' (x : α) := x
results in the signature:
id'.{u} {α : Sort u} (x : α) : αUniverse monomorphism in auto-bound implicit parameters
On the other hand, because Nat is in universe Type 0, this function automatically ends up with a concrete universe level for α, because m is applied to both Nat and α, so both must have the same type and thus be in the same universe:
partial def count [Monad m] (p : α → Bool) (act : m α) : m Nat := do
if p (← act) then
return 1 + (← count p act)
else
return 0
3.3.2.1. Level Expressions🔗
Levels that occur in a definition are not restricted to just variables and addition of constants.
More complex relationships between universes can be defined using level expressions.
Level ::= 0 | 1 | 2 | ... -- Concrete levels
| u, v -- Variables
| Level + n -- Addition of constants
| max Level Level -- Least upper bound
| imax Level Level -- Impredicative LUB
Given an assignment of level variables to concrete numbers, evaluating these expressions follows the usual rules of arithmetic.
The imax operation is defined as follows:
\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}
imax is used to implement impredicative quantification for Prop.
In particular, if A : Sort u and B : Sort v, then (x : A) → B : Sort (imax u v).
If B : Prop, then the function type is itself a Prop; otherwise, the function type's level is the maximum of u and v.
3.3.2.2. Universe Variable Bindings
Universe-polymorphic definitions bind universe variables.
These bindings may be either explicit or implicit.
Explicit universe variable binding and instantiation occurs as a suffix to the definition's name.
Universe parameters are defined or provided by suffixing the name of a constant with a period (.) followed by a comma-separated sequence of universe variables between curly braces.
Universe-polymorphic map
The following declaration of map declares two universe parameters (u and v) and instantiates the polymorphic List with each in turn:
def map.{u, v} {α : Type u} {β : Type v}
(f : α → β) :
List.{u} α → List.{v} β
| [] => []
| x :: xs => f x :: map f xs
Just as Lean automatically instantiates implicit parameters, it also automatically instantiates universe parameters.
When the autoImplicit option is set to true (the default), it is not necessary to explicitly bind universe variables.
When it is set to false, then they must be added explicitly or declared using the universe command.
Auto-implicits and universe polymorphism
When autoImplicit is true (which is the default setting), this definition is accepted even though it does not bind its universe parameters:
set_option autoImplicit true
def map {α : Type u} {β : Type v} (f : α → β) : List α → List β
| [] => []
| x :: xs => f x :: map f xs
When autoImplicit is false, the definition is rejected because u and v are not in scope:
set_option autoImplicit false
def map {α : Type unknown universe level 'u'u} {β : Type unknown universe level 'v'v} (f : α → β) : List α → List β
| [] => []
| x :: xs => f x :: map f xs
unknown universe level 'u'
unknown universe level 'v'
In addition to using autoImplicit, particular identifiers can be declared as universe variables in a particular section scope using the universe command.
syntax
command ::= ...
| Declares one or more universe variables.
`universe u v`
`Prop`, `Type`, `Type u` and `Sort u` are types that classify other types, also known as
*universes*. In `Type u` and `Sort u`, the variable `u` stands for the universe's *level*, and a
universe at level `u` can only classify universes that are at levels lower than `u`. For more
details on type universes, please refer to [the relevant chapter of Theorem Proving in Lean][tpil
universes].
Just as type arguments allow polymorphic definitions to be used at many different types, universe
parameters, represented by universe variables, allow a definition to be used at any required level.
While Lean mostly handles universe levels automatically, declaring them explicitly can provide more
control when writing signatures. The `universe` keyword allows the declared universe variables to be
used in a collection of definitions, and Lean will ensure that these definitions use them
consistently.
[tpil universes]: https://lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html#types-as-objects
(Type universes on Theorem Proving in Lean)
```lean
/- Explicit type-universe parameter. -/
def id₁.{u} (α : Type u) (a : α) := a
/- Implicit type-universe parameter, equivalent to `id₁`.
Requires option `autoImplicit true`, which is the default. -/
def id₂ (α : Type u) (a : α) := a
/- Explicit standalone universe variable declaration, equivalent to `id₁` and `id₂`. -/
universe u
def id₃ (α : Type u) (a : α) := a
```
On a more technical note, using a universe variable only in the right-hand side of a definition
causes an error if the universe has not been declared previously.
```lean
def L₁.{u} := List (Type u)
-- def L₂ := List (Type u) -- error: `unknown universe level 'u'`
universe u
def L₃ := List (Type u)
```
## Examples
```lean
universe u v w
structure Pair (α : Type u) (β : Type v) : Type (max u v) where
a : α
b : β
#check Pair.{v, w}
-- Pair : Type v → Type w → Type (max v w)
```
Declares one or more universe variables for the extent of the current scope.
Just as the variable command causes a particular identifier to be treated as a parameter with a particular type, the universe command causes the subsequent identifiers to be implicitly quantified as as universe parameters in declarations that mention them, even if the option autoImplicit is false.
The universe command when autoImplicit is false
set_option autoImplicit false
universe u
def id₃ (α : Type u) (a : α) := a
Because the automatic implicit parameter feature only insert parameters that are used in the declaration's header, universe variables that occur only on the right-hand side of a definition are not inserted as arguments unless they have been declared with universe even when autoImplicit is true.
Automatic universe parameters and the universe command
This definition with an explicit universe parameter is accepted:
def L.{u} := List (Type u)
Even with automatic implicit parameters, this definition is rejected, because u is not mentioned in the header, which precedes the :=:
set_option autoImplicit true
def L := List (Type unknown universe level 'u'u)
unknown universe level 'u'
With a universe declaration, u is accepted as a parameter even on the right-hand side:
universe u
def L := List (Type u)
The resulting definition of L is universe-polymorphic, with u inserted as a universe parameter.
Declarations in the scope of a universe command are not made polymorphic if the universe variables do not occur in them or in other automatically-inserted arguments.
universe u
def L := List (Type 0)
L : Type 1#check L
3.3.2.3. Universe Unification
Planned Content
Tracked at issue #99
3.3.2.4. Universe Lifting
Planned Content
Tracked at issue #174
🔗structurePLift.{u} (α : Sort u) : Type u
Universe lifting operation from Sort u to Type u.
Constructor
Fields
down | : | α |
|
Extract a value from PLift α
|
🔗structureULift.{r, s} (α : Type s) : Type (max s r)
Universe lifting operation from a lower Type universe to a higher one.
To express this using level variables, the input is Type s and the output is
Type (max s r), so if s ≤ r then the latter is (definitionally) Type r.
The universe variable r is written first so that ULift.{r} α can be used
when s can be inferred from the type of α.
Constructor
ULift.up.{r, s} |
Lift a value into ULift α
|
Fields
down | : | α |
|
Extract a value from ULift α
|