3.3. 宇宙（Universes）

型は 宇宙 （universe）によって分類されます。 各宇宙には レベル （level）があり、これは自然数です。 Sort 演算子は与えられたレベルから宇宙を構築します。 ある宇宙レベルが他の宇宙レベルよりも小さい場合、その宇宙自体も小さいと言います。命題を除いて（この章で後述）、与えられた宇宙内の型はより小さい宇宙内の型に対してのみ量化することができます。 Sort 0 は命題の型であり、各 Sort (u + 1) はデータを記述する型です。

すべての宇宙は1つ大きな宇宙の要素であるため、 Sort 5 は Sort 4 を含みます。つまり、以下の例が受け入れられます：

example : Sort 5 := Sort 4 example : Sort 2 := Sort 1

一方で、 Sort 3 は Sort 5 の要素ではありません：

example : Sort 5 := type mismatch Type 2 has type Type 3 : Type 4 but is expected to have type Type 4 : Type 5Sort 3 
type mismatch
  Type 2
has type
  Type 3 : Type 4
but is expected to have type
  Type 4 : Type 5

同様に、 Unit は Sort 1 に存在するため、 Sort 2 には存在しません：

example : Sort 1 := Unit example : Sort 2 := type mismatch Unit has type Type : Type 1 but is expected to have type Type 1 : Type 2Unit 
type mismatch
  Unit
has type
  Type : Type 1
but is expected to have type
  Type 1 : Type 2

命題とデータは異なる使われ方をし、異なる規則に支配されるため、より便利に区別するために Type と Prop という省略形が用意されています。 Type u は Sort (u + 1) の省略形であるため、 Type 0 は Sort 1 で Type 3 は Sort 4 です。 Type 0 は Type と省略することもできるため、 Unit : Type および Type : Type 1 です。 Prop は Sort 0 の省略形です。

3.3.1. 可述性（Predicativity）

各宇宙は依存関数型を含んでいます。依存関数はさらに全称量化子と含意を表します。関数型の宇宙は、引数の型と戻り値の型の宇宙によって決定されます。具体的な規則は、関数の戻り値が命題かどうかに依存します。

命題を返す関数である述語（つまり、関数の結果が Prop にある型である場合）は引数の型がどのような宇宙に存在しても構いませんが、関数の型自体は Prop に留まります。言い換えると、命題は 非可述 （impredicative） な量化子を特徴づけます。というのも、命題はそれ自体、すべての命題（および他のすべての命題）についての文になりうるからです。

非可述性

証明の irrelevance はすべての命題を量化する命題として書くことができます：

example : Prop := ∀ (P : Prop) (p1 p2 : P), p1 = p2

命題はまた任意のレベルにおいてすべての型を量化することもできます：

example : Prop := ∀ (α : Type), ∀ (x : α), x = x example : Prop := ∀ (α : Type 5), ∀ (x : α), x = x

レベル 1 以上の宇宙（つまり、Type u の階層）では、量化子は 可述 （predicative）です。 これらの宇宙では、関数型の宇宙は引数の型と戻り値の型の宇宙の最小上界となります。

関数型の宇宙レベル

これらの型はどちらも Type 2 に存在します：

example (α : Type 1) (β : Type 2) : Type 2 := α → β example (α : Type 2) (β : Type 1) : Type 2 := α → β
Type の Predicativity

α のレベルは 1 より大きいため、この例は許可されません。言い換えると、注釈された宇宙は実際の関数型の宇宙よりも小さいです：

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 の宇宙は cumulative ではありません； これは Type u の型が自動的に Type (u + 1) にも存在するようにならないことを意味します。各型は正確に1つの宇宙に属します。

cumulativity ではない

この例は注釈された宇宙が関数型の宇宙よりも大きいため、許可されません：

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 は 宇宙多相 （universe polymorphism）をサポートしており、Lean の環境で定義された定数は 宇宙パラメータ （universe parameter）を取ることができます。これらのパラメータはその定数が使用されるときに宇宙レベルでインスタンス化されます。宇宙パラメータは定数名の後のドットに続く波括弧で記述します。

宇宙多相恒等関数

完全に明示的にすると、恒等関数は宇宙パラメータ u を取ります。このシグネチャは以下になります：

id.{u} {α : Sort u} (x : α) : α

宇宙変数はさらに、定義の中で特定の宇宙レベルを提供する 宇宙レベル式 の中で出現させることができます。多相定義が具体的なレベルでインスタンス化されるとき、これらの宇宙レベル式も具体的なレベルをもたらすために評価されます。

宇宙レベル式

この例では、 Codec はそれが含む型の宇宙より1つ大きい宇宙に存在します：

structure Codec.{u} : Type (u + 1) where type : Type u encode : Array UInt32 → type → Array UInt32 decode : Array UInt32 → Nat → Option (type × Nat)

