diff --git a/GLOSSARY.md b/GLOSSARY.md
index 607433e..ed288bb 100644
--- a/GLOSSARY.md
+++ b/GLOSSARY.md
@@ -4,19 +4,25 @@
 | --- | --- | --- |
 | abbreviation | 省略形 | |
 | abstraction | 抽象 | |
+| angle bracket | 角括弧 | square bracketと同じ訳語にしているが、直後にコード例がある場合も多いため文脈で見分けられる想定 |
 | annotation | 注釈 | |
+| anonymous constructor | 匿名コンストラクタ | |
 | associativity | 結合性 | |
 | assumption | 仮定 | |
 | attribute | 属性 | |
 | backtrack | バックトラック | 後戻りと書かれる場合あり |
 | binder | 束縛子 | |
+| boolean | 真偽値 | |
 | bound variable | 束縛変数 | |
+| box | ボックス化 | |
 | canonical | 標準 | |
 | carriage return | CR | |
 | case distinction | 場合分け | |
 | chapter | 章 | |
+| clause | 節 | |
 | closed term | 閉項 | |
 | combinator | コンビネータ | |
+| comma | カンマ | |
 | command | コマンド | |
 | command elaboration | コマンドエラボレーション | |
 | compilation | コンパイル | |
@@ -40,6 +46,7 @@
 | dependent | 依存的 | 後ろに何も続かない場合 |
 | dependent function | 依存関数 | |
 | dependent type theory | 依存型理論 | |
+| deriving | 導出 | |
 | desugar | 脱糖 | |
 | domain | 定義域 | |
 | double-struck | 重ね打ち体 | |
@@ -47,15 +54,21 @@
 | elaborate | エラボレート | |
 | elaboration | エラボレーション | |
 | elaborator | エラボレータ | |
+| elimination rule | 除去則 | |
 | encoding | エンコード | |
 | English letter | 英語アルファベット | |
+| enum inductive | 列挙的帰納 | |
 | environment | 環境 | |
 | environment extensions | 環境拡張 | |
 | equational lemma | 等式の補題 | |
+| equivalent | 同値 | |
 | evaluate | 評価 | |
+| evidence | 根拠 | |
+| exception | 例外 | |
 | exclamation mark | 感嘆符 | |
 | executable | 実行ファイル | |
 | expression | 式 | |
+| fixed-width integer | 固定幅整数 | |
 | formalization | 形式化 | |
 | form feed | 改ページ | |
 | functional programming language | 関数型プログラミング言語 | |
@@ -67,10 +80,12 @@
 | hierarchical identifier | 階層的識別子 | |
 | hierarchy | 階層 | |
 | higher-order function | 高階関数 | |
+| identically | 同一 | |
 | identifier | 識別子 | |
 | identifier component | 識別子要素 | |
 | identifier continuation character | 識別子継続文字 | |
 | implicit parameter | 暗黙のパラメータ | |
+| index, indices | 添字 | |
 | inductively-defined | 帰納的に定義された | |
 | inductive predicate | 帰納的述語 | |
 | inductive type | 帰納型 | |
@@ -95,11 +110,13 @@
 | letterlike | 文字様 | |
 | longest match | 最長一致 | |
 | macro | マクロ | |
+| machine integer | 機械整数 | |
 | machinery | 機構 | |
 | macro Expansion | マクロ展開 | |
 | mapping | マッピング | |
 | memoization | メモ化 | |
 | monad | モナド | |
+| motive | 動機 | |
 | multi-threading | マルチスレッド | |
 | mutually inductive | 相互帰納 | |
 | namespace | 名前空間 | |
@@ -116,6 +133,7 @@
 | parse | パース | |
 | parser | パーサ | |
 | pattern matching | パターンマッチ | |
+| polymorphic | 多相 | |
 | precedence | 優先順位 | 構文解析・演算子等の優先具合を指す |
 | pretty printer | プリティプリンタ | |
 | primitive | プリミティブ | |
@@ -136,8 +154,10 @@
 | representation | 表現 | |
 | reserved keyword | 予約キーワード | 下のreserved wordの表記ゆれかもしれないがいったん別の訳語を割り当てる |
 | reserved word | 予約語 | |
+| run-length encoding | 連長圧縮 | |
 | run-time | ランタイム | |
 | rule | ランタイム | |
+| saturated application | 完全な適用 | 固定訳は無いように思われ、飽和では意味が分かりづらいため |
 | scope | スコープ | |
 | separator | 区切り文字 | |
 | set | （数学的な集合を意味しない場合）あつまり、（数学的な集合の場合）集合 | |
@@ -154,6 +174,7 @@
 | strictness | 正格 | |
 | structure | 構造体 | |
 | subterm | 部分項 | |
+| subtype | 部分型 | |
 | subscript | 下付き文字 | |
 | syntactically | 構文上 | |
 | syntactic sugar | 構文糖衣 | |
@@ -174,14 +195,22 @@
 | transitive | 推移的 | |
 | transitivity | 推移性 | |
 | tree | 木 | |
+| trivial | 自明な | |
 | trust | 信頼 | |
 | type class | 型クラス | |
 | type class instance synthesis | 型クラスインスタンス合成 | |
+| type signature | 型シグネチャ | |
+| unbox | ボックス化解除 | C#の用語を流用 |
 | underscore | アンダースコア | |
 | unification | 単一化 | |
 | union | 合併 | |
+| unit type | ユニット型 | |
+| universe | 宇宙 | |
+| universe level | 宇宙レベル | |
+| well-formed | 適格 | |
 | well-founded | 整礎 | |
 | whitespace | 空白 | |
+| wrapper | ラッパ | |
 
 
 # 英語表現をそのまま用いている単語
@@ -190,6 +219,8 @@
 | --- | --- |
 | choice node | |
 | packed array | System Verilogという言語にこの名前の文法要素がある？ |
+| strict positively, negatively | 自己言及される定義の分類、定訳は無い模様 |
 | prelude | |
+| relevant, irrelevant | 直訳して「関係・無関係」はわかりづらいと判断 |
 | subject reduction | TAPLに出てくる模様 |
 | type ascription | Scala、Rustに同じ用語あり |
\ No newline at end of file
diff --git a/Manual/Elaboration.lean b/Manual/Elaboration.lean
index 67df3b4..eaa22ac 100644
--- a/Manual/Elaboration.lean
+++ b/Manual/Elaboration.lean
@@ -286,7 +286,7 @@ It does not include a syntactic termination checker, nor does it perform unifica
 Before new inductive types or definitions are added to the environment by the command or term elaborators, they must be checked by the kernel to guard against potential bugs in elaboration.
 :::
 
-Lean が信頼する {deftech}_カーネル_ （kernel）はコア型理論のための型チェッカの小さく堅牢な実装です。カーネルには構文的停止チェッカは含まれず、単一化も行いません；停止性はすべての再帰関数をプリミティブ {tech}[recursors] の使用にエラボレートすることで保証され、単一化はエラボレータによってすでに実行されていることが期待されます。コマンドと項エラボレータによって新しい帰納型や定義が環境に追加される前に、エラボレータによって潜在的なバグを防ぐために、それらはカーネルによってチェックされなければなりません。
+Lean が信頼する {deftech}_カーネル_ （kernel）はコア型理論のための型チェッカの小さく堅牢な実装です。カーネルには構文的停止チェッカは含まれず、単一化も行いません；停止性はすべての再帰関数をプリミティブ {tech}[再帰子] の使用にエラボレートすることで保証され、単一化はエラボレータによってすでに実行されていることが期待されます。コマンドと項エラボレータによって新しい帰納型や定義が環境に追加される前に、エラボレータによって潜在的なバグを防ぐために、それらはカーネルによってチェックされなければなりません。
 
 :::comment
 Lean's kernel is written in C++.
@@ -311,7 +311,7 @@ The language implemented by the kernel is a version of the Calculus of Construct
 カーネルが実装する言語は Calculus of Constructions の一種で、以下の特徴を持つ依存型理論です：
 + 完全な依存型
 + 相互に帰納的であったり、他の帰納的データ型の下で入れ子になった再帰を含んだりする帰納的に定義されたデータ型
-+ {tech}[impredicative] ・定義上証明とは無関係な {tech}[propositions] の拡張的 {tech}[universe]
++ {tech}[impredicative] ・定義上証明と irrelevant な {tech}[propositions] の拡張的 {tech}[universe]
 + {tech}[predicative] なデータの宇宙の非蓄積な階層
 * 定義上の計算規則を伴った {ref "quotients"}[商型] （Quotient type）
 + 命題上の関数外延性 {margin}[関数外延性は商型を使って証明できる定理ですが、重要な帰結であるため別で挙げておきます。]
