predicative, impredicative対応

Author: s-taiga

GLOSSARY.md

@@ -126,6 +126,7 @@
 | immediate value | 即値 | |
 | imperative | 命令型 | |
 | implicit parameter | 暗黙のパラメータ | |
+| impredicative | 非可述 | |
 | impredicativity | 非可述性 | |
 | inaccessible | （仮定のアクセス可否の文脈で）アクセス不能 | |
 | incompatible | 互換性 | |
@@ -206,6 +207,7 @@
 | polymorphic | 多相 | |
 | precedence | 優先順位 | 構文解析・演算子等の優先具合を指す |
 | predicate | 述語 | |
+| predicative | 可述 | |
 | predicativity | 可述性 | |
 | pretty printer | プリティプリンタ | |
 | primitive | プリミティブ | |

Manual/Elaboration.lean

@@ -297,8 +297,8 @@ The language implemented by the kernel is a version of the Calculus of Construct
 カーネルが実装する言語は Calculus of Constructions の一種で、以下の特徴を持つ依存型理論です：
 + 完全な依存型
 + 相互に帰納的であったり、他の帰納型の下で入れ子になった再帰を含んだりする帰納的に定義されたデータ型
-+ {tech}[impredicative] ・定義上証明と irrelevant な {tech}[命題] の拡張的 {tech}[宇宙]
-+ {tech}[predicative] なデータの宇宙の非蓄積な階層
++ {tech}[非可述] ・定義上証明と irrelevant な {tech}[命題] の拡張的 {tech}[宇宙]
++ {tech}[可述] なデータの宇宙の非蓄積な階層
 * 定義上の計算規則を伴った {ref "quotients"}[商型] （Quotient type）
 + 命題上の関数外延性 {margin}[関数外延性は商型を使って証明できる定理ですが、重要な帰結であるため別で挙げておきます。]
 + 関数と積についての定義上のη等価性

Manual/Language/InductiveTypes/LogicalModel.lean

@@ -464,7 +464,7 @@ If the universe is not {lean}`Prop`, then the following must hold for each param
 
 :::
 
-帰納型の型コンストラクタは {tech}[宇宙] か戻り値が宇宙である関数型のどちらかに属さなければなりません。各コンストラクタは帰納型の完全な適用を返す関数型に属さなければなりません。もし帰納型の宇宙が {lean}`Prop` であれば、 {lean}`Prop` は {tech}[impredicative] であるため宇宙にはそれ以上の制限はありません。もし宇宙が {lean}`Prop` でない場合、コンストラクタの各パラメータについて以下が成り立つ必要があります：
+帰納型の型コンストラクタは {tech}[宇宙] か戻り値が宇宙である関数型のどちらかに属さなければなりません。各コンストラクタは帰納型の完全な適用を返す関数型に属さなければなりません。もし帰納型の宇宙が {lean}`Prop` であれば、 {lean}`Prop` は {tech}[非可述] であるため宇宙にはそれ以上の制限はありません。もし宇宙が {lean}`Prop` でない場合、コンストラクタの各パラメータについて以下が成り立つ必要があります：
  * コンストラクタのパラメータが（パラメータか添字かの意味で）帰納型のパラメータである場合、このパラメータの型は型コンストラクタの宇宙より大きくはできません。
  * その他のすべてのコンストラクタのパラメータは型コンストラクタの宇宙より小さくなければなりません。
 

Manual/Types.lean

@@ -437,7 +437,7 @@ For these universes, the universe of a function type is the least upper bound of
 
 :::
 
-{tech key:="universe level"}[レベル] `1` 以上の宇宙（つまり、`Type u` の階層）では、量化子は {deftech}[_predicative_] です。 {index}[predicative]{index subterm := "predicative"}[quantification] これらの宇宙では、関数型の宇宙は引数の型と戻り値の型の宇宙の最小上界となります。
+{tech key:="universe level"}[レベル] `1` 以上の宇宙（つまり、`Type u` の階層）では、量化子は {deftech}[_可述_] です。 {index}[predicative]{index subterm := "predicative"}[quantification] これらの宇宙では、関数型の宇宙は引数の型と戻り値の型の宇宙の最小上界となります。
 
 :::comment
 ::Manual.example "Universe levels of function types"
@@ -710,7 +710,7 @@ Level ::= 0 | 1 | 2 | ...  -- 具体的なレベル
         | u, v             -- 変数
         | Level + n        -- 定数の和
         | max Level Level  -- 最小上界
-        | imax Level Level -- Impredicative な最小上界
+        | imax Level Level -- 非可述な最小上界
 ````
 
 :::comment
@@ -730,7 +730,7 @@ If `B : Prop`, then the function type is itself a {lean}`Prop`; otherwise, the f
 
 :::
 
-`imax` は {lean}`Prop` の {tech}[impredicative] な量化子を実装するために使用されます。特に、`A : Sort u` かつ `B : Sort v` である場合、`(x : A) → B : Sort (imax u v)` となります。もし `B : Prop` ならば、その関数型は {lean}`Prop` であり、それ以外ではその関数型のレベルは `u` と `v` の最大値になります。
+`imax` は {lean}`Prop` の {tech}[非可述] な量化子を実装するために使用されます。特に、`A : Sort u` かつ `B : Sort v` である場合、`(x : A) → B : Sort (imax u v)` となります。もし `B : Prop` ならば、その関数型は {lean}`Prop` であり、それ以外ではその関数型のレベルは `u` と `v` の最大値になります。
 
 :::comment
 ### Universe Variable Bindings