Lean はほとんどのレベルパラメータを自動的に推論します。以下の例では、 Char の型は Type 0 であるため、u は 0 でなければならないことから、 Codec.{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

宇宙多相な定義は、実際には様々なレベルでインスタンス可能な スキーマ的定義 （schematic definition）を作り出し、宇宙レベルの異なるインスタンス化は互換性のない値を作ります。

宇宙多相と definitional equality

これは次の例で見ることができます。 T は不必要に宇宙多相な定義で、常に true を返します。 Lean.Parser.Command.declaration : commandopaque とマークされているため、Lean は T の定義を展開して等価性をチェックすることができません。 T のインスタンスはどれもパラメータと同じ型を持ちますが、宇宙のインスタンス化が異なるため互換性がありません：

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

自動的に束縛される暗黙の引数は可能な限り宇宙多相となります。恒等関数を次のように定義します：

def id' (x : α) := x

これは以下のシグネチャになります：

id'.{u} {α : Sort u} (x : α) : α
自動的に束縛された暗黙のパラメータを持つ宇宙のモノ射

一方、 Nat は Type 0 に存在するため、この関数は自動的に α の具体的な宇宙レベルを求めます。m は Nat と α の両方に適用されるため、どちらも同じ型を持たなければならず、結果として同じ宇宙となります：

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）🔗

定義に現れるレベルは変数と定数の加算だけに限定されません。より複雑な宇宙間の関係もレベルの表現を使って定義できます。

Level ::= 0 | 1 | 2 | ...  -- 具体的なレベル
        | u, v             -- 変数
        | Level + n        -- 定数の加算
        | max Level Level  -- 最小上界
        | imax Level Level -- 非可述な最小上界

レベル変数が具体的な数値に割り当てられている場合、これらの式の評価は通常の算術の規則に従います。imax 演算は以下のように定義されます：

\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}

imax は Prop に対する 非可述 な量化子を実装するために使用されます。具体的には、A : Sort u かつ B : Sort v である場合、(x : A) → B : Sort (imax u v) となります。もし B : Prop ならば、その関数型は Prop であり、それ以外ではその関数型のレベルは u と v の最大値になります。

3.3.2.2. 宇宙変数の束縛（Universe Variable Bindings）

宇宙多相定義は宇宙変数を束縛します。これらの束縛は明示的・暗黙的のどちらも可能です。明示的な宇宙変数の束縛とインスタンス化は定義の名前の接尾辞として出現します。宇宙パラメータは定数名にピリオド（.）を接尾辞として付け、その後に波括弧の間にカンマで区切られた一連の宇宙変数を付けることで定義・提供されます。

宇宙多相な map

以下 map の宣言では、2つの宇宙パラメータ（u と v）を宣言し、多相型の List を順番にインスタンス化しています：

def map.{u, v} {α : Type u} {β : Type v} (f : α → β) : List.{u} α → List.{v} β | [] => [] | x :: xs => f x :: map f xs

Lean が暗黙のパラメータを自動的にインスタンス化するように、宇宙パラメータも自動的にインスタンス化されます。autoImplicit オプションが true に設定されている場合（デフォルト）、宇宙変数を明示的に束縛する必要はありません。 false に設定すると、明示的に追加するか universe コマンドを使って宣言する必要があります。

自動的な暗黙と宇宙多相

autoImplicit が true （デフォルト値）の場合、この定義は宇宙パラメータを束縛していなくても許可されます：

set_option autoImplicit true def map {α : Type u} {β : Type v} (f : α → β) : List α → List β | [] => [] | x :: xs => f x :: map f xs

autoImplicit が false の場合、u と v がスコープにないためこの定義は却下されます：

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'

autoImplicit を使うことに加えて、universe コマンドを使って特定の識別子を特定の セクションスコープ 内の宇宙変数として宣言することができます。

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)
```
universe ident ident*

現在のスコープの範囲において1つ以上の宇宙変数を宣言します。

variable コマンドが特定の識別子を特定の型のパラメータとして扱うように、universe コマンドは autoImplicit オプションが false であっても、それに続く識別子を宇宙パラメータとして暗黙的に量化します。

autoImplicit が false の際の universe コマンドset_option autoImplicit false universe u def id₃ (α : Type u) (a : α) := a

自動的な暗黙のパラメータ機能は宣言の ヘッダ で使用されるパラメータのみを挿入するため、定義の右側にのみ現れる宇宙変数は autoImplicit が true の場合でも universe で宣言されていない限り引数として挿入されません。

自動的な宇宙パラメータと universe コマンド

明示的な宇宙パラメータを伴ったこの定義は許可されます：

def L.{u} := List (Type u)

u が := の前にあるヘッダで言及されていないため、自動的な暗黙のパラメータでもこの定義は却下されます：

set_option autoImplicit true def L := List (Type unknown universe level 'u'u) 
unknown universe level 'u'

宇宙宣言では、u は右辺でもパラメータとして許可されます：

universe u def L := List (Type u)

その結果、L の定義は宇宙パラメータとして u が挿入された宇宙多相となります。

universe コマンドのスコープにある宣言は、その中に宇宙変数が無い場合、または自動的に挿入される他の引数の中に宇宙変数が無い場合、多相にはなりません。

universe u def L := List (Type 0) L : Type 1#check L

3.3.2.3. Universe Unification

Planned Content

  • Rules for unification, properties of algorithm

  • Lack of injectivity

  • Universe inference for unannotated inductive types

Tracked at issue #99

3.3.2.4. Universe Lifting

Planned Content

  • When to use universe lifting?

Tracked at issue #174

🔗structure
PLift.{u} (α : Sort u) : Type u

Universe lifting operation from Sort u to Type u.

Constructor

PLift.up.{u}

Lift a value into PLift α

Fields

down : α

Extract a value from PLift α

🔗structure
ULift.{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 α