@@ -356,7 +356,7 @@ In practice, apparent nontermination is indistinguishable from sufficiently slow
 These metatheoretic properties are a result of having impredicativity, quotient types that compute, definitional proof irrelevance, and propositional extensionality; these features are immensely valuable both to support ordinary mathematical practice and to enable automation.
 :::
 
-Lean の型理論には subject reduction の機能はなく、定義上の等価性は必ずしも推移的ではなく、型チェッカが停止しないようにすることも可能です。これらのメタ理論的な特性はいずれも実際には問題になりません。推移性が失敗するのは非常にまれであり、知る限りではそれを行使するために特別にコードを作成した場合を除き非停止は発生していません。最も重要なことは、論理的健全性に影響がないことです。実際には、見かけ上の非停止は十分に遅いプログラムと区別がつきません。これらのメタ理論的特性は、impredicativity・計算する商型・定義上の証明の無関係性・命題上の外延性からの帰結です；これらの機能は、通常の数学的実践をサポートする上でも、自動化を可能にするうえでも非常に価値があります。
+Lean の型理論には subject reduction の機能はなく、定義上の等価性は必ずしも推移的ではなく、型チェッカが停止しないようにすることも可能です。これらのメタ理論的な特性はいずれも実際には問題になりません。推移性が失敗するのは非常にまれであり、知る限りではそれを行使するために特別にコードを作成した場合を除き非停止は発生していません。最も重要なことは、論理的健全性に影響がないことです。実際には、見かけ上の非停止は十分に遅いプログラムと区別がつきません。これらのメタ理論的特性は、impredicativity・計算する商型・定義上の証明との irrelevance・命題上の外延性からの帰結です；これらの機能は、通常の数学的実践をサポートする上でも、自動化を可能にするうえでも非常に価値があります。
 
 :::comment
 # Elaboration Results
@@ -371,7 +371,7 @@ Thus, the elaborator must translate definitions that use pattern matching and re
 This translation is additionally a proof that the function terminates for all potential arguments, because all functions that can be translated to recursors also terminate.
 :::
 
-Lean のコア型理論には、パターンマッチや再帰定義は含まれていません。その代わりに、場合分けとプリミティブな再帰の両方を実装するために使用できる低レベルの {tech}[recursors] を提供します。したがって、エラボレータはパターンマッチと再帰を使用する定義から再帰子を使用する定義に変換する必要があります。この変換はさらに、関数がすべての潜在的な引数に対して停止することの証明でもあります。なぜなら再帰子へ翻訳されるすべての関数は停止するからです。
+Lean のコア型理論には、パターンマッチや再帰定義は含まれていません。その代わりに、場合分けとプリミティブな再帰の両方を実装するために使用できる低レベルの {tech}[再帰子] を提供します。したがって、エラボレータはパターンマッチと再帰を使用する定義から再帰子を使用する定義に変換する必要があります。この変換はさらに、関数がすべての潜在的な引数に対して停止することの証明でもあります。なぜなら再帰子へ翻訳されるすべての関数は停止するからです。
 
 :::comment
 The translation to recursors happens in two phases: during term elaboration, uses of pattern matching are replaced by appeals to auxiliary functions that implement the particular case distinction that occurs in the code.
diff --git a/Manual/Language.lean b/Manual/Language.lean
index 29102eb..beb68e7 100644
--- a/Manual/Language.lean
+++ b/Manual/Language.lean
@@ -36,7 +36,7 @@ A term is {deftech}_well-typed_ if it has a type under the rules of Lean's type
 Only well-typed terms have a meaning.
 
 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.
+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.
 
 A {deftech}_derivation_ demonstrates the well-typedness of a term by explicitly indicating the precise inference rules that are used.
@@ -130,8 +130,8 @@ but is expected to have type
 :::
 ::::
 
-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.
+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.
 
 
 {include Manual.Language.Functions}
