diff --git a/GLOSSARY.md b/GLOSSARY.md
index 752eff5..e1e4dcd 100644
--- a/GLOSSARY.md
+++ b/GLOSSARY.md
@@ -293,6 +293,7 @@
 | underscore | アンダースコア | |
 | unification | 単一化 | |
 | union | 合併 | |
+| unit-like type | unit-like 型 | |
 | unit type | ユニット型 | |
 | universe | 宇宙 | |
 | universe level | 宇宙レベル | |
diff --git a/Manual.lean b/Manual.lean
index f90c9c9..686549e 100644
--- a/Manual.lean
+++ b/Manual.lean
@@ -170,7 +170,7 @@ file := some "the-index"
 
 翻訳に際して、機械翻訳サービス [DeepL翻訳](https://www.deepl.com/ja/translator) を参考にしました。
 
-この翻訳は原文のcommit [ade9c553a5ab008113cf33f88ced657c5146fe24](https://github.com/leanprover/reference-manual/commit/ade9c553a5ab008113cf33f88ced657c5146fe24) に基づいています。
+この翻訳は原文のcommit [27f733b339554f1cc0b3b70e9ca3054397075b97](https://github.com/leanprover/reference-manual/commit/27f733b339554f1cc0b3b70e9ca3054397075b97) に基づいています。
 
 ::::::draft
 
diff --git a/Manual/BasicTypes.lean b/Manual/BasicTypes.lean
index 5e416b3..7e5c776 100644
--- a/Manual/BasicTypes.lean
+++ b/Manual/BasicTypes.lean
@@ -202,44 +202,94 @@ tag := "char-api-classes"
 
 {include 0 Manual.BasicTypes.String}
 
+# ユニット型（The Unit Type）
+
+:::comment
 # The Unit Type
+:::
 
+:::comment
 The unit type is the least informative type.
 It is used when a value is needed, but no further information is relevant.
 There are two varieties of the unit type:
 
+:::
+
+ユニット型は最も情報量の少ない型です。これは、値は必要だがそれ以上の情報は必要ない場合に使用されます。ユニット型には2種類あります：
+
+:::comment
  * {lean}`Unit` is a {lean}`Type` that exists in the smallest non-propositional {tech}[universe].
 
+:::
+
+ * {lean}`Unit` は {lean}`Type` であり、最小の非命題 {tech}[宇宙] に存在します。
+
+:::comment
  * {lean}`PUnit` is {tech key:="universe polymorphism"}[universe polymorphic] and can be used in any non-propositional {tech}[universe].
 
+:::
+
+ * {lean}`PUnit` は {tech}[宇宙多相] であり、任意の非命題 {tech}[宇宙] で使用することができます。
+
+:::comment
 If in doubt, use {lean}`Unit` until universe errors occur.
 
+:::
+
+悩ましい場合は、宇宙に関するエラーが発生するまでは {lean}`Unit` を使ってください。
+
 {docstring Unit}
 
 {docstring Unit.unit}
 
 {docstring PUnit}
 
+:::comment
 ## Definitional Equality
+:::
+
+## 定義上の等価性（Definitional Equality）
 
+
+:::comment
 {deftech}_Unit-like types_ are inductive types that have a single constructor which takes no non-proof parameters.
 {lean}`PUnit` is one such type.
 All elements of unit-like types are {tech key:="definitional equality"}[definitionally equal] to all other elements.
 
-:::example "Definitional Equality of {lean}`Unit`"
+:::
+
+{deftech}_unit-like 型_ （unit-like type）は非証明のパラメータを取らない単一のコンストラクタを持つ帰納型です。 {lean}`PUnit` はそのような型の1つです。unit-like 型のすべての要素は、他のすべての要素を {tech key:="定義上の等価性"}[定義上等しいです] 。
+
+:::comment
+::example "Definitional Equality of {lean}`Unit`"
+:::
+::::example "{lean}`Unit` の定義上の等価性"
+:::comment
 Every term with type {lean}`Unit` is definitionally equal to every other term with type {lean}`Unit`:
 
+:::
+
+{lean}`Unit` 型を持つすべての項は、 {lean}`Unit` 型を持つすべての項と定義上等しいです：
+
 ```lean
 example (e1 e2 : Unit) : e1 = e2 := rfl
 ```
-:::
+::::
 
-::::keepEnv
-:::example "Definitional Equality of Unit-Like Types"
+:::::keepEnv
+:::comment
+::example "Definitional Equality of Unit-Like Types"
+:::
+::::example "unit-like 型の定義上の等価性"
 
+:::comment
 Both {lean}`CustomUnit` and {lean}`AlsoUnit` are unit-like types, with a single constructor that takes no parameters.
 Every pair of terms with either type is definitionally equal.
 
+:::
+
+{lean}`CustomUnit` と {lean}`AlsoUnit` はどちらも unit-like 型であり、パラメータを取らないコンストラクタを1つ持ちます。どちらの型を持つ項のペアも定義上等しいです。
+
 ```lean
 inductive CustomUnit where
   | customUnit
@@ -251,8 +301,13 @@ structure AlsoUnit where
 example (e1 e2 : AlsoUnit) : e1 = e2 := rfl
 ```
 
+:::comment
 Types with parameters, such as {lean}`WithParam`, are also unit-like if they have a single constructor that does not take parameters.
 
+:::
+
+{lean}`WithParam` のようなパラメータを持つ型も、パラメータを取らないコンストラクタが1つあれば unit-like です。
+
 ```lean
 inductive WithParam (n : Nat) where
   | mk
@@ -260,7 +315,12 @@ inductive WithParam (n : Nat) where
 example (x y : WithParam 3) : x = y := rfl
 ```
 
+:::comment
 Constructors with non-proof parameters are not unit-like, even if the parameters are all unit-like types.
+:::
+
+証明ではないパラメータを持つコンストラクタは、パラメータがすべて unit-like 型であっても unit-like になりません。
+
 ```lean
 inductive NotUnitLike where
   | mk (u : Unit)
@@ -278,15 +338,20 @@ but is expected to have type
   e1 = e2 : Prop
 ```
 
+:::comment
 Constructors of unit-like types may take parameters that are proofs.
+:::
+
+unit-like 型のコンストラクタは証明であるパラメータを取ることができます。
+
 ```lean
 inductive ProofUnitLike where
   | mk : 2 = 2 → ProofUnitLike
 
 example (e1 e2 : ProofUnitLike) : e1 = e2 := rfl
 ```
-:::
 ::::
+:::::
 
 # The Empty Type
 
@@ -300,24 +365,54 @@ example (e1 e2 : ProofUnitLike) : e1 = e2 := rfl
 
 {docstring PEmpty}
 
+:::comment
 # Booleans
+:::
+
+# 真偽値（Booleans）
+
 
 {docstring Bool}
 
+:::comment
 The constructors {lean}`Bool.true` and {lean}`Bool.false` are exported from the {lean}`Bool` namespace, so they can be written {lean}`true` and {lean}`false`.
 
+:::
+
+コンストラクタ {lean}`Bool.true` と {lean}`Bool.false` は {lean}`Bool` 名前空間からエクスポートされるため、 {lean}`true` と {lean}`false` と書くことができます。
+
+:::comment
 ## Run-Time Representation
+:::
+
+## ランタイム表現（Run-Time Representation）
+
 
+:::comment
 Because {lean}`Bool` is an {tech}[enum inductive] type, it is represented by a single byte in compiled code.
 
+:::
+
+{lean}`Bool` は {tech}[列挙帰納的] 型であるため、コンパイルされたコードでは1バイトで表現されます。
+
+:::comment
 ## Booleans and Propositions
+:::
+
+## 真偽値と命題（Booleans and Propositions）
+
 
+:::comment
 Both {lean}`Bool` and {lean}`Prop` represent notions of truth.
 From a purely logical perspective, they are equivalent: {tech}[propositional extensionality] means that there are fundamentally only two propositions, namely {lean}`True` and {lean}`False`.
 However, there is an important pragmatic difference: {lean}`Bool` classifies _values_ that can be computed by programs, while {lean}`Prop` classifies statements for which code generation doesn't make sense.
 In other words, {lean}`Bool` is the notion of truth and falsehood that's appropriate for programs, while {lean}`Prop` is the notion that's appropriate for mathematics.
 Because proofs are erased from compiled programs, keeping {lean}`Bool` and {lean}`Prop` distinct makes it clear which parts of a Lean file are intended for computation.
 
+:::
+
+{lean}`Bool` と {lean}`Prop` はどちらも真理の概念を表します。純粋論理の観点から見ると、両者は同等です： {tech}[propositional extensionality] は基本的に2つの命題、すなわち {lean}`True` と {lean}`False` しか存在しないことを意味します。しかし、実用上は重要な違いがあります： {lean}`Bool` はプログラムで計算できる _値_ を分類し、 {lean}`Prop` はコード生成が意味を為さない文を分類します。言い換えると、 {lean}`Bool` はプログラムに適した真偽の概念であり、 {lean}`Prop` は数学に適した概念です。コンパイルされたプログラムから証明は消去されるため、 {lean}`Bool` と {lean}`Prop` を区別しておくことで Lean ファイルのどの部分が計算を目的としているかが明確になります。
+
 ```lean (show := false)
 section BoolProp
 
@@ -332,10 +427,16 @@ example : (true = true) = True := by simp
 #check decide
 ```
 
+:::comment
 A {lean}`Bool` can be used wherever a {lean}`Prop` is expected.
 There is a {tech}[coercion] from every {lean}`Bool` {lean}`b` to the proposition {lean}`b = true`.
 By {lean}`propext`, {lean}`true = true` is equal to {lean}`True`, and {lean}`false = true` is equal to {lean}`False`.
 
+:::
+
+{lean}`Bool` は {lean}`Prop` が期待されているところではどこでも使うことができます。すべての {lean}`Bool` {lean}`b` から命題 {lean}`b = true` への {tech}[coercion] が存在します。 {lean}`propext` により、 {lean}`true = true` は {lean}`True` に、 {lean}`false = true` は {lean}`False` にそれぞれ等しいです。
+
+:::comment
 Not every proposition can be used by programs to make run-time decisions.
 Otherwise, a program could branch on whether the Collatz conjecture is true or false!
 Many propositions, however, can be checked algorithmically.
@@ -343,6 +444,10 @@ These propositions are called {tech}_decidable_ propositions, and have instances
 The function {name}`Decidable.decide` converts a proof-carrying {lean}`Decidable` result into a {lean}`Bool`.
 This function is also a coercion from decidable propositions to {lean}`Bool`, so {lean}`(2 = 2 : Bool)` evaluates to {lean}`true`.
 
+:::
+
+全ての命題をプログラムがランタイム時の判断に使えるわけではありません。そうでなければコラッツ予想が真か偽かでプログラムが分岐してしまいます！しかし、多くの命題はアルゴリズムでチェックすることができます。これらの命題は {tech}_決定可能_ な命題と呼ばれ、 {lean}`Decidable` 型クラスを持ちます。関数 {name}`Decidable.decide` は証明を格納した {lean}`Decidable` の結果を {lean}`Bool` に変換します。この関数は決定可能な命題から {lean}`Bool` への強制演算でもあるため、 {lean}`(2 = 2 : Bool)` は {lean}`true` と評価されます。
+
 ```lean (show := false)
 /-- info: true -/
 #guard_msgs in
@@ -350,11 +455,21 @@ This function is also a coercion from decidable propositions to {lean}`Bool`, so
 end BoolProp
 ```
 
+:::comment
 ## Syntax
+:::
+
+## 構文（Syntax）
 
-:::syntax term
+
+::::syntax term
+:::comment
 The infix operators `&&`, `||`, and `^^` are notations for {lean}`Bool.and`, {lean}`Bool.or`, and {lean}`Bool.xor`, respectively.
 
+:::
+
+中置演算子 `&&` ・ `||` ・ `^^` はそれぞれ {lean}`Bool.and` ・ {lean}`Bool.or` ・ {lean}`Bool.xor` の表記です。
+
 ```grammar
 $_:term && $_:term
 ```
@@ -364,19 +479,34 @@ $_:term || $_:term
 ```grammar
 $_:term ^^ $_:term
 ```
-:::
+::::
 
-:::syntax term
+::::syntax term
+:::comment
 The prefix operator `!` is notation for {lean}`Bool.not`.
+:::
+
+前置演算子 `!` は {lean}`Bool.not` の表記です。
+
 ```grammar
 !$_:term
 ```
-:::
+::::
 
 
+:::comment
 ## API Reference
+:::
 
+## API リファレンス（API Reference）
+
+
+:::comment
 ### Logical Operations
+:::
+
+### 論理演算子（Logical Operations）
+
 
 ```lean (show := false)
 section ShortCircuit
@@ -384,10 +514,15 @@ section ShortCircuit
 axiom BIG_EXPENSIVE_COMPUTATION : Bool
 ```
 
+:::comment
 The functions {name}`cond`, {name Bool.and}`and`, and {name Bool.or}`or` are short-circuiting.
 In other words, {lean}`false && BIG_EXPENSIVE_COMPUTATION` does not need to execute {lean}`BIG_EXPENSIVE_COMPUTATION` before returning `false`.
 These functions are defined using the {attr}`macro_inline` attribute, which causes the compiler to replace calls to them with their definitions while generating code, and the definitions use nested pattern matching to achieve the short-circuiting behavior.
 
+:::
+
+関数 {name}`cond` ・ {name Bool.and}`and` ・ {name Bool.or}`or` は短絡します。つまり、 {lean}`false && BIG_EXPENSIVE_COMPUTATION` は `false` を返す前に {lean}`BIG_EXPENSIVE_COMPUTATION` を実行する必要はありません。これらの関数は {attr}`macro_inline` 属性を使用して定義されています。これによりコンパイラはコードを生成する際に関数の呼び出しを定義に置き換え、入れ子のパターンマッチを用いる定義が短絡評価されるようになります。
+
 ```lean (show := false)
 end ShortCircuit
 ```
@@ -405,11 +540,21 @@ end ShortCircuit
 
 {docstring Bool.atLeastTwo}
 
+:::comment
 ### Comparisons
+:::
+
+### 比較（Comparisons）
+
 
 {docstring Bool.decEq}
 
+:::comment
 ### Conversions
+:::
+
+### 変換（Conversions）
+
 
 {docstring Bool.toISize}
 
diff --git a/Manual/Classes/BasicClasses.lean b/Manual/Classes/BasicClasses.lean
index 7ebc344..140fdbf 100644
--- a/Manual/Classes/BasicClasses.lean
+++ b/Manual/Classes/BasicClasses.lean
@@ -56,13 +56,13 @@ Lean の型クラスの多くは、加算や配列インデックスのような
 
 :::comment
 # Decidability
-%%%
-tag := "decidable-propositions"
-%%%
 
 :::
 
 # 決定可能性（Decidability）
+%%%
+tag := "decidable-propositions"
+%%%
 
 :::comment
 A proposition is {deftech}_decidable_ if it can be checked algorithmically.{index}[decidable]{index subterm:="decidable"}[proposition]
diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean
index d23469f..ead55ff 100644
--- a/Manual/Elaboration.lean
+++ b/Manual/Elaboration.lean
@@ -431,7 +431,7 @@ To provide a uniform interface to functions defined via structural and well-foun
 In the function's namespace, `eq_unfold` relates the function directly to its definition, `eq_def` relates it to the definition after instantiating implicit parameters, and $`N` lemmas `eq_N` relate each case of its pattern-matching to the corresponding right-hand side, including sufficient assumptions to indicate that earlier branches were not taken.
 :::
 
-構造的に単純な再帰関数の場合、その翻訳は型の再帰子を使用します。このような関数はカーネルで実行すると比較的効率的である傾向があり、定義された等式が定義上成立し、理解も容易です。型の再帰子で捕捉できないその他のパターンの再帰を使用する関数は {deftech}[整礎再帰] （well-founded recursion）を使用して翻訳されます。これは各再帰呼び出しのたびに何かしらの基準が減少することの証明のもとの構造的な再帰です。Lean はこれらのケースの多くを自動的に導出できますが、手作業での証明が必要なものもあります。整礎再帰はより柔軟なものですが、基準が減少することを示す証明項が定義する等式が成立するのは命題上だけであるため、結果として得られる関数はカーネルでの実行速度が遅くなることが多いです。構造的で整礎な再帰によって定義された関数に統一されたインタフェースを提供し、それ自身の正しさをチェックするために、エラボレータは関数をもとの定義に関連付ける等式の補題を証明します。関数の名前空間において、`eq_unfold` は関数を直接定義に関連付け、`eq_def` は暗黙のパラメータをインスタンス化した後の定義に関連付け、 $`N` 個の補題 `eq_N` はパターンマッチの各ケースと対応する右辺を関連付けます。これにはそれより前の分岐が取られないことの十分な仮定を含みます。
+構造的に単純な再帰関数の場合、その翻訳は型の再帰子を使用します。このような関数はカーネルで実行すると比較的効率的である傾向があり、定義された等式が定義上成立し、理解も容易です。型の再帰子で捕捉できないその他のパターンの再帰を使用する関数は {deftech}[整礎再帰] （well-founded recursion）を使用して翻訳されます。これは各再帰呼び出しのたびに何かしらの {deftech}_測度_ （measure）が減少することの証明のもとの構造的な再帰です。Lean はこれらのケースの多くを自動的に導出できますが、手作業での証明が必要なものもあります。整礎再帰はより柔軟なものですが、基準が減少することを示す証明項が定義する等式が成立するのは命題上だけであるため、結果として得られる関数はカーネルでの実行速度が遅くなることが多いです。構造的で整礎な再帰によって定義された関数に統一されたインタフェースを提供し、それ自身の正しさをチェックするために、エラボレータは関数をもとの定義に関連付ける等式の補題を証明します。関数の名前空間において、`eq_unfold` は関数を直接定義に関連付け、`eq_def` は暗黙のパラメータをインスタンス化した後の定義に関連付け、 $`N` 個の補題 `eq_N` はパターンマッチの各ケースと対応する右辺を関連付けます。これにはそれより前の分岐が取られないことの十分な仮定を含みます。
 
 :::::keepEnv
 :::comment
diff --git a/Manual/IO.lean b/Manual/IO.lean
index fc2f915..59cd8fa 100644
--- a/Manual/IO.lean
+++ b/Manual/IO.lean
@@ -32,7 +32,7 @@ tag := "io"
 
 
 Lean is a pure functional programming language.
-While Lean code is strictly evaluated at run time, the order of evaluation that is used during type checking, especially while checking {tech}[definitional equality], is formally unspecified and makes use of a number of heuristics that improve performance but are subject to change.
+While Lean code is strictly evaluated at run time, the order of evaluation that is used during type checking, especially while checking {tech}[定義上の等価性]definitional equality, is formally unspecified and makes use of a number of heuristics that improve performance but are subject to change.
 This means that simply adding operations that perform side effects (such as file I/O, exceptions, or mutable references) would lead to programs in which the order of effects is unspecified.
 During type checking, even terms with free variables are reduced; this would make side effects even more difficult to predict.
 Finally, a basic principle of Lean's logic is that functions are _functions_ that map each element of the domain to a unique element of the range.
@@ -129,7 +129,7 @@ example : BaseIO = EIO Empty := rfl
 ## Errors and Error Handling
 
 Error handling in the {lean}`IO` monad uses the same facilities as any other {tech}[exception monad].
-In particular, throwing and catching exceptions uses the methods of the {name}`MonadExceptOf` {tech}[type class].
+In particular, throwing and catching exceptions uses the methods of the {name}`MonadExceptOf` {tech}[型クラス]type class.
 The exceptions thrown in {lean}`IO` have the type {lean}`IO.Error`.
 The constructors of this type represent the low-level errors that occur on most operating systems, such as files not existing.
 The most-used constructor is {name IO.Error.userError}`userError`, which covers all other cases and includes a string that describes the problem.
diff --git a/Manual/Language.lean b/Manual/Language.lean
index 16d0280..f45fe31 100644
--- a/Manual/Language.lean
+++ b/Manual/Language.lean
@@ -32,13 +32,13 @@ set_option linter.unusedVariables false
 {include 0 Manual.Language.Files}
 
 
+# モジュールの内容（Module Contents）
+
 :::comment
 # Module Contents
 
 :::
 
-# モジュールの内容（Module Contents）
-
 :::comment
 As described {ref "module-structure"}[in the section on the syntax of files], a Lean module consists of a header followed by a sequence of commands.
 
diff --git a/Manual/Language/Functions.lean b/Manual/Language/Functions.lean
index 0e6c84e..2a18d65 100644
--- a/Manual/Language/Functions.lean
+++ b/Manual/Language/Functions.lean
@@ -317,7 +317,7 @@ The values of total functions are defined for all type-correct arguments, and th
 
 :::
 
-関数は {keywordOf Lean.Parser.Command.declaration}`def` を使って再帰的に定義することができます。Lean の論理の観点から、すべての関数は {deftech}_全域_ （total）です。これは関数が定義域の各要素を値域の要素に有限時間でマッピングすることを意味します。 {margin}[プログラミング言語のコミュニティによっては、より限定的な意味で _全域_ という用語を使用するものもあり、その場合、関数はクラッシュしなければ全域と見なされますが、非停止は無視されます。] 全域関数の値はすべての型が正しい引数に対して定義され、パターンマッチでケースが漏れて停止に失敗したりクラッシュしたりすることはありません。
+関数は {keywordOf Lean.Parser.Command.declaration}`def` を使って再帰的に定義することができます。Lean の論理の観点から、すべての関数は {deftech}_全域_ （total）です。これは関数が定義域の各要素を値域の要素に有限時間でマッピングすることを意味します。 {margin}[プログラミング言語のコミュニティによっては、異なる意味で _全域_ という用語を使用するものもあり、その場合、関数がハンドルされていないケースによってクラッシュしなければ全域と見なされますが、非停止は無視されます。] 全域関数の値はすべての型が正しい引数に対して定義され、パターンマッチでケースが漏れて停止に失敗したりクラッシュしたりすることはありません。
 
 :::comment
 While the logical model of Lean considers all functions to be total, Lean is also a practical programming language that provides certain "escape hatches".
diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean
index 1ad5295..bc22e79 100644
--- a/Manual/Language/InductiveTypes.lean
+++ b/Manual/Language/InductiveTypes.lean
@@ -169,7 +169,7 @@ Type constructors with indices are said to specify {deftech}_indexed families_ {
 
 :::
 
-添字は型の _族_ （family）を定義していると見なすことができます。添字を選択するごとに、その族から型が選択され、その型は使用可能なコンストラクタのあつまりを持ちます。添字のパラメータを取る型のコンストラクタは {deftech}_添字族_ {index subterm:="of types"}[indexed family] （indexed family）と呼ばれます、
+添字は型の _族_ （family）を定義していると見なすことができます。添字を選択するごとに、その族から型が選択され、その型は使用可能なコンストラクタのあつまりを持ちます。添字を持つ型のコンストラクタは {deftech}_添字族_ {index subterm:="of types"}[indexed family] （indexed family）の型を指定すると言われます。
 
 :::comment
 ## Example Inductive Types
@@ -477,7 +477,7 @@ Providing arguments by name or converting all implicit parameters to explicit pa
 
 :::
 
-帰納型がコンストラクタを1つだけ持つ場合、このコンストラクタは {deftech}_匿名コンストラクタ構文_ （anonymous constructor syntax）の対象となります。コンストラクタの名前を引数に適用して書く代わりに、明示的な引数を角括弧（`'⟨'` と `'⟩'`、Unicode `MATHEMATICAL LEFT ANGLE BRACKET	(U+0x27e8)` と `MATHEMATICAL RIGHT ANGLE BRACKET	(U+0x27e9)`）で囲み、カンマで区切ることができます。これはパターンと式の両方のコンテキストで動作します。引数を名前で指定したり、すべての暗黙的なパラメータを `@` で明示的なものに変換したりするには、通常のコンストラクタ構文を使用する必要があります。
+帰納型がコンストラクタを1つだけ持つ場合、このコンストラクタは {deftech}_匿名コンストラクタ構文_ （anonymous constructor syntax）の対象となります。コンストラクタの名前を引数に適用して書く代わりに、明示的な引数を角括弧（`'⟨'` と `'⟩'`、Unicode `MATHEMATICAL LEFT ANGLE BRACKET	(U+0x27e8)` と `MATHEMATICAL RIGHT ANGLE BRACKET	(U+0x27e9)`）で囲み、カンマで区切ることができます。これはパターンと式の両方のコンテキストで動作します。引数を名前で指定したり、すべての暗黙的なパラメータを `@` で明示的なパラメータに変換したりするには、通常のコンストラクタ構文を使用する必要があります。
 
 :::comment
 ::example "Anonymous constructors"
@@ -792,7 +792,7 @@ Lean assumes that `sizeof(size_t) == sizeof(void*)`—while this is not guarante
 
 :::
 
-C の観点では、これらの帰納型は `lean_object *` として表現されます。各コンストラクタは `lean_ctor_object` として格納され、`lean_is_ctor` は真を返します。`lean_ctor_object` はコンストラクタのインデックスをヘッダに格納し、フィールドはオブジェクトの `m_objs` 部分に格納されます。
+C の観点では、これらの帰納型は `lean_object *` として表現されます。各コンストラクタは `lean_ctor_object` として格納され、`lean_is_ctor` は真を返します。`lean_ctor_object` はコンストラクタのインデックスをヘッダに格納し、フィールドはオブジェクトの `m_objs` 部分に格納されます。Lean は `sizeof(size_t) == sizeof(void*)` を仮定しています。これは C では保証されていませんが、Lean のランタイムシステムには、これが当てはまらない場合に失敗するアサートが含まれています。
 
 :::comment
 The memory order of the fields is derived from the types and order of the fields in the declaration. They are ordered as follows:
diff --git a/Manual/Language/InductiveTypes/Structures.lean b/Manual/Language/InductiveTypes/Structures.lean
index 73ac092..f094935 100644
--- a/Manual/Language/InductiveTypes/Structures.lean
+++ b/Manual/Language/InductiveTypes/Structures.lean
@@ -380,7 +380,7 @@ Default arguments are still present in patterns; if a pattern does not specify a
 
 :::comment
 The optional type annotation allows the structure type to be specified in contexts where it is not otherwise determined.
-::::
+:::
 
 オプションで型注釈することによって、構造体型が他に決定されないコンテキストにおいて構造体型を指定することを可能にします。
 
diff --git a/Manual/Language/RecursiveDefs.lean b/Manual/Language/RecursiveDefs.lean
index fb9f8cb..221ff5a 100644
--- a/Manual/Language/RecursiveDefs.lean
+++ b/Manual/Language/RecursiveDefs.lean
@@ -21,10 +21,10 @@ tag := "recursive-definitions"
 %%%
 
 Allowing arbitrary recursive function definitions would make Lean's logic inconsistent.
-General recursion makes it possible to write circular proofs: "{tech}[proposition] $`P` is true because proposition $`P` is true".
+General recursion makes it possible to write circular proofs: "{tech}[命題]proposition $`P` is true because proposition $`P` is true".
 Outside of proofs, an infinite loop could be assigned the type {name}`Empty`, which can be used with {keywordOf Lean.Parser.Term.nomatch}`nomatch` or {name Empty.rec}`Empty.rec` to prove any theorem.
 
-Banning recursive function definitions outright would render Lean far less useful: {tech}[inductive types] are key to defining both predicates and data, and they have a recursive structure.
+Banning recursive function definitions outright would render Lean far less useful: {tech}[帰納型]inductive types are key to defining both predicates and data, and they have a recursive structure.
 Furthermore, most useful recursive functions do not threaten soundness, and infinite loops usually indicate mistakes in definitions rather than intentional behavior.
 Instead of banning recursive functions, Lean requires that each recursive function is defined safely.
 While elaborating recursive definitions, the Lean elaborator also produces a justification that the function being defined is safe.{margin}[The section on {ref "elaboration-results"}[the elaborator's output] in the overview of elaboration contextualizes the elaboration of recursive definitions in the overall context of the elaborator.]
@@ -33,15 +33,15 @@ There are four main kinds of recursive functions that can be defined:
 
 : Structurally recursive functions
 
-  Structurally recursive functions take an argument such that the function makes recursive calls only on strict sub-components of said argument.{margin}[Strictly speaking, arguments whose types are {tech}[indexed families] are grouped together with their indices, with the whole collection considered as a unit.]
-  The elaborator translates the recursion into uses of the argument's {tech}[recursor].
+  Structurally recursive functions take an argument such that the function makes recursive calls only on strict sub-components of said argument.{margin}[Strictly speaking, arguments whose types are {tech}[添字族]indexed families are grouped together with their indices, with the whole collection considered as a unit.]
+  The elaborator translates the recursion into uses of the argument's {tech}[再帰子]recursor.
   Because every type-correct use of a recursor is guaranteed to avoid infinite regress, this translation is evidence that the function terminates.
   Applications of functions defined via recursors are definitionally equal to the result of the recursion, and are typically relatively efficient inside the kernel.
 
 : Recursion over well-founded relations
 
   Many functions are also difficult to convert to structural recursion; for instance, a function may terminate because the difference between an array index and the size of the array decreases as the index increases, but {name}`Nat.rec` isn't applicable because the index that increases is the function's argument.
-  Here, there is a {tech}[measure] of termination that decreases at each recursive call, but the measure is not itself an argument to the function.
+  Here, there is a {tech}[測度]measure of termination that decreases at each recursive call, but the measure is not itself an argument to the function.
   In these cases, {tech}[well-founded recursion] can be used to define the function.
   Well-founded recursion is a technique for systematically transforming recursive functions with a decreasing measure into recursive functions over proofs that every sequence of reductions to the measure eventually terminates at a minimum.
   Applications of functions defined via well-founded recursion are not necessarily definitionally equal to their return values, but this equality can be proved as a proposition.
diff --git a/Manual/Language/RecursiveDefs/Structural.lean b/Manual/Language/RecursiveDefs/Structural.lean
index f84e2e7..316400a 100644
--- a/Manual/Language/RecursiveDefs/Structural.lean
+++ b/Manual/Language/RecursiveDefs/Structural.lean
@@ -37,7 +37,7 @@ Next, for each group of parameters, a translation using `brecOn` is attempted.
 {spliceContents Manual.Language.RecursiveDefs.Structural.CourseOfValuesExample}
 
 The `below` construction is a mapping from each value of a type to the results of some function call on _all_ smaller values; it can be understood as a memoization table that already contains the results for all smaller values.
-Recursors expect an argument for each of the inductive type's constructors; these arguments are called with the constructor's arguments (and the result of recursion on recursive parameters) during {tech}[ι-reduction].
+Recursors expect an argument for each of the inductive type's constructors; these arguments are called with the constructor's arguments (and the result of recursion on recursive parameters) during {tech}[ι簡約]ι-reduction.
 The course-of-values recursion operator `brecOn`, on the other hand, expects just a single case that covers all constructors at once.
 This case is provided with a value and a `below` table that contains the results of recursion on all values smaller than the given value; it should use the contents of the table to satisfy the motive for the provided value.
 If the function is structurally recursive over a given parameter (or parameter group), then the results of all recursive calls will be present in this table already.
diff --git a/Manual/Language/RecursiveDefs/Structural/CourseOfValuesExample.lean b/Manual/Language/RecursiveDefs/Structural/CourseOfValuesExample.lean
index dc3b05e..32bd571 100644
--- a/Manual/Language/RecursiveDefs/Structural/CourseOfValuesExample.lean
+++ b/Manual/Language/RecursiveDefs/Structural/CourseOfValuesExample.lean
@@ -30,7 +30,7 @@ theorem List.below_eq_below' : @List.below = @List.below' := by
   congr
 ```
 
-In other words, for a given {tech}[motive], {lean}`List.below'` is a type that contains a realization of the motive for all suffixes of the list.
+In other words, for a given {tech}[動機]motive, {lean}`List.below'` is a type that contains a realization of the motive for all suffixes of the list.
 
 More recursive arguments require further nested iterations of the product type.
 For instance, binary trees have two recursive occurrences.
diff --git a/Manual/Monads/Syntax.lean b/Manual/Monads/Syntax.lean
index 7ecd510..73a1f2c 100644
--- a/Manual/Monads/Syntax.lean
+++ b/Manual/Monads/Syntax.lean
@@ -532,7 +532,7 @@ for $[$[$h :]? $x in $y],* do
 :::
 
 A {keywordOf Lean.Parser.Term.doFor}`for`​`…`​{keywordOf Lean.Parser.Term.doFor}`in` loop requires at least one clause that specifies the iteration to be performed, which consists of an optional membership proof name followed by a colon (`:`), a pattern to bind, the keyword {keywordOf Lean.Parser.Term.doFor}`in`, and a collection term.
-The pattern, which may just be an {tech}[identifier], must match any element of the collection; patterns in this position cannot be used as implicit filters.
+The pattern, which may just be an {tech}[識別子]identifier, must match any element of the collection; patterns in this position cannot be used as implicit filters.
 Further clauses may be provided by separating them with commas.
 Each collection is iterated over at the same time, and iteration stops when any of the collections runs out of elements.
 
diff --git a/Manual/Monads/Zoo.lean b/Manual/Monads/Zoo.lean
index 43c6405..2d635c0 100644
--- a/Manual/Monads/Zoo.lean
+++ b/Manual/Monads/Zoo.lean
@@ -157,8 +157,8 @@ For example, there might be a mutable {lean}`Nat` and a mutable {lean}`String` o
 As long as they have different types, it should be convenient to access both.
 In typical use, some monadic operations that are overloaded in type classes have type information available for {tech key:="synthesis"}[instance synthesis], while others do not.
 For example, the argument passed to {name MonadState.set}`set` determines the type of the state to be used, while {name MonadState.get}`get` takes no such argument.
-The type information present in applications of {name MonadState.set}`set` can be used to pick the correct instance when multiple states are available, which suggests that the type of the mutable state should be an input parameter or {tech}[semi-output parameter] so that it can be used to select instances.
-The lack of type information present in uses of {name MonadState.get}`get`, on the other hand, suggests that the type of the mutable state should be an {tech}[output parameter] in {lean}`MonadState`, so type class synthesis determines the state's type from the monad itself.
+The type information present in applications of {name MonadState.set}`set` can be used to pick the correct instance when multiple states are available, which suggests that the type of the mutable state should be an input parameter or {tech}[半出力パラメータ]semi-output parameter so that it can be used to select instances.
+The lack of type information present in uses of {name MonadState.get}`get`, on the other hand, suggests that the type of the mutable state should be an {tech}[出力パラメータ]output parameter in {lean}`MonadState`, so type class synthesis determines the state's type from the monad itself.
 
 This dichotomy is solved by having two versions of many of the effect type classes.
 The version with a semi-output parameter has the suffix `-Of`, and its operations take types explicitly as needed.
@@ -270,7 +270,7 @@ Providing the state type explicitly using {name}`getThe` from {name}`MonadStateO
 (getThe String, getThe Nat) : M String × M Nat
 ```
 
-Setting a state works for either type, because the state type is a {tech}[semi-output parameter] on {name}`MonadStateOf`.
+Setting a state works for either type, because the state type is a {tech}[半出力パラメータ]semi-output parameter on {name}`MonadStateOf`.
 ```lean (name := setNat)
 #check (set 4 : M Unit)
 ```
diff --git a/Manual/Monads/Zoo/Combined.lean b/Manual/Monads/Zoo/Combined.lean
index bfd9f3b..4640218 100644
--- a/Manual/Monads/Zoo/Combined.lean
+++ b/Manual/Monads/Zoo/Combined.lean
@@ -60,7 +60,7 @@ In one ordering, state changes are rolled back when exceptions are caught; in th
 The latter option matches the semantics of most imperative programming languages, but the former is very useful for search-based problems.
 Often, some but not all state should be rolled back; this can be achieved by “sandwiching” {name}`ExceptT` between two separate uses of {name}`StateT`.
 
-To avoid yet another layer of indirection via the use of {lean}`StateT σ (EStateM ε σ') α`, {name}`EStateM` offers the {name}`EStateM.Backtrackable` {tech}[type class].
+To avoid yet another layer of indirection via the use of {lean}`StateT σ (EStateM ε σ') α`, {name}`EStateM` offers the {name}`EStateM.Backtrackable` {tech}[型クラス]type class.
 This class specifies some part of the state that can be saved and restored.
 {name}`EStateM` then arranges for the saving and restoring to take place around error handling.
 
diff --git a/Manual/Tactics.lean b/Manual/Tactics.lean
index df4b22b..aaa97da 100644
--- a/Manual/Tactics.lean
+++ b/Manual/Tactics.lean
@@ -66,13 +66,13 @@ Each goal in a tactic proof corresponds to an incomplete portion of a proof term
 
 :::comment
 # Running Tactics
-%%%
-tag := "by"
-%%%
 
 :::
 
 # タクティクの実行（Running Tactics）
+%%%
+tag := "by"
+%%%
 
 :::TODO
 The syntax of `by` is showing with commas instead of semicolons below
@@ -567,7 +567,7 @@ Metavariables that result from tactics frequently appear as goals whose {tech}[c
 
 :::
 
-疑問符で始まる項は未知の値に対応する _メタ変数_ （metavariable）です。これらは {tech}[宇宙] レベルか項のいずれかを表すこともあります。メタ変数の中には、Lean のエラボレーションプロセスの一環として、値を決定するのに十分な情報が得られていないときに生じるものがあります。このようなメタ変数の名前の最後には `?m.392` や `?u.498` のように数字が付きます。その他のメタ変数はタクティクや {tech}[named holes] の結果として存在するようになります。これらのメタ変数の名前には数字の要素はありません。タクティクの結果として生じるメタ変数は {tech}[ケースラベル] がメタ変数の名前と一致するゴールとして現れることが多いです。
+疑問符で始まる項は未知の値に対応する _メタ変数_ （metavariable）です。これらは {tech}[宇宙] レベルか項のいずれかを表すこともあります。メタ変数の中には、Lean のエラボレーションプロセスの一環として、値を決定するのに十分な情報が得られていないときに生じるものがあります。このようなメタ変数の名前の最後には `?m.392` や `?u.498` のように数字が付きます。その他のメタ変数はタクティクや {tech}[synthetic holes] の結果として存在するようになります。これらのメタ変数の名前には数字の要素はありません。タクティクの結果として生じるメタ変数は {tech}[ケースラベル] がメタ変数の名前と一致するゴールとして現れることが多いです。
 
 :::comment
 ::example "Universe Level Metavariables"
diff --git a/Manual/Terms.lean b/Manual/Terms.lean
index c8091ba..eb40bdf 100644
--- a/Manual/Terms.lean
+++ b/Manual/Terms.lean
@@ -31,7 +31,7 @@ This chapter will describe Lean's term language, including the following feature
 :::
 
 {deftech}_Terms_ are the principal means of writing mathematics and programs in Lean.
-The {tech}[elaborator] translates them to Lean's minimal core language, which is then checked by the kernel and compiled for execution.
+The {tech}[エラボレータ]elaborator translates them to Lean's minimal core language, which is then checked by the kernel and compiled for execution.
 The syntax of terms is {ref "syntax-ext"}[arbitrarily extensible]; this chapter documents the term syntax that Lean provides out-of-the-box.
 
 # Identifiers
@@ -63,8 +63,8 @@ Resolving an identifier in a way that both creates one of these declarations and
 The rules for resolving and realizing a name are the same, so even though this section refers only to resolving names, it applies to both.
 
 Name resolution is affected by the following:
- * {tech key:="pre-resolved identifier"}[Pre-resolved names] attached to the identifier
- * The {tech}[macro scopes] attached to the identifier
+ * {tech key:="事前解決された識別子"}[Pre-resolved names]pre-resolved identifier attached to the identifier
+ * The {tech}[マクロスコープ]macro scopes attached to the identifier
  * The local bindings in scope, including auxiliary definitions created as part of the elaboration of {keywordOf Lean.Parser.Term.letrec}`let rec`.
  * Aliases created with {keywordOf Lean.Parser.Command.export}`export` in modules transitively imported by the current module
  * The current {tech}[section scope], in particular the current namespace, opened namespaces, and section variables
@@ -270,7 +270,7 @@ def MyList α := List α
 
 Lean's function types describe more than just the function's domain and range.
 They also provide instructions for elaborating application sites by indicating that some parameters are to be discovered automatically via unification or {ref "instance-synth"}[type class synthesis], that others are optional with default values, and that yet others should be synthesized using a custom tactic script.
-Furthermore, their syntax contains support for abbreviating {tech key:="currying"}[curried] functions.
+Furthermore, their syntax contains support for abbreviating {tech key:="カリー化"}[curried]currying functions.
 
 :::syntax term title:="Function types"
 Dependent function types include an explicit name:
@@ -595,7 +595,7 @@ After all arguments have been inserted and there is an ellipsis, then the missin
 If any fresh variables were created for missing explicit positional arguments, the entire application is wrapped in a {keywordOf Lean.Parser.Term.fun}`fun` term that binds them.
 Finally, instance synthesis is invoked and as many metavariables as possible are solved:
  1. A type is inferred for the entire function application. This may cause some metavariables to be solved due to unification that occurs during type inference.
- 2. The instance metavariables are synthesized. {tech}[Default instances] are only used if the inferred type is a metavariable that is the output parameter of one of the instances.
+ 2. The instance metavariables are synthesized. {tech}[デフォルトインスタンス]Default instances are only used if the inferred type is a metavariable that is the output parameter of one of the instances.
  3. If there is an expected type, it is unified with the inferred type; however, errors resulting from this unification are discarded. If the expected and inferred types can be equal, unification can solve leftover implicit argument metavariables. If they can't be equal, an error is not thrown because a surrounding elaborator may be able to insert {tech}[coercions] or {tech key:="lift"}[monad lifts].
 
 
@@ -684,7 +684,7 @@ fun x y => sum3 x y x : Nat → Nat → Nat
 
 
 Optional and automatic parameters are not part of Lean's core type theory.
-They are encoded using the {name}`optParam` and {name}`autoParam` {tech}[gadgets].
+They are encoded using the {name}`optParam` and {name}`autoParam` {tech}[ガジェット]gadgets.
 
 {docstring optParam}
 
@@ -908,7 +908,7 @@ end
 # Literals
 
 There are two kinds of numeric literal: natural number literals and {deftech}[scientific literals].
-Both are overloaded via {tech key:="type class"}[type classes].
+Both are overloaded via {tech key:="型クラス"}[type classes]type class.
 
 ## Natural Numbers
 
@@ -918,7 +918,7 @@ variable {n : Nat}
 ```
 
 When Lean encounters a natural number literal {lean}`n`, it interprets it via the overloaded method {lean}`OfNat.ofNat n`.
-A {tech}[default instance] of {lean}`OfNat Nat n` ensures that the type {lean}`Nat` can be inferred when no other type information is present.
+A {tech}[デフォルトインスタンス]default instance of {lean}`OfNat Nat n` ensures that the type {lean}`Nat` can be inferred when no other type information is present.
 
 {docstring OfNat}
 
@@ -1184,13 +1184,13 @@ They consist of the following:
 
   If an identifier is not bound in the current scope and is not applied to arguments, then it represents a pattern variable.
   {deftech}_Pattern variables_ match any value, and the values thus matched are bound to the pattern variable in the local environment in which the {tech}[right-hand side] is evaluated.
-  If the identifier is bound, it is a pattern if it is bound to the {tech}[constructor] of an {tech}[inductive type] or if its definition has the {attr}`match_pattern` attribute.
+  If the identifier is bound, it is a pattern if it is bound to the {tech}[コンストラクタ]constructor of an {tech}[帰納型]inductive type or if its definition has the {attr}`match_pattern` attribute.
 
 : Applications
 
   Function applications are patterns if the function being applied is an identifier that is bound to a constructor or that has the {attr}`match_pattern` attribute and if all arguments are also patterns.
   If the identifier is a constructor, the pattern matches values built with that constructor if the argument patterns match the constructor's arguments.
-  If it is a function with the {attr}`match_pattern` attribute, then the function application is unfolded and the resulting term's {tech}[normal form] is used as the pattern.
+  If it is a function with the {attr}`match_pattern` attribute, then the function application is unfolded and the resulting term's {tech}[正規形]normal form is used as the pattern.
   Default arguments are inserted as usual, and their normal forms are used as patterns.
   {tech key:="ellipsis"}[Ellipses], however, result in all further arguments being treated as universal patterns, even those with associated default values or tactics.
 
@@ -1198,13 +1198,13 @@ They consist of the following:
 
   {ref "char-syntax"}[Character literals] and {ref "string-syntax"}[string literals] are patterns that match the corresponding character or string.
   {ref "raw-string-literals"}[Raw string literals] are allowed as patterns, but {ref "string-interpolation"}[interpolated strings] are not.
-  {ref "nat-syntax"}[Natural number literals] in patterns are interpreted by synthesizing the corresponding {name}`OfNat` instance and reducing the resulting term to {tech}[normal form], which must be a pattern.
+  {ref "nat-syntax"}[Natural number literals] in patterns are interpreted by synthesizing the corresponding {name}`OfNat` instance and reducing the resulting term to {tech}[正規形]normal form, which must be a pattern.
   Similarly, {tech}[scientific literals] are interpreted via the corresponding {name}`OfScientific` instance.
   While {lean}`Float` has such an instance, {lean}`Float`s cannot be used as patterns because the instance relies on an opaque function that can't be reduced to a valid pattern.
 
 : Structure Instances
 
-  {tech}[Structure instances] may be used as patterns.
+  {tech}[構造体インスタンス]Structure instances may be used as patterns.
   They are interpreted as the corresponding structure constructor.
 
 : Quoted names
@@ -1426,7 +1426,7 @@ variable {α : Type u}
 ```
 
 :::example "Type Refinement"
-This {tech}[indexed family] describes mostly-balanced trees, with the depth encoded in the type.
+This {tech}[添字族]indexed family describes mostly-balanced trees, with the depth encoded in the type.
 ```lean
 inductive BalancedTree (α : Type u) : Nat → Type u where
   | empty : BalancedTree α 0
@@ -1531,8 +1531,8 @@ simp_all made no progress
 ### Explicit Motives
 
 Pattern matching is not a built-in primitive of Lean.
-Instead, it is translated to applications of {tech}[recursors] via {tech}[auxiliary matching functions].
-Both require a {tech}_motive_ that explains the relationship between the discriminant and the resulting type.
+Instead, it is translated to applications of {tech}[再帰子]recursors via {tech}[補助マッチ関数]auxiliary matching functions.
+Both require a {tech}_動機_ motive that explains the relationship between the discriminant and the resulting type.
 Generally, the {keywordOf Lean.Parser.Term.match}`match` elaborator is capable of synthesizing an appropriate motive, and the refinement of types that occurs during pattern matching is a result of the motive that was selected.
 In some specialized circumstances, a different motive may be needed and may be provided explicitly using the `(motive := …)` syntax of {keywordOf Lean.Parser.Term.match}`match`.
 This motive should be a function type that expects at least as many parameters as there are discriminants.
@@ -1653,7 +1653,7 @@ variable {n : Nat}
 In patterns, defined constants with the {attr}`match_pattern` attribute are unfolded and normalized rather than rejected.
 This allows a more convenient syntax to be used for many patterns.
 In the standard library, {name}`Nat.add`, {name}`HAdd.hAdd`, {name}`Add.add`, and {name}`Neg.neg` all have this attribute, which allows patterns like {lean}`n + 1` instead of {lean}`Nat.succ n`.
-Similarly, {name}`Unit` and {name}`Unit.unit` are definitions that set the respective {tech}[universe parameters] of {name}`PUnit` and {name}`PUnit.unit` to 0; the {attr}`match_pattern` attribute on {name}`Unit.unit` allows it to be used in patterns, where it expands to {lean}`PUnit.unit.{0}`.
+Similarly, {name}`Unit` and {name}`Unit.unit` are definitions that set the respective {tech}[宇宙パラメータ]universe parameters of {name}`PUnit` and {name}`PUnit.unit` to 0; the {attr}`match_pattern` attribute on {name}`Unit.unit` allows it to be used in patterns, where it expands to {lean}`PUnit.unit.{0}`.
 
 :::syntax attr (title := "Attribute for Match Patterns")
 The {attr}`match_pattern` attribute indicates that a definition should be unfolded, rather than rejected, in a pattern.
@@ -1688,7 +1688,7 @@ def add : Nat → Nat → Nat
   | a, Nat.succ b => Nat.succ (Nat.add a b)
 ```
 
-No {tech}[ι-reduction] is possible, because the value being matched is a variable, not a constructor.
+No {tech}[ι簡約]ι-reduction is possible, because the value being matched is a variable, not a constructor.
 {lean}`1 + k` gets stuck as {lean}`Nat.add 1 k`, which is not a valid pattern.
 
 In the case of {lean}`k + 1`, that is, {lean}`Nat.add k (.succ .zero)`, the second pattern matches, so it reduces to {lean}`Nat.succ (Nat.add k .zero)`.
@@ -1959,7 +1959,7 @@ typeclass instance problem is stuck, it is often due to metavariables
 ```
 
 A prefix type ascription with {keywordOf Lean.Parser.Term.show}`show`, together with a {tech}[hole], can be used to indicate the monad.
-The {tech key:="default instance"}[default] {lean}`OfNat _ 5` instance provides enough type information to fill the hole with {lean}`Nat`.
+The {tech key:="デフォルトインスタンス"}[default] {lean}`OfNat _ 5` instance provides enough type information to fill the hole with {lean}`Nat`.
 ```lean
 example := show StateM String _ from do
   return 5
diff --git a/Manual/Types.lean b/Manual/Types.lean
index c126ef3..3d53a0b 100644
--- a/Manual/Types.lean
+++ b/Manual/Types.lean
@@ -15,11 +15,15 @@ open Verso.Genre Manual
 
 set_option maxRecDepth 800
 
+/-
 #doc (Manual) "The Type System" =>
+-/
+#doc (Manual) "型システム（The Type System）" =>
 %%%
 tag := "type-system"
 %%%
 
+:::comment
 {deftech}_Terms_, also known as {deftech}_expressions_, are the fundamental units of meaning in Lean's core language.
 They are produced from user-written syntax by the {tech}[elaborator].
 Lean's type system relates terms to their _types_, which are also themselves terms.
@@ -27,37 +31,89 @@ Types can be thought of as denoting sets, while terms denote individual elements
 A term is {deftech}_well-typed_ if it has a type under the rules of Lean's type theory.
 Only well-typed terms have a meaning.
 
+:::
+
+{deftech}_項_ （term）は {deftech}_式_ （expression）としても知られ、Lean のコア言語における意味の基本単位です。これらは {tech}[エラボレータ] によってユーザが書いた構文から生成されます。Lean の型システムは項をその _型_ （type）に関連付けます。型は集合を表し、項は集合の個々の要素を表すと考えることができます。Lean の型理論のルールに従った型を持つ項は {deftech}_well-typed_ と言います。well-typed である項のみが意味を持ちます。
+
+:::comment
 Terms are a dependently typed λ-calculus: they include function abstraction, application, variables, and `let`-bindings.
 In addition to bound variables, variables in the term language may refer to {tech}[constructors], {tech}[type constructors], {tech}[recursors], {deftech}[defined constants], or opaque constants.
 Constructors, type constructors, recursors, and opaque constants are not subject to substitution, while defined constants may be replaced with their definitions.
 
+:::
+
+項は依存型付きラムダ計算です；関数抽象・適用・変数・`let` 束縛を含みます。束縛変数に加えて、項言語の変数は {tech}[コンストラクタ] ・ {tech}[型コンストラクタ] ・ {tech}[再帰子] ・ {deftech}[defined constants] ・不透明な定数を参照することができます。コンストラクタ・型コンストラクタ・再帰子・不透明な定数は置換の対象にはなりませんが、定義された定数はその定義に置き換えることができます。
+
+:::comment
 A {deftech}_derivation_ demonstrates the well-typedness of a term by explicitly indicating the precise inference rules that are used.
 Implicitly, well-typed terms can stand in for the derivations that demonstrate their well-typedness.
 Lean's type theory is explicit enough that derivations can be reconstructed from well-typed terms, which greatly reduces the overhead that would be incurred from storing a complete derivation, while still being expressive enough to represent modern research mathematics.
 This means that proof terms are sufficient evidence of the truth of a theorem and are amenable to independent verification.
 
+:::
+
+{deftech}_導出_ （derivation）は使用される正確な推論規則を明示的に示すことで項の well-typed さを示します。暗黙的に、well-typed な項は、その well-typed であることを示す導出の代わりにすることができます。Lean の型理論は十分に明示的であるため、well-typed な項から導出を再構築することができ、完全な導出を保存することで発生するオーバーヘッドを大幅に削減することができるにもかかわらず、この理論は現代の研究数学を表現するに足る表現力を保ちます。これは、証明項が定理の真理の十分な根拠となり、独立した検証が可能であることを意味します。
+
+:::comment
 In addition to having types, terms are also related by {deftech}_definitional equality_.
 This is the mechanically-checkable relation that equates terms modulo their computational behavior.
 Definitional equality includes the following forms of {deftech}[reduction]:
 
+:::
+
+型を持つことに加えて、項は {deftech}_定義上の等価性_ （definitional equality）によっても関連付けられます。これは機械的にチェック可能な関係であり、計算動作に応じて項を等しくします。定義上の等価性には {deftech}[簡約] （reduction）の以下の形式が含まれます：
+
+:::comment
  : {deftech}[β] (beta)
 
     Applying a function abstraction to an argument by substitution for the bound variable
 
+:::
+
+ : {deftech}[β] (beta)
+
+    束縛された変数への置換によって、引数に関数抽象を適用する
+
+:::comment
  : {deftech}[δ] (delta)
 
     Replacing occurrences of {tech}[defined constants] by the definition's value
 
+:::
+
+ : {deftech}[δ] (delta)
+
+    {tech}[defined constant] の出現箇所を定義の値で置き換える
+
+:::comment
  : {deftech}[ι] (iota)
 
     Reduction of recursors whose targets are constructors (primitive recursion)
 
+:::
+
+ : {deftech}[ι] (iota)
+
+    コンストラクタをターゲットとする再帰子の簡約（原始再帰）
+
+:::comment
  : {deftech}[ζ] (zeta)
 
      Replacement of let-bound variables by their defined values
 
+:::
+
+ : {deftech}[ζ] (zeta)
+
+    let 束縛変数を定義された値に置き換える
+
+:::comment
 Terms in which all possible reductions have been carried out are in {deftech}_normal form_.
 
+:::
+
+すべての可能な簡約が行われた項は {deftech}_正規形_ （normal form）となります。
+
 ::::keepEnv
 ```lean (show := false)
 axiom α : Type
@@ -78,27 +134,50 @@ example : S.mk x.f1 x.f2 = x := by rfl
 export S (f1 f2)
 ```
 
+:::comment
 Definitional equality includes η-equivalence of functions and single-constructor inductive types.
 That is, {lean}`fun x => f x` is definitionally equal to {lean}`f`, and {lean}`S.mk x.f1 x.f2` is definitionally equal to {lean}`x`, if {lean}`S` is a structure with fields {lean}`f1` and {lean}`f2`.
 It also features proof irrelevance, so any two proofs of the same proposition are definitionally equal.
 It is reflexive, symmetric, and a congruence.
+:::
+
+定義上の等価性には関数と単一コンストラクタの帰納型についてのη同値が含まれます。つまり、 {lean}`fun x => f x` は {lean}`f` に定義上等しく、 {lean}`S` がフィールド {lean}`f1` と {lean}`f2` を持つ構造体である時には {lean}`S.mk x.f1 x.f2` は {lean}`x` と定義上等価です。また証明の irrelevance も特徴づけ、同じ命題の2つの証明は定義上等価です。これは反射的・対称的・合同です。
+
 ::::
 
+:::comment
 Definitional equality is used by conversion: if two terms are definitionally equal, and a given term has one of them as its type, then it also has the other as its type.
 Because definitional equality includes reduction, types can result from computations over data.
 
-::::keepEnv
-:::Manual.example "Computing types"
+:::
+
+定義上の等価性は変換にも用いられます：2つの項が定義上等しく、ある項がその一方を型として持つ場合、その項ももう一方を型として持ちます。定義上の等価性は簡約を含むため、データに対する計算から型が生じることがあります。
+
+:::::keepEnv
+:::comment
+::Manual.example "Computing types"
+:::
+::::Manual.example "型の計算"
 
+:::comment
 When passed a natural number, the function {lean}`LengthList` computes a type that corresponds to a list with precisely that many entries in it:
 
+:::
+
+自然数を渡すと、関数 {lean}`LengthList` は正確にその数のエントリを持つリストに対応する型を計算します：
+
 ```lean
 def LengthList (α : Type u) : Nat → Type u
   | 0 => PUnit
   | n + 1 => α × LengthList α n
 ```
 
+:::comment
 Because Lean's tuples nest to the right, multiple nested parentheses are not needed:
+:::
+
+Lean のタプルは右側にネストしているため、複数のネストした括弧は必要ありません：
+
 ````lean
 example : LengthList Int 0 := ()
 
@@ -106,7 +185,12 @@ example : LengthList String 2 :=
   ("Hello", "there", ())
 ````
 
+:::comment
 If the length does not match the number of entries, then the computed type will not match the term:
+:::
+
+長さが項目数と一致しない場合、計算された型はその項と一致しません：
+
 ```lean error:=true name:=wrongNum
 example : LengthList String 5 :=
   ("Wrong", "number", ())
@@ -121,50 +205,109 @@ has type
 but is expected to have type
   LengthList String 3 : Type
 ```
-:::
 ::::
+:::::
 
+:::comment
 The basic types in Lean are {tech}[universes], {tech}[function] types, and {tech}[type constructors] of {tech}[inductive types].
 {tech}[Defined constants], applications of {tech}[recursors], function application, {tech}[axioms] or {tech}[opaque constants] may additionally give types, just as they can give rise to terms in any other type.
 
 
+:::
+
+Lean の基本型は {tech}[宇宙] ・ {tech}[関数] 型・ {tech}[帰納型] の {tech}[型コンストラクタ] です。 {tech}[Defined constants] ・ {tech}[再帰子] の適用・関数適用・ {tech}[axioms] ・ {tech}[不透明な定数] のいずれかは他の型の項を生じさせることができるのと同様に、さらに型を与えることができます。
+
 {include Manual.Language.Functions}
 
-# Propositions
+# 命題（Propositions）
 %%%
 tag := "propositions"
 %%%
 
+:::comment
+-- エラーが出るため章タイトルの上下を入れ替えている
+# Propositions
+:::
+
+:::comment
 {deftech}[Propositions] are meaningful statements that admit proof. {index}[proposition]
 Nonsensical statements are not propositions, but false statements are.
 All propositions are classified by {lean}`Prop`.
 
+:::
+
+{deftech}[命題] （propositioin）は証明を認める意味のある文です。 {index}[proposition] 無意味な文は命題ではありませんが、偽の文は命題です。すべての命題は {lean}`Prop` によって分類されます。
+
+:::comment
 Propositions have the following properties:
 
+:::
+
+命題は以下の性質を持ちます：
+
+:::comment
 : Definitional proof irrelevance
 
   Any two proofs of the same proposition are completely interchangeable.
 
+:::
+
+: 定義上の証明の irrelevance
+
+  同じ命題の2つの証明は完全に交換可能です。
+
+:::comment
 : Run-time irrelevance
 
   Propositions are erased from compiled code.
 
+:::
+
+: ランタイムにおける irrelevance
+
+  命題はコンパイルされたコードからは消去されます。
+
+:::comment
 : Impredicativity
 
   Propositions may quantify over types from any universe whatsoever.
 
+:::
+
+: impredicativity
+
+  命題はあらゆる宇宙からの型に対して量化することができます。
+
+:::comment
 : Restricted Elimination
 
   With the exception of {tech}[subsingletons], propositions cannot be eliminated into non-proposition types.
 
+:::
+
+: 制限された除去
+
+  {tech}[subsingletons] を除いて、命題は非命題型に除去することができません。
+
+:::comment
 : {deftech key:="propositional extensionality"}[Extensionality] {index subterm:="of propositions"}[extensionality]
 
   Any two logically equivalent propositions can be proven to be equal with the {lean}`propext` axiom.
 
+:::
+
+: {deftech key:="propositional extensionality"}[外延性] {index subterm:="of propositions"}[extensionality]
+
+  論理的に同等な2つの命題は、 {lean}`propext` 公理によって等しいことが証明できます。
+
 {docstring propext}
 
+:::comment
 # Universes
 
+:::
+
+:::comment
 Types are classified by {deftech}_universes_. {index}[universe]
 Each universe has a {deftech (key:="universe level")}_level_, {index subterm := "of universe"}[level] which is a natural number.
 The {lean}`Sort` operator constructs a universe from a given level. {index}[`Sort`]
@@ -172,14 +315,28 @@ If the level of a universe is smaller than that of another, the universe itself
 With the exception of propositions (described later in this chapter), types in a given universe may only quantify over types in smaller universes.
 {lean}`Sort 0` is the type of propositions, while each `Sort (u + 1)` is a type that describes data.
 
+:::
+
+型は {deftech}_宇宙_ （universe）によって分類されます。 {index}[universe] 各宇宙には {deftech (key:="universe level")}_レベル_ （level）があり、これは自然数です。 {lean}`Sort` 演算子は与えられたレベルから宇宙を構築します。 {index}[`Sort`] ある宇宙レベルが他の宇宙レベルよりも小さい場合、その宇宙自体も小さいと言います。命題を除いて（この章で後述）、与えられた宇宙内の型はより小さい宇宙内の型に対してのみ量化することができます。 {lean}`Sort 0` は命題の型であり、各 `Sort (u + 1)` はデータを記述する型です。
+
+:::comment
 Every universe is an element of every strictly larger universe, so {lean}`Sort 5` includes {lean}`Sort 4`.
 This means that the following examples are accepted:
+:::
+
+すべての宇宙はすべての狭義に大きな宇宙の要素なので、 {lean}`Sort 5` は {lean}`Sort 4` を含みます。つまり、以下の例が認められます：
+
 ```lean
 example : Sort 5 := Sort 4
 example : Sort 2 := Sort 1
 ```
 
+:::comment
 On the other hand, {lean}`Sort 3` is not an element of {lean}`Sort 5`:
+:::
+
+一方で、 {lean}`Sort 3` は {lean}`Sort 5` の要素ではありません：
+
 ```lean (error := true) (name := sort3)
 example : Sort 5 := Sort 3
 ```
@@ -193,7 +350,12 @@ but is expected to have type
   Type 4 : Type 5
 ```
 
+:::comment
 Similarly, because {lean}`Unit` is in {lean}`Sort 1`, it is not in {lean}`Sort 2`:
+:::
+
+同様に、 {lean}`Unit` は {lean}`Sort 1` に存在するため、 {lean}`Sort 2` には存在しません：
+
 ```lean
 example : Sort 1 := Unit
 ```
@@ -210,46 +372,92 @@ but is expected to have type
   Type 1 : Type 2
 ```
 
+:::comment
 Because propositions and data are used differently and are governed by different rules, the abbreviations {lean}`Type` and {lean}`Prop` are provided to make the distinction more convenient.  {index}[`Type`] {index}[`Prop`]
 `Type u` is an abbreviation for `Sort (u + 1)`, so {lean}`Type 0` is {lean}`Sort 1` and {lean}`Type 3` is {lean}`Sort 4`.
 {lean}`Type 0` can also be abbreviated {lean}`Type`, so `Unit : Type` and `Type : Type 1`.
 {lean}`Prop` is an abbreviation for {lean}`Sort 0`.
 
+:::
+
+命題とデータは異なる使われ方をし、異なる規則に支配されるため、より便利に区別するために {lean}`Type` と {lean}`Prop` という省略形が用意されています。 {index}[`Type`] {index}[`Prop`] `Type u` は `Sort (u + 1)` の省略形であるため、 {lean}`Type 0` は {lean}`Sort 1` で {lean}`Type 3` は {lean}`Sort 4` です。 {lean}`Type 0` は {lean}`Type` と省略することもできるため、 `Unit : Type` および `Type : Type 1` です。 {lean}`Prop` は {lean}`Sort 0` の省略形です。
+
 ## Predicativity
 
+:::comment
 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.
 
+:::
+
+各宇宙は依存関数型を含んでおり、それはさらに全称量化子と含意を表します。関数型の宇宙は、引数の型と戻り値の型の宇宙によって決定されます。具体的な規則は、関数の戻り値が命題かどうかに依存します。
+
+:::comment
 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 {deftech}[_impredicative_] {index}[impredicative]{index subterm := "impredicative"}[quantification] quantification, because propositions can themselves be statements about all propositions (and all other types).
 
-:::Manual.example "Impredicativity"
+:::
+
+命題を返す関数である述語（つまり、関数の結果が `Prop` にある型である場合）は引数の型がどのような宇宙に会っても構いませんが、関数の型自体は `Prop` に留まります。言い換えると、命題は {deftech}[_impredicative_] {index}[impredicative]{index subterm := "impredicative"}[quantification] な量化子を特徴づけます。というのも、命題はそれ自体、すべての命題（および他のすべての命題）についての文になりうるからです。
+
+::::Manual.example "Impredicativity"
+:::comment
 Proof irrelevance can be written as a proposition that quantifies over all propositions:
+:::
+
+証明の irrelevance はすべての命題を量化する命題として書くことができます：
+
 ```lean
 example : Prop := ∀ (P : Prop) (p1 p2 : P), p1 = p2
 ```
 
+:::comment
 A proposition may also quantify over all types, at any given level:
+:::
+
+命題はまた任意のレベルにおいてすべての型を量化することもできます：
+
 ```lean
 example : Prop := ∀ (α : Type), ∀ (x : α), x = x
 example : Prop := ∀ (α : Type 5), ∀ (x : α), x = x
 ```
-:::
+::::
 
+:::comment
 For universes at {tech key:="universe level"}[level] `1` and higher (that is, the `Type u` hierarchy), quantification is {deftech}[_predicative_]. {index}[predicative]{index subterm := "predicative"}[quantification]
 For these universes, the universe of a function type is the least upper bound of the argument and return types' universes.
 
-:::Manual.example "Universe levels of function types"
+:::
+
+{tech key:="universe level"}[レベル] `1` 以上の宇宙（つまり、`Type u` の階層）では、量化子は {deftech}[_predicative_] です。 {index}[predicative]{index subterm := "predicative"}[quantification] これらの宇宙では、関数型の宇宙は引数の型と戻り値の型の宇宙の最小上界となります。
+
+:::comment
+::Manual.example "Universe levels of function types"
+:::
+::::Manual.example "関数型の宇宙レベル"
+:::comment
 Both of these types are in {lean}`Type 2`:
+:::
+
+これらの型はどちらも {lean}`Type 2` に存在します：
+
 ```lean
 example (α : Type 1) (β : Type 2) : Type 2 := α → β
 example (α : Type 2) (β : Type 1) : Type 2 := α → β
 ```
-:::
+::::
 
-:::Manual.example "Predicativity of {lean}`Type`"
+:::comment
+::Manual.example "Predicativity of {lean}`Type`"
+:::
+::::Manual.example "{lean}`Type` の Predicativity"
+:::comment
 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:
+:::
+
+`α` のレベルは `1` より大きいため、この例は許可されません。言い換えると、注釈された宇宙は実際の関数型の宇宙よりも小さいです：
+
 ```lean error := true name:=toosmall
 example (α : Type 2) (β : Type 1) : Type 1 := α → β
 ```
@@ -261,13 +469,26 @@ has type
 but is expected to have type
   Type 1 : Type 2
 ```
-:::
+::::
 
+:::comment
 Lean's universes are not {deftech}[cumulative];{index}[cumulativity] a type in `Type u` is not automatically also in `Type (u + 1)`.
 Each type inhabits precisely one universe.
 
-:::Manual.example "No cumulativity"
+:::
+
+Lean の宇宙は {deftech}[cumulative] ではありません； {index}[cumulativity] これは `Type u` の型が自動的に `Type (u + 1)` にも存在するようにならないことを意味します。
+
+:::comment
+::Manual.example "No cumulativity"
+:::
+::::Manual.example "cumulativity ではない"
+:::comment
 This example is not accepted because the annotated universe is larger than the function type's universe:
+:::
+
+この例は注釈された宇宙が関数型の宇宙よりも大きいため、許可されません：
+
 ```lean error := true name:=toobig
 example (α : Type 2) (β : Type 1) : Type 3 := α → β
 ```
@@ -279,28 +500,60 @@ has type
 but is expected to have type
   Type 3 : Type 4
 ```
-:::
+::::
+
+:::comment
 
 ## Polymorphism
 
+:::
+
+## 多相性（Polymorphism）
+
+:::comment
 Lean supports {deftech}_universe polymorphism_, {index subterm:="universe"}[polymorphism] {index}[universe polymorphism] which means that constants defined in the Lean environment can take {deftech}[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.
 
-:::Manual.example "Universe-polymorphic identity function"
+:::
+
+Lean は {deftech}_宇宙多相_ {index subterm:="universe"}[polymorphism] {index}[universe polymorphism] （universe polymorphism）をサポートしており、Lean 環境で定義された定数は {deftech}[宇宙パラメータ] を取ることができます。これらのパラメータは定数が使用されるときに宇宙レベルでインスタンス化されます。宇宙パラメータは定数名の後のドットに続く波括弧で記述します。
+
+:::comment
+::Manual.example "Universe-polymorphic identity function"
+:::
+::::Manual.example "宇宙多相恒等関数"
+:::comment
 When fully explicit, the identity function takes a universe parameter `u`. Its signature is:
+:::
+
+完全に明示的な場合、恒等関数は宇宙パラメータ `u` を取ります。このシグネチャは以下になります：
+
 ```signature
 id.{u} {α : Sort u} (x : α) : α
 ```
-:::
+::::
 
+:::comment
 Universe variables may additionally occur in {ref "level-expressions"}[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.
 
-::::keepEnv
-:::Manual.example "Universe level expressions"
+:::
+
+宇宙変数はさらに、定義の中で特定の宇宙レベルを提供する {ref "level-expressions"}[宇宙レベル式] の中で現れるかもしれません。多相定義が具体的なレベルでインスタンス化されるとき、これらの宇宙レベル式も具体的なレベルをもたらすために評価されます。
+
+:::::keepEnv
+:::comment
+::Manual.example "Universe level expressions"
+:::
+::::Manual.example "宇宙レベル式"
 
+:::comment
 In this example, {lean}`Codec` is in a universe that is one greater than the universe of the type it contains:
+:::
+
+この例では、 {lean}`Codec` はそれが含む型の宇宙より1つ大きい宇宙に存在します：
+
 ```lean
 structure Codec.{u} : Type (u + 1) where
   type : Type u
@@ -308,8 +561,13 @@ structure Codec.{u} : Type (u + 1) where
   decode : Array UInt32 → Nat → Option (type × Nat)
 ```
 
+:::comment
 Lean automatically infers most level parameters.
 In the following example, it is not necessary to annotate the type as {lean}`Codec.{0}`, because {lean}`Char`'s type is {lean}`Type 0`, so `u` must be `0`:
+:::
+
+Lean はほとんどのレベルパラメータを自動的に推論します。以下の例では、 {lean}`Char` の型は {lean}`Type 0` であるため、`u` は `0` でなければならないことから、 {lean}`Codec.{0}` と注釈する必要はありません。
+
 ```lean (keep := true)
 def Codec.char : Codec where
   type := Char
@@ -322,17 +580,30 @@ def Codec.char : Codec where
     else
       failure
 ```
-:::
 ::::
+:::::
 
+:::comment
 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.
 
-::::keepEnv
-:::Manual.example "Universe polymorphism and definitional equality"
+:::
+
+宇宙多相な定義は、実際には様々なレベルでインスタンス可能な _スキーマ的定義_ （schematic definition）を作り出し、宇宙レベルの異なるインスタンス化は互換性のない値を作ります。
+
+:::comment
+::Manual.example "Universe polymorphism and definitional equality"
+:::
+:::::keepEnv
+::::Manual.example "宇宙多相と定義上の等価性"
 
+:::comment
 This can be seen in the following example, in which {lean}`T` is a gratuitously-universe-polymorphic function that always returns {lean}`true`.
 Because it is marked {keywordOf Lean.Parser.Command.declaration}`opaque`, Lean can't check equality by unfolding the definitions.
 Both instantiations of {lean}`T` have the parameters and the same type, but their differing universe instantiations make them incompatible.
+:::
+
+これは次の例で見ることができます。 {lean}`T` は不要な宇宙多相定義で、常に {lean}`true` を返します。 {keywordOf Lean.Parser.Command.declaration}`opaque` とマークされているため、Lean は {lean}`T` の定義を展開して等価性をチェックすることができません。 {lean}`T` のインスタンスはどれもパラメータと同じ型を持ちますが、宇宙のインスタンス化が異なるため互換性がありません：
+
 ```lean (error := true) (name := uniIncomp)
 opaque T.{u} (_ : Nat) : Bool := (fun (α : Sort u) => true) PUnit.{u}
 
@@ -348,21 +619,39 @@ has type
 but is expected to have type
   Eq.{1} (T.{u} 0) (T.{v} 0) : Prop
 ```
-:::
 ::::
+:::::
 
+:::comment
 Auto-bound implicit arguments are as universe-polymorphic as possible.
 Defining the identity function as follows:
+:::
+
+自動的に束縛される暗黙の引数は可能な限り宇宙多相となります。恒等関数を次のように定義します：
+
 ```lean
 def id' (x : α) := x
 ```
+:::comment
 results in the signature:
+:::
+
+これは以下のシグネチャになります：
+
 ```signature
 id'.{u} {α : Sort u} (x : α) : α
 ```
 
-:::Manual.example "Universe monomorphism in auto-bound implicit parameters"
+:::comment
+::Manual.example "Universe monomorphism in auto-bound implicit parameters"
+:::
+::::Manual.example "自動的に束縛された暗黙のパラメータを持つ宇宙のモノ射"
+:::comment
 On the other hand, because {name}`Nat` is in universe {lean}`Type 0`, this function automatically ends up with a concrete universe level for `α`, because `m` is applied to both {name}`Nat` and `α`, so both must have the same type and thus be in the same universe:
+:::
+
+一方、 {name}`Nat` は {lean}`Type 0` に存在するため、この関数は自動的に `α` の具体的な宇宙レベルを求めます。`m` は {name}`Nat` と `α` の両方に適用されるため、どちらも同じ型を持たなければならず、結果として同じ宇宙となります：
+
 ```lean
 partial def count [Monad m] (p : α → Bool) (act : m α) : m Nat := do
   if p (← act) then
@@ -382,16 +671,25 @@ info: count.{u_1} {m : Type → Type u_1} {α : Type} [Monad m] (p : α → Bool
 #guard_msgs in
 #check count
 ```
-:::
+::::
 
+:::comment
 ### Level Expressions
+:::
+### レベル式（Level Expressions）
 %%%
 tag := "level-expressions"
 %%%
 
+:::comment
 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.
 
+:::
+
+定義に現れるレベルは変数と定数の和だけに限定されません。より複雑な宇宙間の関係もレベルの表現を使って定義できます。
+
+:::comment
 ````
 Level ::= 0 | 1 | 2 | ...  -- Concrete levels
         | u, v             -- Variables
@@ -399,26 +697,62 @@ Level ::= 0 | 1 | 2 | ...  -- Concrete levels
         | max Level Level  -- Least upper bound
         | imax Level Level -- Impredicative LUB
 ````
+:::
+````
+Level ::= 0 | 1 | 2 | ...  -- 具体的なレベル
+        | u, v             -- 変数
+        | Level + n        -- 定数の和
+        | max Level Level  -- 最小上界
+        | imax Level Level -- Impredicative な最小上界
+````
 
+:::comment
 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:
 
+:::
+
+レベル変数が具体的な数値に割り当てられている場合、これらの式の評価は通常の算術の規則に従います。`imax` 演算は以下のように定義されます：
+
 $$``\mathtt{imax}\ u\ v = \begin{cases}0 & \mathrm{when\ }v = 0\\\mathtt{max}\ u\ v&\mathrm{otherwise}\end{cases}``
 
+:::comment
 `imax` is used to implement {tech}[impredicative] quantification for {lean}`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 {lean}`Prop`; otherwise, the function type's level is the maximum of `u` and `v`.
 
+:::
+
+`imax` は {lean}`Prop` の {tech}[impredicative] な量化子を実装するために使用されます。特に、`A : Sort u` かつ `B : Sort v` である場合、`(x : A) → B : Sort (imax u v)` となります。もし `B : Prop` ならば、その関数型は {lean}`Prop` であり、それ以外ではその関数型のレベルは `u` と `v` の最大値になります。
+
+:::comment
 ### Universe Variable Bindings
 
+:::
+
+### 宇宙変数の束縛（Universe Variable Bindings）
+
+:::comment
 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.
 
-::::keepEnv
-:::Manual.example "Universe-polymorphic `map`"
+:::
+
+宇宙多相定義は宇宙変数を束縛します。これらの束縛は明示的・暗黙的のどちらも可能です。明示的な宇宙変数の束縛とインスタンス化は定義の名前の接尾辞として行われます。宇宙パラメータは定数名にピリオド（`.`）を接尾辞として付け、その後に波括弧の間にカンマで区切られた一連の宇宙変数を付けることで定義・提供されます。
+
+:::::keepEnv
+:::comment
+::Manual.example "Universe-polymorphic `map`"
+:::
+::::Manual.example "宇宙多相な `map`"
+:::comment
 The following declaration of {lean}`map` declares two universe parameters (`u` and `v`) and instantiates the polymorphic {name}`List` with each in turn:
+:::
+
+以下{lean}`map` の宣言では、2つの宇宙パラメータ（`u` と `v`）を宣言し、多相型の {name}`List` を順番にインスタンス化しています：
+
 ```lean
 def map.{u, v} {α : Type u} {β : Type v}
     (f : α → β) :
@@ -426,15 +760,28 @@ def map.{u, v} {α : Type u} {β : Type v}
   | [] => []
   | x :: xs => f x :: map f xs
 ```
-:::
 ::::
+:::::
 
+:::comment
 Just as Lean automatically instantiates implicit parameters, it also automatically instantiates universe parameters.
 When the {TODO}[describe this option and add xref] `autoImplicit` option is set to {lean}`true` (the default), it is not necessary to explicitly bind universe variables.
 When it is set to {lean}`false`, then they must be added explicitly or declared using the `universe` command. {TODO}[xref]
 
-:::Manual.example "Auto-implicits and universe polymorphism"
+:::
+
+Lean が暗黙のパラメータを自動的にインスタンス化するように、宇宙パラメータも自動的にインスタンス化されます。`autoImplicit` オプションが {lean}`true` に設定されている場合（これがデフォルトです）、宇宙変数を明示的に束縛する必要はありません。 {lean}`false` に設定すると、明示的に追加するか `universe` コマンドを使って宣言する必要があります。
+
+:::comment
+::Manual.example "Auto-implicits and universe polymorphism"
+:::
+::::Manual.example "自動的な暗黙さと宇宙多相"
+:::comment
 When `autoImplicit` is {lean}`true` (which is the default setting), this definition is accepted even though it does not bind its universe parameters:
+:::
+
+`autoImplicit` が {lean}`true` （デフォルト値）の場合、この定義は宇宙パラメータを束縛していなくても許可されます：
+
 ```lean (keep := false)
 set_option autoImplicit true
 def map {α : Type u} {β : Type v} (f : α → β) : List α → List β
@@ -442,7 +789,12 @@ def map {α : Type u} {β : Type v} (f : α → β) : List α → List β
   | x :: xs => f x :: map f xs
 ```
 
+:::comment
 When `autoImplicit` is {lean}`false`, the definition is rejected because `u` and `v` are not in scope:
+:::
+
+`autoImplicit` が {lean}`false` の場合、`u` と `v` がスコープにないためこの定義は却下されます：
+
 ```lean (error := true) (name := uv)
 set_option autoImplicit false
 def map {α : Type u} {β : Type v} (f : α → β) : List α → List β
@@ -455,21 +807,39 @@ unknown universe level 'u'
 ```leanOutput uv
 unknown universe level 'v'
 ```
-:::
+::::
 
+:::comment
 In addition to using `autoImplicit`, particular identifiers can be declared as universe variables in a particular {tech}[section scope] using the `universe` command.
 
-:::syntax Lean.Parser.Command.universe
+:::
+
+`autoImplicit` を使うことに加えて、`universe` コマンドを使って特定の識別子を特定の {tech}[section scope] 内の宇宙変数として宣言することができます。
+
+::::syntax Lean.Parser.Command.universe
 ```grammar
 universe $x:ident $xs:ident*
 ```
 
+:::comment
 Declares one or more universe variables for the extent of the current scope.
 
+:::
+
+現在のスコープの範囲において1つ以上の宇宙変数を宣言します。
+
+:::comment
 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 {lean}`false`.
 :::
 
-:::Manual.example "The `universe` command when `autoImplicit` is `false`"
+`variable` コマンドが特定の識別子を特定の型のパラメータとして扱うように、`universe` コマンドは `autoImplicit` オプションが {lean}`false` であっても、それに続く識別子を宇宙パラメータとして暗黙的に量化します。
+
+::::
+
+:::comment
+::Manual.example "The `universe` command when `autoImplicit` is `false`"
+:::
+:::Manual.example "`autoImplicit` が `false` の際の `universe` コマンド"
 ```lean (keep := false)
 set_option autoImplicit false
 universe u
@@ -477,15 +847,33 @@ def id₃ (α : Type u) (a : α) := a
 ```
 :::
 
+:::comment
 Because the automatic implicit parameter feature only insert parameters that are used in the declaration's {tech}[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`.
 
-:::Manual.example "Automatic universe parameters and the `universe` command"
+:::
+
+自動的な暗黙のパラメータ機能は宣言の {tech}[ヘッダ] で使用されるパラメータのみを挿入するため、定義の右側にのみ現れる宇宙変数は `autoImplicit` が `true` の場合でも `universe` で宣言されていない限り引数として挿入されません。
+
+:::comment
+::Manual.example "Automatic universe parameters and the `universe` command"
+:::
+::::Manual.example "自動的な宇宙パラメータと `universe` コマンド"
 
+:::comment
 This definition with an explicit universe parameter is accepted:
+:::
+
+明示的な宇宙パラメータを伴ったこの定義は許可されます：
+
 ```lean (keep := false)
 def L.{u} := List (Type u)
 ```
+:::comment
 Even with automatic implicit parameters, this definition is rejected, because `u` is not mentioned in the header, which precedes the `:=`:
+:::
+
+`u` が `:=` の前にあるヘッダで言及されていないため、自動的な暗黙のパラメータでもこの定義は却下されます：
+
 ```lean (error := true) (name := unknownUni) (keep := false)
 set_option autoImplicit true
 def L := List (Type u)
@@ -493,20 +881,35 @@ def L := List (Type u)
 ```leanOutput unknownUni
 unknown universe level 'u'
 ```
+:::comment
 With a universe declaration, `u` is accepted as a parameter even on the right-hand side:
+:::
+
+宇宙宣言では、`u` は右辺でもパラメータとして許可されます：
+
 ```lean (keep := false)
 universe u
 def L := List (Type u)
 ```
+:::comment
 The resulting definition of `L` is universe-polymorphic, with `u` inserted as a universe parameter.
 
+:::
+
+その結果、`L` の定義は宇宙パラメータとして `u` が挿入された宇宙多相となります。
+
+:::comment
 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` コマンドのスコープにある宣言は、その中に宇宙変数が無い場合、または自動的に挿入される他の引数の中に宇宙変数が無い場合、多相にはなりません。
+
 ```lean
 universe u
 def L := List (Type 0)
 #check L
 ```
-:::
+::::
 
 ### Universe Unification