diff --git a/Manual/Language/Functions.lean b/Manual/Language/Functions.lean
index a6caa5c..9df9504 100644
--- a/Manual/Language/Functions.lean
+++ b/Manual/Language/Functions.lean
@@ -231,7 +231,7 @@ However, not all functions originate from abstractions: {tech}[type constructors
 
 :::
 
-{keywordOf Lean.Parser.Command.declaration parser:=Lean.Parser.Command.definition}`def` のようなキーワードで定義された関数定義は {keywordOf Lean.Parser.Term.fun}`fun` に脱糖されます。しかし、すべての関数が抽象されたものではありません： {tech}[type constructors] ・ {tech}[constructors] ・ {tech}[recursors] は関数型を持つ場合がありますが、関数抽象だけでは定義できません。
+{keywordOf Lean.Parser.Command.declaration parser:=Lean.Parser.Command.definition}`def` のようなキーワードで定義された関数定義は {keywordOf Lean.Parser.Term.fun}`fun` に脱糖されます。しかし、すべての関数が抽象されたものではありません： {tech}[型コンストラクタ] ・ {tech}[コンストラクタ] ・ {tech}[再帰子] は関数型を持つ場合がありますが、関数抽象だけでは定義できません。
 
 :::comment
 # Currying
@@ -687,7 +687,7 @@ These operations result in an arbitrarily chosen inhabitant of the type in Lean'
 
 :::
 
-同様に、配列への範囲外アクセスなど、コンパイルされたコードでは実行時に失敗するはずの操作は、結果の型が inhabited であることが分かっている場合にのみ使用することができます。これらの操作の結果、Lean のロジックでは型の住人が任意に選ばれます（具体的には、その型の {name}`Inhabited` インスタンスで指定されたもの）。
+同様に、配列への範囲外アクセスなど、コンパイルされたコードではランタイムに失敗するはずの操作は、結果の型が inhabited であることが分かっている場合にのみ使用することができます。これらの操作の結果、Lean のロジックでは型の住人が任意に選ばれます（具体的には、その型の {name}`Inhabited` インスタンスで指定されたもの）。
 
 :::comment
 ::example "Panic"
diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean
index 3366780..5ba02d7 100644
--- a/Manual/Language/InductiveTypes.lean
+++ b/Manual/Language/InductiveTypes.lean
@@ -16,29 +16,57 @@ open Lean.Parser.Command («inductive» «structure» declValEqns computedField)
 
 set_option maxRecDepth 800
 
+/-
 #doc (Manual) "Inductive Types" =>
+-/
+#doc (Manual) "帰納型" =>
 
+:::comment
 {deftech}_Inductive types_ are the primary means of introducing new types to Lean.
-While {tech}[universes] and {tech}[関数]functions are built-in primitives that could not be added by users, every other type in Lean is either an inductive type or defined in terms universes, functions, and inductive types..
+While {tech}[universes] and {tech}[functions] are built-in primitives that could not be added by users, every other type in Lean is either an inductive type or defined in terms universes, functions, and inductive types..
 Inductive types are specified by their {deftech}_type constructors_ {index}[type constructor] and their {deftech}_constructors_; {index}[constructor] their other properties are derived from these.
 Each inductive type has a single type constructor, which may take both {tech}[universe parameters] and ordinary parameters.
 Inductive types may have any number of constructors; these constructors introduce new values whose types are headed by the inductive type's type constructor.
 
+:::
+
+{deftech}_帰納型_ （inductive type）は Lean に新しい型を導入する主な手段です。 {tech}[universes] と {tech}[関数] は組み込みのプリミティブでユーザが追加することはできませんが、Lean の他のすべての型は帰納型であるか、宇宙・関数・帰納型によって定義されたものであるかのどちらかです。帰納型は {deftech}_型コンストラクタ_ （type constructor）{index}[type constructor] と {deftech}_コンストラクタ_ （constructor） {index}[constructor] によって指定されます；帰納型の性質はこれらから導かれます。各帰納型は1つの型コンストラクタを持ち、 {tech}[universe parameters] と通常のパラメータの両方を取ることができます。帰納型は任意の数のコンストラクタを持つことができます；これらのコンストラクタは帰納型の型コンストラクタによって型が導かれる新しい値を導入します。
+
+:::comment
 Based on the type constructor and the constructors for an inductive type, Lean derives a {deftech}_recursor_{index}[recursor]{see "recursor"}[eliminator].
 Logically, recursors represent induction principles or elimination rules; computationally, they represent primitive recursive computations.
 The termination of recursive functions is justified by translating them into uses of the recursors, so Lean's kernel only needs to perform type checking of recursor applications, rather than including a separate termination analysis.
 Lean additionally produces a number of helper constructions based on the recursor,{margin}[The term _recursor_ is always used, even for non-recursive datatypes.] which are used elsewhere in the system.
 
 
+:::
+
+帰納型の型コンストラクタとコンストラクタに基づいて、Lean は {deftech}_再帰子_{index}[recursor]{see "recursor"}[eliminator] （recursor）を導出します。論理的には、再帰子は帰納原理や除去則を表し、計算上はプリミティブな再帰計算を表します。再帰関数の停止は、再帰子の使用に変換することで正当化されるため、Lean のカーネルは再帰子の適用の型チェックを行うだけでよく、停止性の分析を別途行う必要はありません。Lean はさらに、システムの他の場所でも使用される再帰子 {margin}[_再帰子_ という用語は再帰的でないデータ型でも常に使用されます。] に基づいた数多くの補助的な構成を提供しています。
+
+:::comment
 _Structures_ are a special case of inductive types that have exactly one constructor.
 When a structure is declared, Lean generates helpers that enable additional language features to be used with the new structure.
 
+:::
+
+_構造体_ （structure）はコンストラクタを1つだけ持つ帰納型の特殊なケースです。構造体が宣言されると、Lean は新しい構造体で追加の言語機能を使用できるようにする補助関数を生成します。
+
+:::comment
 This section describes the specific details of the syntax used to specify both inductive types and structures, the new constants and definitions in the environment that result from inductive type declarations, and the run-time representation of inductive types' values in compiled code.
 
+:::
+
+本節では、帰納型と構造体の両方を指定するために使用される構文の具体的な詳細・帰納型の宣言から生じる環境内の新しい定数と定義・コンパイルされたコードにおける帰納型の値のランタイム表現について説明します。
+
+:::comment
 # Inductive Type Declarations
 
 
-:::syntax command (alias := «inductive»)
+:::
+
+# 帰納型の宣言
+
+::::syntax command (alias := «inductive»)
 ```grammar
 $_:declModifiers
 inductive $d:declId $_:optDeclSig where
@@ -46,62 +74,133 @@ inductive $d:declId $_:optDeclSig where
 $[deriving $[$_ $[with $_]?],*]?
 ```
 
+:::comment
 Declares a new inductive type.
 The meaning of the {syntaxKind}`declModifiers` is as described in the section {ref "declaration-modifiers"}[on declaration modifiers].
 :::
 
+新しい帰納型を宣言します。 {syntaxKind}`declModifiers` の意味は {ref "declaration-modifiers"}[宣言修飾子について] の節で説明した通りです。
+
+::::
+
+:::comment
 After declaring an inductive type, its type constructor, constructors, and recursor are present in the environment.
 New inductive types extend Lean's core logic—they are not encoded or represented by some other already-present data.
 Inductive type declarations must satisfy {ref "well-formed-inductives"}[a number of well-formedness requirements] to ensure that the logic remains consistent.
 
+:::
+
+帰納型を宣言すると、その型コンストラクタ・コンストラクタ・再帰子が環境に現れます。新しい帰納型は Lean のコア論理を拡張します。それらは既に存在する他のデータによってエンコードされたり表現されたりすることはありません。帰納型の宣言は、論理の一貫性を保つために {ref "well-formed-inductives"}[多くの適格な要件] を満たす必要があります。
+
+:::comment
 The first line of the declaration, from {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`inductive` to {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where`, specifies the new {tech}[type constructor]'s name and type.
 If a type signature for the type constructor is provided, then its result type must be a {tech}[universe], but the parameters do not need to be types.
 If no signature is provided, then Lean will attempt to infer a universe that's just big enough to contain the resulting type.
 In some situations, this process may fail to find a minimal universe or fail to find one at all, necessitating an annotation.
 
+:::
+
+宣言の最初の行にて、 {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`inductive` から {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where` までは新しい {tech}[型コンストラクタ] の名前と型を指定しています。型コンストラクタの型シグネチャが提供されている場合、その結果の型は {tech}[universe] でなければなりませんが、パラメータは型である必要はありません。シグネチャが提供されない場合、Lean は結果の型を含むのに十分な大きさの宇宙を推論しようとします。状況によってはこのプロセスは最小の宇宙を見つけることができなかったり、全く見つけることができなかったりすることがあり、その場合は注釈が必要です。
+
+:::comment
 The constructor specifications follow {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where`.
 Constructors are not mandatory, as constructorless datatypes such as {lean}`False` and {lean}`Empty` are perfectly sensible.
 Each constructor specification begins with a vertical bar (`'|'`, Unicode `'VERTICAL BAR' (U+007c)`), declaration modifiers, and a name.
-The name is a {tech}[生識別子]raw identifier.
+The name is a {tech}[raw identifier].
 A declaration signature follows the name.
 The signature may specify any parameters, modulo the well-formedness requirements for inductive type declarations, but the return type in the signature must be a saturated application of the type constructor of the inductive type being specified.
 If no signature is provided, then the constructor's type is inferred by inserting sufficient implicit parameters to construct a well-formed return type.
 
+:::
+
+コンストラクタの仕様は {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`where` の後に続きます。コンストラクタは必須ではありません。コンストラクタのないデータ型としては {lean}`False` と {lean}`Empty` などがまさに当てはまります。各コンストラクタの指定は、縦棒（`'|'`、Unicode `'VERTICAL BAR' (U+007c)`）・宣言修飾子・名前で始まります。名前は {tech}[生識別子] です。宣言シグネチャは名前の後に続きます。シグネチャは帰納的宣言の適格要件に従って任意のパラメータを指定することができますが、シグネチャの戻り型は指定された帰納型の型コンストラクタを完全に適用したものでなければなりません。シグネチャが提供されない場合、コンストラクタの型は適格な戻り値を構成するのに十分な暗黙のパラメータを挿入することによって推測されます。
+
+:::comment
 The new inductive type's name is defined in the {tech}[current namespace].
 Each constructor's name is in the inductive type's namespace.{index subterm:="of inductive type"}[namespace]
 
+:::
+
+新しい帰納型の名前は {tech}[current namespace] で定義されます。各コンストラクタの名前は帰納型の名前空間にあります。 {index subterm:="of inductive type"}[namespace]
+
+:::comment
 ## Parameters and Indices
 
+:::
+
+## パラメータと添字
+
+:::comment
 Type constructors may take two kinds of arguments: {deftech}_parameters_ {index subterm:="of inductive type"}[parameter] and {deftech key:="index"}_indices_.{index subterm:="of inductive type"}[index]
 Parameters must be used consistently in the entire definition; all occurrences of the type constructor in each constructor in the declaration must take precisely the same argument.
 Indices may vary among the occurrences of the type constructor.
 All parameters must precede all indices in the type constructor's signature.
 
+:::
+
+型コンストラクタは2種類の引数を取ることができます： {deftech}_パラメータ_ {index subterm:="of inductive type"}[parameter] （parameter）と {deftech key:="index"}_添字_ {index subterm:="of inductive type"}[index] （index, indices）です。パラメータは定義全体で一貫して使用されなければなりません；宣言内の各コンストラクタで型コンストラクタが出現する場合は、すべて正確に同じ引数を取る必要があります。添字は型コンストラクタの出現箇所によって異なっていてもかまいません。すべてのパラメータは、型コンストラクタのシグネチャのすべての添字の前にいなければなりません。
+
+:::comment
 Parameters that occur prior to the colon (`':'`) in the type constructor's signature are considered parameters to the entire inductive type declaration.
 They are always parameters that must be uniform throughout the type's definition.
 Generally speaking, parameters that occur after the colon are indices that may vary throughout the definition of the type.
 However, if the option {option}`inductive.autoPromoteIndices` is {lean}`true`, then syntactic indices that could have been parameters are made into parameters.
 An index could have been a parameter if all of its type dependencies are themselves parameters and it is used uniformly as an uninstantiated variable in all occurrences of the inductive type's type constructor in all constructors.
 
+:::
+
+型コンストラクタのシグネチャのコロン（`':'`）より前に現れるパラメータは帰納型宣言全体に対するパラメータと見なされます。これらは常に型の定義全体を通して一様でなければならないパラメータです。一般的に言えば、コロンの後にあるパラメータは型の定義全体を通して変化する可能性のある添字です。しかし、オプション {option}`inductive.autoPromoteIndices` が {lean}`true` の場合、パラメータになる可能性のある構文としては添字のものがパラメータになります。添字がパラメータである可能性があるのは、その型の依存関係がすべてパラメータであり、帰納型の型コンストラクタのすべてのコンストラクタで一律にインスタンス化されていない変数として使用される場合です。
+
 {optionDocs inductive.autoPromoteIndices}
 
+:::comment
 Indices can be seen as defining a _family_ of types.
 Each choice of indices selects a type from the family, which has its own set of available constructors.
 Type constructors that take index parameters are referred to as {deftech}_indexed families_ {index subterm:="of types"}[indexed family] of types.
 
+:::
+
+添字は型の _族_ （family）を定義していると見なすことができます。添字を選択するごとに、その族から型が選択され、その型は使用可能なコンストラクタのあつまりを持ちます。添字のパラメータを取る型のコンストラクタは {deftech}_添字族_ {index subterm:="of types"}[indexed family] （indexed family）と呼ばれます、
+
+:::comment
 ## Example Inductive Types
 
-:::example "A constructorless type"
+:::
+
+## 帰納型の例
+
+:::comment
+::example "A constructorless type"
+:::
+::::example "コンストラクタの無い型"
+:::comment
 {lean}`Zero` is an empty datatype, equivalent to Lean's {lean}`Empty` type:
+:::
+
+{lean}`Zero` は空のデータ型であり、Lean の {lean}`Empty` 型と同値です：
+
 ```lean
 inductive Zero : Type where
 ```
 
+:::comment
 Empty datatypes are not useless; they can be used to indicate unreachable code.
 :::
 
-:::example "A constructorless proposition"
+空のデータ型は無用なものではありません；到達不可能なコードを示すために使うことができます。
+
+::::
+
+:::comment
+::example "A constructorless proposition"
+:::
+::::example "コンストラクタの無い命題"
+:::comment
 {lean}`No` is a false {tech}[proposition], equivalent to Lean's {lean}`False`:
+:::
+
+{lean}`No` は偽の {tech}[proposition] であり、Lean の {lean}`False` と同値です：
+
 ```lean
 inductive No : Prop where
 ```
@@ -111,48 +210,84 @@ theorem no_is_false : No = False := by
   apply propext
   constructor <;> intro h <;> cases h
 ```
-:::
+::::
 
-:::example "A unit type"
+:::comment
+::example "A unit type"
+:::
+::::example "ユニット型"
+:::comment
 {lean}`One` is equivalent to Lean's {lean}`Unit` type:
+:::
+
+{lean}`One` は Lean の {lean}`Unit` 型と同値です：
+
 ```lean
 inductive One where
   | one
 ```
+:::comment
 It is an example of an inductive type in which the signatures have been omitted for both the type constructor and the constructor.
 Lean assigns {lean}`One` to {lean}`Type`:
+:::
+
+これは型コンストラクタとコンストラクタの両方のシグネチャが省略された帰納型の例です。Lean は {lean}`One` を {lean}`Type` に割り当てます：
+
 ```lean (name := OneTy)
 #check One
 ```
 ```leanOutput OneTy
 One : Type
 ```
+:::comment
 The constructor is named {lean}`One.one`, because constructor names are the type constructor's namespace.
 Because {lean}`One` expects no arguments, the signature inferred for {lean}`One.one` is:
+:::
+
+コンストラクタ名は型コンストラクタの名前空間にあるため、コンストラクタ名は {lean}`One.one` です。 {lean}`One` は引数を期待しないため、 {lean}`One.one` のシグネチャは次のようになります：
+
 ```lean (name := oneTy)
 #check One.one
 ```
 ```leanOutput oneTy
 One.one : One
 ```
-:::
+::::
 
 
-:::example "A true proposition"
+:::comment
+::example "A true proposition"
+:::
+::::example "真である命題"
+:::comment
 {lean}`Yes` is equivalent to Lean's {lean}`True` proposition:
 
+:::
+
+{lean}`Yes` は Lean の {lean}`True` 命題と同値です：
+
 ```lean
 inductive Yes : Prop where
   | intro
 ```
+:::comment
 Unlike {lean}`One`, the new inductive type {lean}`Yes` is specified to be in the {lean}`Prop` universe.
+:::
+
+{lean}`One` と異なり、この新しい帰納型 {lean}`Yes` は {lean}`Prop` 宇宙にあることが指定されています。
+
 ```lean (name := YesTy)
 #check Yes
 ```
 ```leanOutput YesTy
 Yes : Prop
 ```
+:::comment
 The signature inferred for {lean}`Yes.intro` is:
+:::
+
+{lean}`Yes.intro` のシグネチャは以下のように推測されます：
+
 ```lean (name := yesTy)
 #check Yes.intro
 ```
@@ -165,33 +300,51 @@ theorem yes_is_true : Yes = True := by
   apply propext
   constructor <;> intros <;> constructor
 ```
-:::
+::::
 
-::::example "A type with parameter and index"
+:::comment
+::example "A type with parameter and index"
+:::
+:::::example "パラメータと添字のある型"
 
-:::keepEnv
+::::keepEnv
 ```lean (show:=false)
 universe u
 axiom α : Type u
 axiom b : Bool
 ```
 
+:::comment
 An {lean}`EvenOddList α b` is a list where {lean}`α` is the type of the data stored in the list and {lean}`b` is {lean}`true` when there are an even number of entries:
 :::
 
+{lean}`EvenOddList α b` はリストで、 {lean}`α` はリストに格納されているデータの型、 {lean}`b` はエントリの数が偶数の時に {lean}`true` となります：
+
+::::
+
 ```lean
 inductive EvenOddList (α : Type u) : Bool → Type u where
   | nil : EvenOddList α true
   | cons : α → EvenOddList α isEven → EvenOddList α (not isEven)
 ```
 
+:::comment
 This example is well typed because there are two entries in the list:
+:::
+
+この例では、リストに2つのエントリがあるため、正しく型付けられています：
+
 ```lean
 example : EvenOddList String true :=
   .cons "a" (.cons "b" .nil)
 ```
 
+:::comment
 This example is not well typed because there are three entries in the list:
+:::
+
+この例では、リストに3つのエントリがあるため、型付けは正しくありません：
+
 ```lean (error := true) (name := evenOddOops)
 example : EvenOddList String true :=
   .cons "a" (.cons "b" (.cons "c" .nil))
@@ -205,17 +358,22 @@ but is expected to have type
   EvenOddList String true : Type
 ```
 
-:::keepEnv
+::::keepEnv
 ```lean (show:=false)
 universe u
 axiom α : Type u
 axiom b : Bool
 ```
 
+:::comment
 In this declaration, {lean}`α` is a {tech}[parameter], because it is used consistently in all occurrences of {name}`EvenOddList`.
 {lean}`b` is an {tech}[index], because different {lean}`Bool` values are used for it at different occurrences.
 :::
 
+この宣言では、 {lean}`α` は {tech}[パラメータ] です。なぜなら、これは {name}`EvenOddList` のすべての出現で一貫して使用されているからです。 {lean}`b` は {tech}[index] であり、異なる出現で異なる {lean}`Bool` 値が使用されるからです。
+
+::::
+
 
 ```lean (show:=false) (keep:=false)
 def EvenOddList.length : EvenOddList α b → Nat
@@ -229,20 +387,33 @@ theorem EvenOddList.length_matches_evenness (xs : EvenOddList α b) : b = (xs.le
     simp [length]
     cases b' <;> simp only [Bool.true_eq_false, false_iff, true_iff] <;> simp at ih <;> omega
 ```
-::::
+:::::
 
-:::::keepEnv
-::::example "Parameters before and after the colon"
+::::::keepEnv
+:::comment
+::example "Parameters before and after the colon"
+:::
+:::::example "コロンの前後にあるパラメータ"
 
+:::comment
 In this example, both parameters are specified before the colon in {name}`Either`'s signature.
 
+:::
+
+この例では、パラメータはどちらも {name}`Either` のシグネチャにおいてコロンの前に指定されています。
+
 ```lean
 inductive Either (α : Type u) (β : Type v) : Type (max u v) where
   | left : α → Either α β
   | right : α → Either α β
 ```
 
+:::comment
 In this version, there are two types named `α` that might not be identical:
+:::
+
+このバージョンでは `α` という名前の型が2つあり、同一ではないかもしれません：
+
 ```lean (name := Either') (error := true)
 inductive Either' (α : Type u) (β : Type v) : Type (max u v) where
   | left : {α : Type u} → {β : Type v} → α → Either' α β
@@ -255,50 +426,93 @@ expected
   α✝
 ```
 
+:::comment
 Placing the parameters after the colon results in parameters that can be instantiated by the constructors:
+:::
+
+コロンの後にパラメータを置くと、コンストラクタでインスタンス化できるパラメータになります：
+
 ```lean (name := Either'')
 inductive Either'' : Type u → Type v → Type (max u v) where
   | left : {α : Type u} → {β : Type v} → α → Either'' α β
   | right : α → Either'' α β
 ```
+:::comment
 {name}`Either''.right`'s type parameters are discovered via Lean's ordinary rules for {tech}[automatic implicit] parameters.
-::::
+:::
+
+{name}`Either''.right` の型パラメータは Lean の {tech}[automatic implicit] パラメータに関する通常のルールによって発見されます。
+
 :::::
+::::::
 
 
+:::comment
 ## Anonymous Constructor Syntax
 
+:::
+
+## 匿名コンストラクタ構文
+
+:::comment
 If an inductive type has just one constructor, then this constructor is eligible for {deftech}_anonymous constructor syntax_.
 Instead of writing the constructor's name applied to its arguments, the explicit arguments can be enclosed in angle brackets (`'⟨'` and `'⟩'`, Unicode `MATHEMATICAL LEFT ANGLE BRACKET	(U+0x27e8)` and `MATHEMATICAL RIGHT ANGLE BRACKET	(U+0x27e9)`) and separated with commas.
 This works in both pattern and expression contexts.
 Providing arguments by name or converting all implicit parameters to explicit with `@` requires using the ordinary constructor syntax.
 
-::::example "Anonymous constructors"
+:::
+
+帰納型がコンストラクタを1つだけ持つ場合、このコンストラクタは {deftech}_匿名コンストラクタ構文_ （anonymous constructor syntax）の対象となります。コンストラクタの名前を引数に適用して書く代わりに、明示的な引数を角括弧（`'⟨'` と `'⟩'`、Unicode `MATHEMATICAL LEFT ANGLE BRACKET	(U+0x27e8)` と `MATHEMATICAL RIGHT ANGLE BRACKET	(U+0x27e9)`）で囲み、カンマで区切ることができます。これはパターンと式の両方のコンテキストで動作します。引数を名前で指定したり、すべての暗黙的なパラメータを `@` で明示的なものに変換したりするには、通常のコンストラクタ構文を使用する必要があります。
 
-:::keepEnv
+:::comment
+::example "Anonymous constructors"
+:::
+:::::example "匿名コンストラクタ"
+
+::::keepEnv
 ```lean (show:=false)
 axiom α : Type
 ```
+:::comment
 The type {lean}`AtLeastOne α` is similar to `List α`, except there's always at least one element present:
 :::
 
+型 {lean}`AtLeastOne α` は `List α` と似ていますが、少なくとも1つの要素が常に存在します：
+
+::::
+
 ```lean
 inductive AtLeastOne (α : Type u) : Type u where
   | mk : α → Option (AtLeastOne α) → AtLeastOne α
 ```
 
+:::comment
 Anonymous constructor syntax can be used to construct them:
+:::
+
+匿名コンストラクタ構文を使ってこれを構成することができます：
+
 ```lean
 def oneTwoThree : AtLeastOne Nat :=
   ⟨1, some ⟨2, some ⟨3, none⟩⟩⟩
 ```
+:::comment
 and to match against them:
+:::
+
+また、この型の値にマッチすることができます：
+
 ```lean
 def AtLeastOne.head : AtLeastOne α → α
   | ⟨x, _⟩ => x
 ```
 
+:::comment
 Equivalently, traditional constructor syntax could have been used:
+:::
+
+上記と同等に、通常のコンストラクタ構文も使うことが可能です：
+
 ```lean
 def oneTwoThree' : AtLeastOne Nat :=
   .mk 1 (some (.mk 2 (some (.mk 3 none))))
@@ -306,118 +520,287 @@ def oneTwoThree' : AtLeastOne Nat :=
 def AtLeastOne.head' : AtLeastOne α → α
   | .mk x _ => x
 ```
-::::
+:::::
 
 
+:::comment
 ## Deriving Instances
 
+:::
+
+## インスタンスの導出
+
+:::comment
 The optional {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`deriving` clause of an inductive type declaration can be used to derive instances of type classes.
 Please refer to {ref "deriving-instances"}[the section on instance deriving] for more information.
 
 
+:::
+
+帰納的宣言のオプションとして、 {keywordOf Lean.Parser.Command.declaration (parser:=«inductive»)}`deriving` 節は、型クラスのインスタンスを導出するために使用することができます。詳細は {ref "deriving-instances"}[インスタンス導出についての節] を参照してください。
+
 {include 0 Manual.Language.InductiveTypes.Structures}
 
 {include 0 Manual.Language.InductiveTypes.LogicalModel}
 
-# Run-Time Representation
+# ランタイム表現
 %%%
 tag := "run-time-inductives"
 %%%
 
+:::comment
+// include の直後だとエラーになったため場所移動
+# Run-Time Representation
+:::
+
+:::comment
 An inductive type's run-time representation depends both on how many constructors it has, how many arguments each constructor takes, and whether these arguments are {tech}[relevant].
 
+:::
+
+帰納型のランタイム表現は、それがいくつのコンストラクタを持つか・各コンストラクタがいくつの引数を取り、それらの引数が {tech}[relevant] であるかどうかの両方に依存します。
+
+:::comment
 ## Exceptions
 
+:::
+
+## 例外
+
+:::comment
 Not every inductive type is represented as indicated here—some inductive types have special support from the Lean compiler:
-:::keepEnv
+:::
+
+すべての帰納型がここで示されているように表現されるわけではありません。いくつかの帰納型は Lean のコンパイラによって特別にサポートされています：
+
+::::keepEnv
 ````lean (show := false)
 axiom α : Prop
 ````
 
+:::comment
  * The fixed-width integer types {lean}`UInt8`, ..., {lean}`UInt64`, and {lean}`USize` are represented by the C types `uint8_t`, ..., `uint64_t`, and `size_t`, respectively.
 
+:::
+
+ * 固定幅整数 {lean}`UInt8`, ..., {lean}`UInt64` ・ {lean}`USize` は、それぞれ C の `uint8_t`, ..., `uint64_t` と `size_t` 型で表されます。
+
+:::comment
  * {lean}`Char` is represented by `uint32_t`
 
+:::
+
+ * {lean}`Char` は `uint32_t` で表現されます。
+
+:::comment
  * {lean}`Float` is represented by `double`
 
+:::
+
+ * {lean}`Float` は `double` で表現されます。
+
+:::comment
  * An {deftech}_enum inductive_ type of at least 2 and at most $`2^32` constructors, each of which has no parameters, is represented by the first type of `uint8_t`, `uint16_t`, `uint32_t` that is sufficient to assign a unique value to each constructor. For example, the type {lean}`Bool` is represented by `uint8_t`, with values `0` for {lean}`false` and `1` for {lean}`true`. {TODO}[Find out whether this should say "no relevant parameters"]
 
+:::
+
+ * {deftech}_列挙帰納的_ （enum inductive）型は少なくとも2個から最大 $`2^32` 個のコンストラクタを持ち、各コンストラクタはパラメータを持ちませんが、 `uint8_t` ・ `uint16_t` ・ `uint32_t` のうち各コンストラクタに一意な値を割り当てるのに十分な最初の型によって表現されます。例えば、 {lean}`Bool` 型は `uint8_t` で表現され、 {lean}`false` の場合は `0` 、 {lean}`true` の場合は `1` になります。
+
+:::comment
  * {lean}`Decidable α` is represented the same way as `Bool` {TODO}[Aren't Decidable and Bool just special cases of the rules for trivial constructors and irrelevance?]
 
+:::
+
+ * {lean}`Decidable α` は `Bool` と同じように表現されます。
+
+:::comment
  * {lean}`Nat` is represented by `lean_object *`. Its run-time value is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is `1` (checked by `lean_is_scalar`), an encoded unboxed natural number (`lean_box`/`lean_unbox`). {TODO}[Move these to FFI section or Nat chapter]
+
 :::
 
+ * {lean}`Nat` は `lean_object *` で表現されます。そのランタイム値は不透明な bignum オブジェクトへのポインタか、または「ポインタ」の最下位ビットが `1` の場合（`lean_is_scalar` でチェックされます）、ボックス化解除された整数にエンコードされます（`lean_box`/`lean_unbox`）。
+
+::::
+
 ## Relevance
 
+:::comment
 Types and proofs have no run-time representation.
 That is, if an inductive type is a `Prop`, then its values are erased prior to compilation.
 Similarly, all theorem statements and types are erased.
 Types with run-time representations are called {deftech}_relevant_, while types without run-time representations are called {deftech}_irrelevant_.
 
-:::example "Types are irrelevant"
+:::
+
+型と証明はランタイム表現を持ちません。つまり、帰納型が `Prop` である場合、その値はコンパイル前に消去されます。同様に、すべての定理文と型は消去されます。ランタイム表現を持つ型を {deftech}_relevant_ と呼び、ランタイム表現を持たない型を {deftech}_irrelevant_ と呼びます。
+
+:::comment
+::example "Types are irrelevant"
+:::
+::::example "型は irrelevant である"
+:::comment
 Even though {name}`List.cons` has the following signature, which indicates three parameters:
+:::
+
+{name}`List.cons` は以下のように3つのパラメータを持つシグネチャにも関わらず：
+
 ```signature
 List.cons.{u} {α : Type u} : α → List α → List α
 ```
+:::comment
 its run-time representation has only two, because the type argument is run-time irrelevant.
 :::
 
-:::example "Proofs are irrelevant"
+このランタイム表現では2つのみのパラメータとなります。なぜなら、型引数はランタイムでは irrelevant だからです。
+
+::::
+
+:::comment
+::example "Proofs are irrelevant"
+:::
+::::example "証明は irrelevant である"
+:::comment
 Even though {name}`Fin.mk` has the following signature, which indicates three parameters:
+:::
+
+{name}`Fin.mk` は以下のように3つのパラメータを持つシグネチャにも関わらず：
+
 ```signature
 Fin.mk {n : Nat} (val : Nat) : val < n → Fin n
 ```
+:::comment
 its run-time representation has only two, because the proof is erased.
 :::
 
+このランタイム表現では2つのみのパラメータとなります。なぜなら、証明は消去されるからです。
+
+::::
+
+:::comment
 In most cases, irrelevant values simply disappear from compiled code.
 However, in cases where some representation is required (such as when they are arguments to polymorphic constructors), they are represented by a trivial value.
 
+:::
+
+ほとんどの場合、irrelevant な値は単にコンパイルされたコードから消えるだけです。しかし、何らかの表現が必要な場合（多相コンストラクタの引数など）、自明な値で表現されます。
+
+:::comment
 ## Trivial Wrappers
 
+:::
+
+## 自明なラッパ
+
+:::comment
 If an inductive type has exactly one constructor, and that constructor has exactly one run-time relevant parameter, then the inductive type is represented identically to its parameter.
 
-:::example "Zero-Overhead Subtypes"
+:::
+
+帰納型が正確に1つのコンストラクタを持ち、そのコンストラクタが正確に1つのランタイムにおいて relevant なパラメータを持つならば、帰納型はそのパラメータと同一のものとして表現されます。
+
+:::comment
+::example "Zero-Overhead Subtypes"
+:::
+::::example "オーバーヘッドのない部分型"
+:::comment
 The structure {name}`Subtype` bundles an element of some type with a proof that it satisfies a predicate.
 Its constructor takes four arguments, but three of them are irrelevant:
+:::
+
+構造体 {name}`Subtype` はある型の要素と、それがある述語を満たすことの証明を束ねたものです。コンストラクタは4つの引数を取りますが、そのうち3つは irrelevant です：
+
 ```signature
 Subtype.mk.{u} {α : Sort u} {p : α → Prop}
   (val : α) (property : p val) : Subtype p
 ```
+:::comment
 Thus, subtypes impose no runtime overhead in compiled code, and are represented identically to the type of the {name Subtype.val}`val` field.
 :::
 
+このように、部分型はコンパイルされたコードにおいてランタイムのオーバーヘッドを発生させず、 {name Subtype.val}`val` フィールドの型と同一のものとして表現されます。
+
+::::
+
+:::comment
 ## Other Inductive Types
 
+:::
+
+## その他の帰納型
+
+:::comment
 If an inductive type doesn't fall into one of the categories above, then its representation is determined by its constructors.
 Constructors without relevant parameters are represented by their index into the list of constructors, as unboxed unsigned machine integers (scalars).
 Constructors with relevant parameters are represented as an object with a header, the constructor's index, an array of pointers to other objects, and then arrays of scalar fields sorted by their types.
 The header tracks the object's reference count and other necessary bookkeeping.
 
+:::
+
+帰納型が上記のカテゴリのいずれにも属さない場合、その表現はコンストラクタによって決定されます。relevant なパラメータを持たないコンストラクタは、コンストラクタのリストへのインデックスによって表現され、ボックス化解除された符号なし機械整数（スカラー）として表現されます。relevant なパラメータを持つコンストラクタは、ヘッダ・コンストラクタのインデックス・他のオブジェクトへのポインタの配列・型の順に並べられたスカラーのフィールドの配列を持つオブジェクトとして表現されます。ヘッダはオブジェクトの参照カウントやその他の必要な記録を追跡します。
+
+:::comment
 Recursive functions are compiled as they are in most programming languages, rather than by using the inductive type's recursor.
 Elaborating recursive functions to recursors serves to provide reliable termination evidence, not executable code.
 
+:::
+
+再帰関数は帰納型の再帰子を使用するのではなく、ほとんどのプログラミング言語と同じようにコンパイルされます。再帰関数を再帰子にエラボレートするのは、実行ファイルのコードではなく、信頼された停止の根拠を提供するために役立てられます。
+
 ### FFI
 
+:::comment
 From the perspective of C, these other inductive types are represented by `lean_object *`.
 Each constructor is stored as a `lean_ctor_object`, and `lean_is_ctor` will return true.
 A `lean_ctor_object` stores the constructor index in its header, and the fields are stored in the `m_objs` portion of the object.
 
+:::
+
+C の観点では、これらの帰納型は `lean_object *` として表現されます。各コンストラクタは `lean_ctor_object` として格納され、`lean_is_ctor` は真を返します。`lean_ctor_object` はコンストラクタのインデックスをヘッダに格納し、フィールドはオブジェクトの `m_objs` 部分に格納されます。
+
+:::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:
 
+:::
+
+フィールドのメモリ順序は、宣言のフィールドの型とその並び順から導かれます。フィールドの並び順は以下に従います：
+
+:::comment
 * Non-scalar fields stored as `lean_object *`
 * Fields of type {lean}`USize`
 * Other scalar fields, in decreasing order by size
 
+:::
+
+* `lean_object *` として格納される非スカラーのフィールド
+* {lean}`USize` 型のフィールド
+* その他のスカラーのフィールドはサイズの降順で並ぶ
+
+:::comment
 Within each group the fields are ordered in declaration order. **Warning**: Trivial wrapper types still count toward a field being treated as non-scalar for this purpose.
 
+:::
+
+各グループ内では、フィールドは宣言順に並んでいます。**警告**：自明なラッパ型は、この目的のためにフィールドが非スカラーとして扱われます。
+
+:::comment
 * To access fields of the first kind, use `lean_ctor_get(val, i)` to get the `i`th non-scalar field.
 * To access {lean}`USize` fields, use `lean_ctor_get_usize(val, n+i)` to get the `i`th usize field and `n` is the total number of fields of the first kind.
 * To access other scalar fields, use `lean_ctor_get_uintN(val, off)` or `lean_ctor_get_usize(val, off)` as appropriate. Here `off` is the byte offset of the field in the structure, starting at `n*sizeof(void*)` where `n` is the number of fields of the first two kinds.
 
+:::
+
+* 最初の種類のフィールドにアクセスするには、 `lean_ctor_get(val, i)` を使って `i` 番目の非スカラーフィールドを取得します。
+* {lean}`USize` フィールドにアクセスするには、`lean_ctor_get_usize(val, n+i)` を使って `i` 番目の usize フィールドを取得します。`n` は最初の種類のフィールドの総数です。
+* その他のスカラーフィールドにアクセスするには、`lean_ctor_get_uintN(vai, off)` または `lean_ctor_get_usize(val, off)` を適切に使用します。ここで `off` は構造体内のフィールドのバイトオフセットであり、`n*sizeof(void*)` から始まります。`n` はその前の2種類のフィールドの数です。
+
 ::::keepEnv
 
+:::comment
 For example, a structure such as
+:::
+
+例えば、以下のような構造体があるとして、
+
 ```lean
 structure S where
   ptr_1 : Array Nat
@@ -434,8 +817,13 @@ structure S where
   sc32_1 : UInt32
   sc16_2 : UInt16
 ```
+:::comment
 would get re-sorted into the following memory order:
 
+:::
+
+これは以下のメモリ順序に再ソートされます：
+
 * {name}`S.ptr_1` - `lean_ctor_get(val, 0)`
 * {name}`S.ptr_2` - `lean_ctor_get(val, 1)`
 * {name}`S.ptr_3` - `lean_ctor_get(val, 2)`
@@ -457,15 +845,33 @@ Figure out how to test/validate/CI these statements
 :::
 
 
+:::comment
 # Mutual Inductive Types
 
+:::
+
+# 相互帰納型
+
+:::comment
 Inductive types may be mutually recursive.
 Mutually recursive definitions of inductive types are specified by defining the types in a `mutual ... end` block.
 
-:::example "Mutually Defined Inductive Types"
+:::
+
+帰納型は相互に再帰することができます。帰納型の相互再帰定義は `mutual ... end` ブロックの中での型の定義として指定されます。
+
+:::comment
+::example "Mutually Defined Inductive Types"
+:::
+::::example "相互に定義された帰納型"
+:::comment
 The type {name}`EvenOddList` in a prior example used a Boolean index to select whether the list in question should have an even or odd number of elements.
 This distinction can also be expressed by the choice of one of two mutually inductive datatypes {name}`EvenList` and {name}`OddList`:
 
+:::
+
+先の例の型 {name}`EvenOddList` は真偽値の添字を使用して問題のリストの要素数が偶数か奇数かを選択しました。この区別は、2つの相互帰納的データ型 {name}`EvenList` と {name}`OddList` のどちらかを選択することでも表現できます：
+
 ```lean
 mutual
   inductive EvenList (α : Type u) : Type u where
@@ -485,21 +891,49 @@ example : OddList String := .cons "x" (.cons "y" .nil)
 invalid dotted identifier notation, unknown identifier `OddList.nil` from expected type
   OddList String
 ```
-:::
+::::
 
+:::comment
 ## Requirements
 
+:::
+
+## 要件
+
+:::comment
 The inductive types declared in a `mutual` block are considered as a group; they must collectively satisfy generalized versions of the well-formedness criteria for non-mutually-recursive inductive types.
 This is true even if they could be defined without the `mutual` block, because they are not in fact mutually recursive.
 
+:::
+
+`mutual` ブロックで宣言された帰納型は1つのグループとして扱われます；これらはすべて非相互再帰帰納型の適格な基準を一般化したものを満たさなければなりません。これらは実は相互に再帰的ではないため、`mutual` ブロック無しで定義できた場合でも同様です。
+
+:::comment
 ### Mutual Dependencies
 
+:::
+
+### 相互依存
+
+:::comment
 Each type constructor's signature must be able to be elaborated without reference to the other inductive types in the `mutual` group.
 In other words, the inductive types in the `mutual` group may not take each other as arguments.
 The constructors of each inductive type may mention the other type constructors in the group in their parameter types, with restrictions that are a generalization of those for recursive occurrences in non-mutual inductive types.
 
-:::example "Mutual inductive type constructors may not mention each other"
+:::
+
+それぞれの型コンストラクタのシグネチャは、`mutual` グループ内の他の帰納型を参照することなくエラボレートできなければなりません。言い換えると、`mutual` グループ内の帰納型はお互いを引数として取ることはできません。それぞれの帰納型のコンストラクタは、非相互帰納型における再帰的な出現のための制限を一般化したもので、パラメータ型においてグループ内の他の型コンストラクタに言及することができます。
+
+:::comment
+::example "Mutual inductive type constructors may not mention each other"
+:::
+::::example "お互いに言及しない相互帰納型コンストラクタ"
+:::comment
 These inductive types are not accepted by Lean:
+:::
+
+これらの帰納型は Lean に許容されません：
+
 ```lean (error:=true) (name := mutualNoMention)
 mutual
   inductive FreshList (α : Type) (r : α → α → Prop) : Type where
@@ -511,21 +945,44 @@ mutual
 end
 ```
 
+:::comment
 The type constructors may not refer to the other type constructors in the `mutual` group, so `FreshList` is not in scope in the type constructor of `Fresh`:
+:::
+
+型コンストラクタは `mutual` グループの他の型コンストラクタを参照することはできないため、 `FreshList` は `Fresh` の型コンストラクタのスコープにありません：
+
 ```leanOutput mutualNoMention
 unknown identifier 'FreshList'
 ```
-:::
+::::
 
 
+:::comment
 ### Parameters Must Match
 
+:::
+
+### マッチすべきパラメータ
+
+:::comment
 All inductive types in the `mutual` group must have the same {tech}[parameters].
 Their indices may differ.
 
-::::keepEnv
-::: example "Differing numbers of parameters"
+:::
+
+`mutual` グループ内のすべての帰納型は同じ {tech}[パラメータ] を持たなければなりません。それらの添字は異なっていてもかまいません。
+
+:::::keepEnv
+:::comment
+:: example "Differing numbers of parameters"
+:::
+:::: example "パラメータ数が異なる場合"
+:::comment
 Even though `Both` and `OneOf` are not mutually recursive, they are declared in the same `mutual` block and must therefore have identical parameters:
+:::
+
+`Both` と `OneOf` は相互再帰的ではありませんが、同じ `mutual` ブロックで宣言されているため、同じパラメータを持たなければなりません：
+
 ```lean (name := bothOptional) (error := true)
 mutual
   inductive Both (α : Type u) (β : Type v) where
@@ -538,13 +995,21 @@ end
 ```leanOutput bothOptional
 invalid inductive type, number of parameters mismatch in mutually inductive datatypes
 ```
-:::
 ::::
+:::::
 
-::::keepEnv
-::: example "Differing parameter types"
+:::::keepEnv
+:::comment
+:: example "Differing parameter types"
+:::
+:::: example "パラメータの型が異なる場合"
+:::comment
 Even though `Many` and `OneOf` are not mutually recursive, they are declared in the same `mutual` block and must therefore have identical parameters.
 They both have exactly one parameter, but `Many`'s parameter is not necessarily in the same universe as `Optional`'s:
+:::
+
+`Many` と `OneOf` は相互再帰的ではありませんが、同じ `mutual` ブロックで宣言されているため、同じパラメータを持たなければなりません。両者は正確に1つのパラメータを持っていますが、`Many` のパラメータは `Optional` のパラメータと同じ宇宙にあるとは限りません：
+
 ```lean (name := manyOptional) (error := true)
 mutual
   inductive Many (α : Type) : Type u where
@@ -561,17 +1026,35 @@ invalid mutually inductive types, parameter 'α' has type
 but is expected to have type
   Type : Type 1
 ```
-:::
 ::::
+:::::
 
+:::comment
 ### Universe Levels
 
+:::
+
+### 宇宙レベル
+
+:::comment
 The universe levels of each inductive type in a mutual group must obey the same requirements as non-mutually-recursive inductive types.
 Additionally, all the inductive types in a mutual group must be in the same universe, which implies that their constructors are similarly limited with respect to their parameters' universes.
 
-::::example "Universe mismatch"
-:::keepEnv
+:::
+
+相互グループ内の各帰納型の宇宙レベルは、非相互再帰的な帰納型と同じ要件に従わなければなりません。さらに、相互グループ内のすべての帰納型は同じ宇宙でなければならず、これはそれらのコンストラクタがパラメータの宇宙に関して同様に制限されることを意味します。
+
+:::comment
+::example "Universe mismatch"
+:::
+:::::example "宇宙のミスマッチ"
+::::keepEnv
+:::comment
 These mutually-inductive types are a somewhat complicated way to represent run-length encoding of a list:
+:::
+
+これらの相互帰納型はリストの連長圧縮を表すやや複雑な方法です：
+
 ```lean
 mutual
   inductive RLE : List α → Type where
@@ -591,10 +1074,15 @@ example : RLE [1, 1, 2, 2, 3, 1, 1, 1] :=
   .nil
 ```
 
+:::comment
 Specifying {name}`PrefixRunOf` as a {lean}`Prop` would be sensible, but it cannot be done because the types would be in different universes:
 :::
 
-:::keepEnv
+{name}`PrefixRunOf` を {lean}`Prop` として指定するほうが感覚的ですが、型が異なる宇宙になるためできません：
+
+::::
+
+::::keepEnv
 ```lean (error :=true) (name := rleBad)
 mutual
   inductive RLE : List α → Type where
@@ -612,10 +1100,15 @@ invalid mutually inductive types, resulting universe mismatch, given
 expected type
   Type
 ```
-:::
+::::
 
-:::keepEnv
+::::keepEnv
+:::comment
 This particular property can be expressed by separately defining the well-formedness condition and using a subtype:
+:::
+
+この特殊な性質は、適格条件を個別に定義し、部分型を使用することで表現できます：
+
 ```lean
 def RunLengths α := List (α × Nat)
 def NoRepeats : RunLengths α → Prop
@@ -644,16 +1137,29 @@ example : RLE [1, 1, 2, 2, 3, 1, 1, 1] where
   runsMatch := by simp [RunsMatch]
   nonZero := by simp [NonZero]
 ```
-:::
 ::::
+:::::
 
 
 ### Positivity
+:::comment
 Each inductive type that is defined in the `mutual` group may occur only strictly positively in the types of the parameters of the constructors of all the types in the group.
 In other words, in the type of each parameter to each constructor in all the types of the group, none of the type constructors in the group occur to the left of any arrows, and none of them occur in argument positions unless they are an argument to an inductive datatype's type constructor.
 
-::: example "Mutual strict positivity"
+:::
+
+`mutual` グループで定義される各帰納型は、グループ内のすべての型のコンストラクタのパラメータの型中において strict positively にのみ出現可能です。言い換えると、グループ内のすべての型の各コンストラクタのパラメータの型では、グループ内のどの型コンストラクタも矢印の左側には出現せず、帰納的データ型の型コンストラクタの引き数でない限り引数の位置に出現しません。
+
+:::comment
+:: example "Mutual strict positivity"
+:::
+:::: example "相互に strict positivity"
+:::comment
 In the following mutual group, `Tm` occurs in a negative position in the argument to `Binding.scope`:
+:::
+
+以下の相互グループでは、`Tm` が `Binding.scope` の引数の negative な位置に出現しています：
+
 ```lean (error := true) (name := mutualHoas)
 mutual
   inductive Tm where
@@ -663,16 +1169,29 @@ mutual
     | scope : (Tm → Tm) → Binding
 end
 ```
+:::comment
 Because `Tm` is part of the same mutual group, it must occur only strictly positively in the arguments to the constructors of `Binding`.
 It occurs, however, negatively:
+:::
+
+`Tm` は同じ相互グループの一部であるため、`Binding` のコンストラクタの引数としては strict positive にのみ出現しなければなりません。しかし、ここでは negative に出現しています：
+
 ```leanOutput mutualHoas
 (kernel) arg #1 of 'Binding.scope' has a non positive occurrence of the datatypes being declared
 ```
-:::
+::::
 
-::: example "Nested positions"
+:::comment
+:: example "Nested positions"
+:::
+:::: example "ネストされた位置"
+:::comment
 The definitions of {name}`LocatedStx` and {name}`Stx` satisfy the positivity condition because the recursive occurrences are not to the left of any arrows and, when they are arguments, they are arguments to inductive type constructors.
 
+:::
+
+{name}`LocatedStx` と {name}`Stx` の定義は、再帰的な出現がどの矢印の左にもなく、引数である場合は帰納的な型コンストラクタの引数であるため、positivity の条件を満たします。
+
 ```lean
 mutual
   inductive LocatedStx where
@@ -682,17 +1201,30 @@ mutual
     | node (kind : String) (args : List LocatedStx)
 end
 ```
-:::
+::::
 
+:::comment
 ## Recursors
 
+:::
+
+## 再帰子
+
+:::comment
 Mutual inductive types are provided with primitive recursors, just like non-mutually-defined inductive types.
 These recursors take into account that they must process the other types in the group, and thus will have a motive for each inductive type.
 Because all inductive types in the `mutual` group are required to have identical parameters, the recursors still take the parameters first, abstracting them over the motives and the rest of the recursor.
 Additionally, because the recursor must process the group's other types, it will require cases for each constructor of each of the types in the group.
 The actual dependency structure between the types is not taken into account; even if an additional motive or constructor case is not really required due to there being fewer mutual dependencies than there could be, the generated recursor still requires them.
 
-::: example "Even and odd"
+:::
+
+相互帰納型には、非相互に定義された帰納型と同様に、プリミティブな再帰子が用意されています。これらの再帰子は、グループ内の他の型を処理しなければならないことを考慮し、それぞれの帰納型に対して動機を持つことになります。`mutual` グループ内のすべての帰納型は同一のパラメータを持つ必要があるため、再帰子はパラメータを最初に受け取り、動機と再帰子の残りの部分を抽象化します。さらに、再帰子はグループの他の型を処理する必要があるため、グループ内の各型コンストラクタについてのケースが必要になります。型の間の実施あの依存構造は考慮されません；相互依存関係が少ないことで追加の動機またはコンストラクタのケースが実際には必要ない場合でも、生成された再帰子はそれらを必要とします。
+
+:::comment
+:: example "Even and odd"
+:::
+::: example "偶奇"
 ```lean
 mutual
   inductive Even : Nat → Prop where
@@ -724,8 +1256,16 @@ Odd.rec
 
 :::
 
-:::example "Spuriously mutual types"
+:::comment
+::example "Spuriously mutual types"
+:::
+::::example "疑似的な相互型"
+:::comment
 The types {name}`Two` and {name}`Three` are defined in a mutual block, even though they do not refer to each other:
+:::
+
+型 {name}`Two` と {name}`Three` はお互いを参照しないにもかかわらず、相互ブロック内で定義されています：
+
 ```lean
 mutual
   inductive Two (α : Type) where
@@ -734,7 +1274,12 @@ mutual
     | mk : α → α → α → Three α
 end
 ```
+:::comment
 {name}`Two`'s recursor, {name}`Two.rec`, nonetheless requires a motive and a case for {name}`Three`:
+:::
+
+それにもかかわらず、 {name}`Two` の再帰子である {name}`Two.rec` は {name}`Three` の動機とケースを必要とします。
+
 ```signature
 Two.rec.{u} {α : Type}
   {motive_1 : Two α → Sort u}
@@ -743,9 +1288,18 @@ Two.rec.{u} {α : Type}
   ((a a_1 a_2 : α) → motive_2 (Three.mk a a_1 a_2)) → (t : Two α) → motive_1 t
 ```
 
-:::
+::::
 
+:::comment
 ## Run-Time Representation
 
+:::
+
+## ランタイム表現
+
+:::comment
 Mutual inductive types are represented identically to {ref "run-time-inductives"}[non-mutual inductive types] in compiled code and in the runtime.
 The restrictions on mutual inductive types exist to ensure Lean's consistency as a logic, and do not impact compiled code.
+:::
+
+相互帰納型はコンパイルされたコードでもランタイムでも {ref "run-time-inductives"}[非相互帰納型] と同一に表現されます。相互帰納型に対する制限は、Lean の論理としての一貫性を保証するために存在し、コンパイルされたコードには影響しません。
diff --git a/Manual/Language/InductiveTypes/LogicalModel.lean b/Manual/Language/InductiveTypes/LogicalModel.lean
index 7a07077..0530962 100644
--- a/Manual/Language/InductiveTypes/LogicalModel.lean
+++ b/Manual/Language/InductiveTypes/LogicalModel.lean
@@ -17,14 +17,14 @@ set_option maxRecDepth 800
 
 # Recursors
 
-Every inductive type is equipped with a {tech}[recursor].
+Every inductive type is equipped with a {tech}[再帰子]recursors.
 The recursor is completely determined by the signatures of the type constructor and the constructors.
 Recursors have function types, but they are primitive and are not definable using `fun`.
 
 ## Recursor Types
 
 The recursor takes the following parameters:
-: The inductive type's {tech}[parameters]
+: The inductive type's {tech}[パラメータ]parameters
 
   Because parameters are consistent, they can be abstracted over the entire recursor
 
diff --git a/Manual/Language/InductiveTypes/Structures.lean b/Manual/Language/InductiveTypes/Structures.lean
index 11e9b26..d3835d6 100644
--- a/Manual/Language/InductiveTypes/Structures.lean
+++ b/Manual/Language/InductiveTypes/Structures.lean
@@ -42,7 +42,7 @@ structure RecStruct where
 # Structure Parameters
 
 Just like ordinary inductive type declarations, the header of the structure declaration contains a signature that may specify both parameters and a resulting universe.
-Structures may not define {tech}[indexed families].
+Structures may not define {tech}[添字族]indexed families.
 
 # Fields
 
@@ -170,7 +170,7 @@ def NatStringBimap.insert
 ```
 :::
 
-Because structures are represented by single-constructor inductive types, their constructors can be invoked or matched against using {tech}[anonymous constructor syntax].
+Because structures are represented by single-constructor inductive types, their constructors can be invoked or matched against using {tech}[匿名コンストラクタ構文]anonymous constructor syntax.
 Additionally, structures may be constructed or matched against using the names of the fields together with values for them.
 
 :::syntax term
@@ -379,7 +379,7 @@ example : toAcademicWork = Textbook.toAcademicWork := by
 The resulting structure's projections can be used as if its fields are simply the union of the parents' fields.
 The Lean elaborator automatically generates an appropriate accessor when it encounters a projection.
 Likewise, the field-based initialization and structure update notations hide the details of the encoding of inheritance.
-The encoding is, however, visible when using the constructor's name, when using {tech}[anonymous constructor syntax], or when referring to fields by their index rather than their name.
+The encoding is, however, visible when using the constructor's name, when using {tech}[匿名コンストラクタ構文]anonymous constructor syntax, or when referring to fields by their index rather than their name.
 
 :::: example "Field indices and structure inheritance"