diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 1b5e01e..4ed5787 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -22,5 +22,5 @@
 - [型推論](./type_checking/type_inference.md)
 - [定義上の同値](./type_checking/definitional_equality.md)
 - [簡約](./type_checking/reduction.md)
-- [Open issues & future work](./future_work.md)
-- [Further reading](./further_reading.md)
\ No newline at end of file
+- [課題と今後の展望](./future_work.md)
+- [その他の記事](./further_reading.md)
\ No newline at end of file
diff --git a/src/further_reading.md b/src/further_reading.md
index 4d572ff..e28eb83 100644
--- a/src/further_reading.md
+++ b/src/further_reading.md
@@ -1,19 +1,51 @@
+<!--
 # Further reading
+-->
 
+# その他の記事
+
+<!--
 + Mario Carneiro's [thesis on Lean's type theory](https://github.com/digama0/lean-type-theory)
+-->
+
++ Mario Carneiro による [Lean の型理論](https://github.com/digama0/lean-type-theory)
 
+<!--
 + Lean's official kernel: https://github.com/leanprover/lean4/tree/master/src/kernel
+-->
 
++ Lean 公式カーネル：https://github.com/leanprover/lean4/tree/master/src/kernel
+
+<!--
 + [lean4lean](https://github.com/digama0/lean4lean/tree/master), a reimplementation of Lean's kernel in Lean4.
+-->
+
++ [lean4lean](https://github.com/digama0/lean4lean/tree/master)、Lean 4 による Lean カーネルの再実装
 
+<!--
 + [lean4export](https://github.com/leanprover/lean4export), the recommended/official exporter for Lean 4 environments.
+-->
+
++ [lean4export](https://github.com/leanprover/lean4export)、Lean 4 環境のオフィシャル・推奨エクスポータ
 
 + [lean4checker](https://github.com/leanprover/lean4checker)
 
+<!--
 + Peter Dybjer's original description of the inductive types implemented by Lean: P. Dybjer. Inductive families. Formal aspects of computing, 6(4):440–465, 1994.
+-->
+
++ Peter Dybjer による Lean で実装される帰納型に関するオリジナルの記述：P. Dybjer. Inductive families. Formal aspects of computing, 6(4):440–465, 1994.
 
+<!--
 + Conor McBride and James McKinna's paper [_I am not a number: I am a free variable_](http://www.e-pig.org/downloads/notanum.pdf) describing the locally nameless approach to bound/free variables
+-->
 
++ Conor McBride と James McKinna の論文 [_I am not a number: I am a free variable_](http://www.e-pig.org/downloads/notanum.pdf) は束縛・自由変数への locally nameless なアプローチを記述しています。
+
+<!--
 + Information about non-positive occurrences in inductive types, from _Counterexamples in Type Systems_: https://counterexamples.org/strict-positivity.html?highlight=posi#positivity-strict-and-otherwise
+-->
+
++ 帰納型における positive ではない出現に関する情報、_Counterexamples in Type Systems_: https://counterexamples.org/strict-positivity.html?highlight=posi#positivity-strict-and-otherwise
 
 + Freek Wiedijk. Pollack-inconsistency. Electronic Notes in Theoretical Computer Science, 285:85–100, 2012
diff --git a/src/future_work.md b/src/future_work.md
index 4edef8d..f10623f 100644
--- a/src/future_work.md
+++ b/src/future_work.md
@@ -1,25 +1,73 @@
+<!--
 # Future work and open issues
+-->
 
+# 課題と今後の展望
+
+<!--
 ## File format
+-->
+
+## ファイルフォーマット
 
+<!--
 There is an open rfc [here](https://github.com/leanprover/lean4export/issues/3) about moving the export file format to json, which would be a major version change.
+-->
+
+エクスポートファイルのフォーマットをJSONに移行する件について、[こちら](https://github.com/leanprover/lean4export/issues/3) にオープンなRFCがあります。これは大きなバージョン変更になるでしょう。
 
+<!--
 ## Ensuring Nat/String are defined properly.
+-->
 
+## 整数・文字列が適切に定義されていることの確認
+
+<!--
 The Lean community has not yet settled on a particular solution for determining whether the declarations in an export file for `Nat`, `String`, and the operations covered by the relevant kernel extensions match those expected by extensions in a way that does not pull the exporter into the trusted code. 
+-->
+
+`Nat`・`String`・およびそれらに関連するカーネル拡張がカバーする操作のためのエクスポートファイルの宣言が、信頼されたコードにエクスポータを引き込まない方法で拡張が期待するものと一致するかどうかを判断するための特定の解決策について Lean コミュニティはまだ定まっていません。
 
+<!--
 An approach similar to that taken for `Eq` and the `Quot` declarations (defining them by hand within the type checker, then asserting they're the same) is not feasible due to the complexity of the fully elaborated terms for the supported binary operations on `Nat`.
+-->
+
+`Eq` と `Quot` の宣言のようなアプローチ（型チェッカ内で手作業で定義し、それらが同じであることを保証する）は `Nat` でサポートしているバイナリ演算のための完全にエラボレートされた項が複雑であるため実行不可能です。
 
+<!--
 ## Improving Pollack consistency
+-->
 
+## Pollack consistency の改善
+
+<!--
 Lean 4 offers very powerful facilities for defining custom syntax, macros, and pretty printer behaviors, and almost every aspect of Lean 4's internals is available to users. These elements of Lean's design were effective responses to real world feedback from the mathlib community during Lean 3's lifetime.
+-->
+
+Lean 4 はカスタム構文・マクロ・プリティプリンタの定義に非常に強力な機能を提供し、Lean 4 の内部のほとんどすべての側面がユーザによって利用可能です。Lean の設計のこれらの要素は Lean 3 の存続期間中に mathlib コミュニティから実際に寄せられたフィードバックに対する効果的な対応でした。
 
+<!--
 While these features were important factors in Lean's success as a tool for enabling large formalization efforts, they are also in tension with Lean4's Pollack consistency[^pollack], or lack thereof. Without replicating the macro and syntax extension capabilities in the pretty printer, type checkers cannot consistently read terms back to the user in a form that is recognizable. However, the idea of adding these features to a pretty printer is an unappealing expansion of the trusted code base. An alternative approach is to drop the pretty printer in favor of a trusted parser (ala metamath zero), but Lean's parser can be modified on the fly in userspace with custom syntax declarations.
+-->
+
+これらの機能は大規模な形式化作業を可能にするツールとして Lean が成功した重要な要因である一方、Lean 4 の Pollack consistency[^pollack] が危うく、もしくは損なわれる恐れがあります。プリティプリンタでマクロと構文拡張機能を複製しなければ、型チェッカは一貫して項を認識可能な形で読んでユーザに返すことができません。しかし、これらの機能をプリティプリンタに追加するアイデアは信頼されたコードベースを拡張する点においては魅力的なものではありません。別のアプローチとしてプリティプリンタをやめて、信頼できるパーサ（通称 metamath zero）を採用する方法もありますが、Lean のパーサはカスタム構文宣言を使ってユーザ空間でその場で変更することができます。
 
+<!--
 As Lean matures and adoption increases, there is likely to be a push for progress in the development of techniques and practices that allow users to take advantage of Lean's extensibility while sacrificing the least degree of Pollack consistency.
+-->
 
+Lean が成熟し、採用が進むにつれて Pollack consistency を犠牲にすることなく、ユーザが Lean の拡張性を活用できるような技術や手法の開発が進められるでしょう。
+
+<!--
 ## Forward reasoning
+-->
+
+## 前方推論
 
+<!--
 Existing type checkers implement a form of backward reasoning; an alternate strategy for type checking is to accept and check forward reasoning chains worked out by an external program, potentially allowing for an even simpler type checker.
+-->
+
+既存の型チェッカは後方推論の形式を実装しています；型チェッカの戦略の別路線として、外部プログラムによって作成された前方推論の連鎖を受け入れ、チェックすることがあり、これは後方推論よりもシンプルな型チェッカとなる可能性があります。
 
 [^pollack]: Freek Wiedijk. Pollack-inconsistency. Electronic Notes in Theoretical Computer Science, 285:85–100, 2012
\ No newline at end of file
diff --git a/src/type_checking/reduction.md b/src/type_checking/reduction.md
index e53eebb..7422eb7 100644
--- a/src/type_checking/reduction.md
+++ b/src/type_checking/reduction.md
@@ -1,20 +1,30 @@
-<!-- # Reduction -->
+<!--
+# Reduction
+-->
 
 # 簡約
 
-<!-- Reduction is about nudging expressions toward their [normal form](https://en.wikipedia.org/wiki/Normal_form_(abstract_rewriting)) so we can determine whether expressions are definitionally equal. For example, we need to perform beta reduction to determine that `(fun x => x) Nat.zero` is definitionally equal to `Nat.zero`, and delta reduction to determine that `id List.nil` is definitionally equal to `List.nil`.  -->
+<!--
+Reduction is about nudging expressions toward their [normal form](https://en.wikipedia.org/wiki/Normal_form_(abstract_rewriting)) so we can determine whether expressions are definitionally equal. For example, we need to perform beta reduction to determine that `(fun x => x) Nat.zero` is definitionally equal to `Nat.zero`, and delta reduction to determine that `id List.nil` is definitionally equal to `List.nil`. 
+-->
 
 簡約とは、式が定義上等しいかどうかを判定てきるように式を [正規形](https://ja.wikipedia.org/wiki/%E6%AD%A3%E8%A6%8F%E5%8C%96_(%E9%A0%85%E6%9B%B8%E3%81%8D%E6%8F%9B%E3%81%88)) に近づけることです。例えば、`(fun x => x) Nat.zero` が `Nat.zero` と定義上等しいと判断するためにβ簡約を行い、`id List.nil` が `List.nil` と定義上等しいと判断するためにδ簡約を行う必要があります。
 
-<!-- Reduction in Lean's kernel has two properties that introduce concerns which sometimes go unaddressed in basic textbook treatments of the topic. First, reduction in some cases is interleaved with inference. Among other things, this means reduction may need to be performed with open terms, even though the reduction procedures themselves are not creating free variables. Second, `const` expressions which are applied to multiple arguments may need to be considered together with those arguments during reduction (as in iota reduction), so sequences of applications need to be unfolded together at the beginning of reduction.  -->
+<!--
+Reduction in Lean's kernel has two properties that introduce concerns which sometimes go unaddressed in basic textbook treatments of the topic. First, reduction in some cases is interleaved with inference. Among other things, this means reduction may need to be performed with open terms, even though the reduction procedures themselves are not creating free variables. Second, `const` expressions which are applied to multiple arguments may need to be considered together with those arguments during reduction (as in iota reduction), so sequences of applications need to be unfolded together at the beginning of reduction. 
+-->
 
 Lean のカーネルにおける簡約には2つの性質がありますが、この分野を扱う基本的な教科書では触れられない恐れがあります。まず、場合によっては簡約と推論が同時に行われることがあります。とりわけ、たとえ簡約によって自由変数が生成されなくとも、これは開いた項で簡約を実行する必要があるかもしれないことを意味しています。第二に、複数の引数に適用される `const` 式は（ι簡約のように）簡約を行う中でそれらの引数を一緒に考慮する必要がある場合があり、簡約開始時に一連の適用を一緒に展開する必要があります。
 
-<!-- ## Beta reduction  -->
+<!--
+## Beta reduction 
+-->
 
 ## β簡約
 
-<!-- Beta reduction is about reducing function application. Concretely, the reduction: -->
+<!--
+Beta reduction is about reducing function application. Concretely, the reduction:
+-->
 
 β簡約は関数適用についての簡約です。具体的には、次の簡約です：
 
@@ -22,7 +32,9 @@ Lean のカーネルにおける簡約には2つの性質がありますが、
 (fun x => x) a    ~~>    a
 ```
 
-<!-- An implementation of beta reduction must despine an expression to collect any arguments in `app` expressions, check whether the expression to which they're applied is a lambda, then substitute the appropriate argument for any appearances of the corresponding bound variable in the function body: -->
+<!--
+An implementation of beta reduction must despine an expression to collect any arguments in `app` expressions, check whether the expression to which they're applied is a lambda, then substitute the appropriate argument for any appearances of the corresponding bound variable in the function body:
+-->
 
 β簡約の実装は `app` 式の引数を集め、それらが適用される式がラムダ式であるかどうかをチェックし、適切な引数を関数本体の対応する束縛変数の出現に置換するために式を手入れしなければなりません：
 
@@ -36,7 +48,9 @@ betaReduceAux f args:
   | _, _ => foldApps f args
 ```
 
-<!-- An important performance optimization for the instantiation (substitution) component of beta reduction is what's sometimes referred to as "generalized beta reduction", which involves gathering the arguments that have a corresponding lambda and substituting them in all at once. This optimization means that for `n` sequential lambda expressions with applied arguments, we only perform one traveral of the expression to substitute the appropriate arguments, instead of `n` traversals. -->
+<!--
+An important performance optimization for the instantiation (substitution) component of beta reduction is what's sometimes referred to as "generalized beta reduction", which involves gathering the arguments that have a corresponding lambda and substituting them in all at once. This optimization means that for `n` sequential lambda expressions with applied arguments, we only perform one traveral of the expression to substitute the appropriate arguments, instead of `n` traversals.
+-->
 
 β簡約のインスタンス化（置換）コンポーネントの重要なパフォーマンス最適化は、「generalized beta reduction」と呼ばれるもので、対応するラムダ式を持つ引数を集め、それらを一度に置換する方法です。この最適化は、適用された引数を持つ `n` 個の連続したラムダ式に対して、`n` 回の走査ではなく、適切な引数を代入するための1回の走査のみを実行することを意味します。
 
@@ -50,11 +64,15 @@ betaReduceAux f remArgs argsToApply:
   | _, _ => foldApps (inst f argsToApply) remArgs
 ```
 
-<!-- ## Zeta reduction (reducing `let` expressions) -->
+<!--
+## Zeta reduction (reducing `let` expressions)
+-->
 
 ## ζ簡約（`let` 式の簡約）
 
-<!-- Zeta reduction is a fancy name for reduction of `let` expressions. Concretely, reducing  -->
+<!--
+Zeta reduction is a fancy name for reduction of `let` expressions. Concretely, reducing 
+-->
 
 ζ簡約は `let` 式の簡約を表す大仰な名前です。具体的には、次の簡約です：
 
@@ -62,7 +80,9 @@ betaReduceAux f remArgs argsToApply:
 let (x : T) := y; x + 1    ~~>    (y : T) + 1
 ```
 
-<!-- An implementation can be as simple as: -->
+<!--
+An implementation can be as simple as:
+-->
 
 実装はシンプルであり、ほぼ次と同じです：
 
@@ -71,15 +91,21 @@ reduce Let _ val body:
   instantiate body val
 ```
 
-<!-- ## Delta reduction (definition unfolding) -->
+<!--
+## Delta reduction (definition unfolding)
+-->
 
 ## δ簡約（定義の展開）
 
-<!-- Delta reduction refers to unfolding definitions (and theorems). Delta reduction is done by replacing a `const ..` expr with the referenced declaration's value, after swapping out the declaration's generic universe parameters for the ones that are relevant to the current context.  -->
+<!--
+Delta reduction refers to unfolding definitions (and theorems). Delta reduction is done by replacing a `const ..` expr with the referenced declaration's value, after swapping out the declaration's generic universe parameters for the ones that are relevant to the current context. 
+-->
 
 δ簡約は定義（と定理）を展開することを指します。δ簡約は `const ..` 式について、その定義の多相宇宙パラメータを現在のコンテキストに関連した値で交換した後に、参照されている定義の値で置き換えることによって行われます。
 
-<!-- If the current environment contains a definition `x` which was declared with universe parameters `u*`and value `v`, then we may delta reduce an expression `Const(x, w*)` by replacing it with `val`, then substituting the universe parameters `u*` for those in `w*`. -->
+<!--
+If the current environment contains a definition `x` which was declared with universe parameters `u*`and value `v`, then we may delta reduce an expression `Const(x, w*)` by replacing it with `val`, then substituting the universe parameters `u*` for those in `w*`.
+-->
 
 現在の環境に定義 `x` があり、その定義が宇宙パラメータ `u*` と値 `v` で宣言されている場合、式 `Const(x, w*)` を `val` で置き換えてδ簡約し、宇宙パラメータ `u*` を `w*` に置き換えます。
 
@@ -89,27 +115,39 @@ deltaReduce Const name levels:
   substituteLevels (e := v) (ks := d.uparams) (vs := levels)
 ```
 
-<!-- If we had to remove any applied arguments to reach the `const` expression that was delta reduced, those arguments should be reapplied to the reduced definition. -->
+<!--
+If we had to remove any applied arguments to reach the `const` expression that was delta reduced, those arguments should be reapplied to the reduced definition.
+-->
 
 δ簡約された `const` 式に到達するために、適用された引数を簡約しなければならなかった場合、それらの引数は簡約された定義に再適用されなければなりません。
 
-<!-- ## Projection reduction -->
+<!--
+## Projection reduction
+-->
 
 ## 射影の簡約
 
-<!-- A `proj` expression has a natural number index indicating the field to be projected, and another expression which is the structure itself. The actual expression comprising the structure should be a sequence of arguments applied to `const` referencing a constructor. -->
+<!--
+A `proj` expression has a natural number index indicating the field to be projected, and another expression which is the structure itself. The actual expression comprising the structure should be a sequence of arguments applied to `const` referencing a constructor.
+-->
 
 `proj` 式は射影されるフィールドを表す自然数のインデックスと、構造体そのものを示す式を持ちます。構造体を構成する実際の式は、コンストラクタを参照する `const` に適用される一連の引き数でなければなりません。
 
-<!-- Keep in mind that for fully elaborated terms, the arguments to the constructor will include any parameters, so an instance of the `Prod` constructor would be e.g. `Prod.mk A B (a : A) (b : B)`. -->
+<!--
+Keep in mind that for fully elaborated terms, the arguments to the constructor will include any parameters, so an instance of the `Prod` constructor would be e.g. `Prod.mk A B (a : A) (b : B)`.
+-->
 
 ここで心に留めてもらいたいこととして、完全にエラボレートされた項に対して、コンストラクタの引数は任意のパラメータを含むため、`Prod` コンストラクタのインスタンスは例えば `Prod.mk A B (a : A) (b : B)` となります。
 
-<!-- The natural number indicating the projected field is 0-based, where 0 is the first *non-parameter* argument to the constructor, since a projection cannot be used to access the structure's parameters. -->
+<!--
+The natural number indicating the projected field is 0-based, where 0 is the first *non-parameter* argument to the constructor, since a projection cannot be used to access the structure's parameters.
+-->
 
 射影されたフィールドを示す自然数は0始まりであり、0はコンストラクタの最初の **非パラメータ** 引数です。というのも射影は構造体のパラメータのアクセスに使うことができないからです。
 
-<!-- With this in mind, it becomes clear that once we despine the constructor's arguments into `(constructor, [arg0, .., argN])`, we can reduce the projection by simply taking the argument at position `i + num_params`, where `num_params` is what it sounds like, the number of parameters for the structure type. -->
+<!--
+With this in mind, it becomes clear that once we despine the constructor's arguments into `(constructor, [arg0, .., argN])`, we can reduce the projection by simply taking the argument at position `i + num_params`, where `num_params` is what it sounds like, the number of parameters for the structure type.
+-->
 
 これを念頭に置けば、コンストラクタの引数を `(constructor, [arg0, .., argN])` へと手直しすれば、射影の簡約は単純に `i + num_params` の位置にある引数を取るだけであることが明白になるでしょう。ここで `num_params` はその名前の通りのもので、その構造体型のパラメータの数を表します。
 
@@ -123,39 +161,57 @@ reduce proj fieldIdx structure:
   -- args will be `[A, B, a, b]`
 ```
 
-<!-- ### Special case for projections: String literals -->
+<!--
+### Special case for projections: String literals
+-->
 
 ### 射影の特殊なケース：文字列リテラル
 
-<!-- The kernel extension for string literals introduces one special case in projection reduction, and one in iota reduction.  -->
+<!--
+The kernel extension for string literals introduces one special case in projection reduction, and one in iota reduction. 
+-->
 
 カーネルは文字列リテラルについて拡張を行っており、これによって射影の簡約で1つ、ι簡約で1つの特殊なケースが導入されます。
 
-<!-- Projection reduction for string literals: Because the projection expression's structure might reduce to a string literal (Lean's `String` type is defined as a structure with one field, which is a `List Char`) -->
+<!--
+Projection reduction for string literals: Because the projection expression's structure might reduce to a string literal (Lean's `String` type is defined as a structure with one field, which is a `List Char`)
+-->
 
 文字列リテラルに対する射影の簡約：なぜなら構造体の射影の式を簡約すると文字列リテラルになる可能性があるからです（Lean の `String` 型は `List Char` のフィールドを1つ持つ構造体として定義されています）。
 
-<!-- If the structure reduces as a `StringLit (s)`, we convert that to `String.mk (.. : List Char)` and proceed as usual for projection reduction. -->
+<!--
+If the structure reduces as a `StringLit (s)`, we convert that to `String.mk (.. : List Char)` and proceed as usual for projection reduction.
+-->
 
 もしその構造体が `StringLit (s)` に簡約される場合、これを `String.mk (.. : List Char)` に変換し、いつものように射影の簡約が処理されます。
 
-<!-- ## Nat literal reduction -->
+<!--
+## Nat literal reduction
+-->
 
 ## 整数リテラルの簡約
 
-<!-- The kernel extension for nat literals includes reduction of `Nat.succ` as well as the binary operations of addition, subtraction, multiplication, exponentiation, division, mod, boolean equality, and boolean less than or equal. -->
+<!--
+The kernel extension for nat literals includes reduction of `Nat.succ` as well as the binary operations of addition, subtraction, multiplication, exponentiation, division, mod, boolean equality, and boolean less than or equal.
+-->
 
 整数リテラル用のカーネル拡張には加算・減算・乗算・指数・除算・剰余・真偽値の同値・真偽値の以下の二項演算に加えて `Nat.succ` の簡約が含まれます。
 
-<!-- If the expression being reduced is `Const(Nat.succ, []) n` where `n` can be reduced to a nat literal `n'`, we reduce to `NatLit(n'+1)` -->
+<!--
+If the expression being reduced is `Const(Nat.succ, []) n` where `n` can be reduced to a nat literal `n'`, we reduce to `NatLit(n'+1)`
+-->
 
 簡約される式が `Const(Nat.succ, []) n` で `n` が整数リテラル `n` に簡約できる場合、`NatLit(n'+1)` に簡約されます。
 
-<!-- If the expression being reduced is `Const(Nat.<binop>, []) x y` where `x` and `y` can be reduced to nat literals `x'` and `y'`, we apply the native version of the appropriate `<binop>` to `x'` and `y'`, returning the resulting nat literal. -->
+<!--
+If the expression being reduced is `Const(Nat.<binop>, []) x y` where `x` and `y` can be reduced to nat literals `x'` and `y'`, we apply the native version of the appropriate `<binop>` to `x'` and `y'`, returning the resulting nat literal.
+-->
 
 もし式が `Const(Nat.<binop>, []) x y` へと簡約され `x` と `y` がそれぞれ整数リテラル `x'` と `y'` に簡約される場合、適切な `<binop>` のネイティブ版を `x'` と `y'` に適用し、結果の整数リテラルを返します。
 
-<!-- Examples: -->
+<!--
+Examples:
+-->
 
 例：
 ```
@@ -166,27 +222,39 @@ Const(Nat.add, []) NatLit(2) NatLit(3) ~> NatLit(2+3)
 Const(Nat.add, []) (Const Nat.succ [], NatLit(10)) NatLit(3) ~> NatLit(11+3)
 ```
 
-<!-- ## Iota reduction (pattern matching) -->
+<!--
+## Iota reduction (pattern matching)
+-->
 
 ## ι簡約（パターンマッチ）
 
-<!-- Iota reduction is about applying reduction strategies that are specific to, and derived from, a given inductive declaration. What we're talking about is application of an inductive declaration's recursor (or the special case of `Quot` which we'll see later). -->
+<!--
+Iota reduction is about applying reduction strategies that are specific to, and derived from, a given inductive declaration. What we're talking about is application of an inductive declaration's recursor (or the special case of `Quot` which we'll see later).
+-->
 
 ι簡約とは与えられた帰納的宣言に特有でかつそこから派生した簡約戦略を適用することです。これはまさに帰納的宣言の再帰子（または後で説明する `Quot` の特別な場合）の適用です。
 
-<!-- Each recursor has a set of "recursor rules", one recursor rule for each constructor. In contrast to the recursor, which presents as a type, these recursor rules are value level expressions showing how to eliminate an element of type `T` created with constructor `T.c`. For example, `Nat.rec` has a recursor rule for `Nat.zero`, and another for `Nat.succ`. -->
+<!--
+Each recursor has a set of "recursor rules", one recursor rule for each constructor. In contrast to the recursor, which presents as a type, these recursor rules are value level expressions showing how to eliminate an element of type `T` created with constructor `T.c`. For example, `Nat.rec` has a recursor rule for `Nat.zero`, and another for `Nat.succ`.
+-->
 
 各再帰子は「再帰子ルール」を持っており、各コンストラクタごとに1つの再帰子ルールがあります。型として表示される再帰子とは対照的に、これらの再帰子ルールはコンストラクタ `T.c` で作成された `T` 型の要素をどのように除去するかを示す値レベルの式です。例えば、`Nat.rec` は `Nat.zero` と `Nat.succ` それぞれに対する再帰子ルールを持ちます。
 
-<!-- For an inductive declaration `T`, one of the elements demanded by `T`'s recursor is an actual `(t : T)`, which is the thing we're eliminating. This `(t : T)` argument is known as the "major premise". Iota reduction performs pattern matching by taking apart the major premise to see what constructor was used to make `t`, then retrieving and applying the corresponding recursor rule from the environment. -->
+<!--
+For an inductive declaration `T`, one of the elements demanded by `T`'s recursor is an actual `(t : T)`, which is the thing we're eliminating. This `(t : T)` argument is known as the "major premise". Iota reduction performs pattern matching by taking apart the major premise to see what constructor was used to make `t`, then retrieving and applying the corresponding recursor rule from the environment.
+-->
 
 帰納的宣言 `T` に対して、`T` の再帰子が要求する要素の1つは実際の `(t : T)` であり、これは除去する対象です。この `(t : T)` 引数は「major premise」と呼ばれます。ι簡約は major premise を分解することで `t` の構築にあたってどのコンストラクタが使われたかを確認し、対応する再帰子ルールを環境から取得して適用することでパターンマッチを行います。
 
-<!-- Because the recursor's type signature also demands the parameters, motives, and minor premises required, we don't need to change the arguments to the recursor to perform reduction on e.g. `Nat.zero` as opposed to `Nat.succ`. -->
+<!--
+Because the recursor's type signature also demands the parameters, motives, and minor premises required, we don't need to change the arguments to the recursor to perform reduction on e.g. `Nat.zero` as opposed to `Nat.succ`.
+-->
 
 再帰子の型シグネチャは必要なパラメータ・motive・minor premiseも要求するため、例えば `Nat.succ` とは対照的に `Nat.zero` に対して簡約を実行するために再帰子の引数を変更する必要はありません。
 
-<!-- In practice, it's sometimes necessary to do some initial manipulation to expose the constructor used to create the major premise, since it may not be found as a direct application of a constructor. For example, a `NatLit(n)` expression will need to be transformed into either `Nat.zero`, or `App Const(Nat.succ, []) ..`. For structures, we may also perform structural eta expansion, transforming an element `(t : T)` into `T.mk t.1 .. t.N`, thereby exposing the application of the `mk` constructor, permitting iota reduction to proceed (if we can't figure out what constructor was used to create the major premise, reduction fails). -->
+<!--
+In practice, it's sometimes necessary to do some initial manipulation to expose the constructor used to create the major premise, since it may not be found as a direct application of a constructor. For example, a `NatLit(n)` expression will need to be transformed into either `Nat.zero`, or `App Const(Nat.succ, []) ..`. For structures, we may also perform structural eta expansion, transforming an element `(t : T)` into `T.mk t.1 .. t.N`, thereby exposing the application of the `mk` constructor, permitting iota reduction to proceed (if we can't figure out what constructor was used to create the major premise, reduction fails).
+-->
 
 実際には major premise を作成するために使用されたコンストラクタを公開するための初期化的な手動操作が必要になることがあります。というのもこのコンストラクタがコンストラクタを直接適用したものとして見つからないことがあるからです。例えば、`NatLit(n)` 式は `Nat.zero` か `App Const(Nat.succ, []) ..` のいずれかに変換する必要があります。構造体では、構造体のη展開を行う場合もあります。要素 `(t : T)` を `T.mk t.1 .. t.N` に変換することで、`mk` コンストラクタの適用が明らかになり、ι簡約を進めることができます（major premise を作成するために使用されたコンストラクタが分からない場合、簡約は失敗します）。
 
@@ -225,51 +293,75 @@ fun
 ```
 
 
-<!-- ### k-like reduction -->
+<!--
+### k-like reduction
+-->
 
 ### k-like 簡約
 
-<!-- For some inductive types, known as "subsingleton eliminators", we can proceed with iota reduction even when the major premise's constructor is not directly exposed, as long as we know its type. This may be the case when, for example, the major premise appears as a free variable. This is known as k-like reduction, and is permitted because all elements of a subsingleton eliminator are identical.  -->
+<!--
+For some inductive types, known as "subsingleton eliminators", we can proceed with iota reduction even when the major premise's constructor is not directly exposed, as long as we know its type. This may be the case when, for example, the major premise appears as a free variable. This is known as k-like reduction, and is permitted because all elements of a subsingleton eliminator are identical. 
+-->
 
 「subsingleton eliminator」として知られているいくつかの帰納型では、major premise のコンストラクタが直接公開されていなくても、その型が分かっている限りι簡約を進めることができます。これは例えば major premise が自由変数として現れるような場合です。これは k-like 簡約と呼ばれ、subsingleton eliminator のすべての要素が同一であるため許容されます。
 
-<!-- To be a subsingleton eliminator, an inductive declaration must be an inductive prop, must not be a mutual or nested inductive, must have exactly one constructor, and the sole constructor must take only the type's parameters as arguments (it cannot "hide" any information that isn't fully captured in its type signature). -->
+<!--
+To be a subsingleton eliminator, an inductive declaration must be an inductive prop, must not be a mutual or nested inductive, must have exactly one constructor, and the sole constructor must take only the type's parameters as arguments (it cannot "hide" any information that isn't fully captured in its type signature).
+-->
 
 subsingleton eliminator であるためには、帰納的宣言は帰納的な命題でなければならず、また相互帰納的対象や入れ子の帰納的対象であってはならず、コンストラクタはちょうど1つでなければならず、その唯一のコンストラクタは型のパラメータだけを引数として取らなければなりません（型シグネチャで完全に捕捉されていない情報を「隠す」ことはできません）。
 
-<!-- For example, the value of any element of the type `Eq Char 'x'` is fully determined just by its type, because all elements of this type are identical. -->
+<!--
+For example, the value of any element of the type `Eq Char 'x'` is fully determined just by its type, because all elements of this type are identical.
+-->
 
 例えば、`Eq Char 'x'` 型の要素の値はこの型のすべての要素は同一であるため、その型だけで完全に決定されます。
 
-<!-- If iota reduction finds a major premise which is a subsingleton eliminator, it is permissible to substitute the major premise for an application of the type's constructor, because that is the only element the free variable could actually be. For example, a major premise which is a free variable of type `Eq Char 'a'` may be substituted for an explicitly constructed `Eq.refl Char 'a'`. -->
+<!--
+If iota reduction finds a major premise which is a subsingleton eliminator, it is permissible to substitute the major premise for an application of the type's constructor, because that is the only element the free variable could actually be. For example, a major premise which is a free variable of type `Eq Char 'a'` may be substituted for an explicitly constructed `Eq.refl Char 'a'`.
+-->
 
 ι簡約によって subsingleton eliminator である major premise が見つかった場合、その major premise を型コンストラクタの適用に置換することが許容されます。なぜならその自由変数としてあり得るのがこの型コンストラクタだけだからです。例えば、`Eq Char 'a'` 型の自由変数である major premise は明示的に構成された `Eq.refl Char 'a'` に置換することができます。
 
-<!-- Getting to the nuts and bolts, if we neglected to look for and apply k-like reduction, free variables that are subsingleton eliminators would fail to identify the corresponding recursor rule, iota reduction would fail, and certain conversions expected to succeed would no longer succeed. -->
+<!--
+Getting to the nuts and bolts, if we neglected to look for and apply k-like reduction, free variables that are subsingleton eliminators would fail to identify the corresponding recursor rule, iota reduction would fail, and certain conversions expected to succeed would no longer succeed.
+-->
 
 根本的な話として、もし k-like 簡約を探索して適用することを怠れば、subsingleton eliminator である自由変数は対応する再帰規則を特定できず、ι簡約は失敗し、成功すると期待されたある種の変換は成功しなくなるでしょう。
 
-<!-- ### `Quot` reduction; `Quot.ind` and `Quot.lift` -->
+<!--
+### `Quot` reduction; `Quot.ind` and `Quot.lift`
+-->
 
 ### `Quot` の簡約；`Quot.ind` と `Quot.lift`
 
-<!-- `Quot` introduces two special cases which need to be handled by the kernel, one for `Quot.ind`, and one for `Quot.lift`. -->
+<!--
+`Quot` introduces two special cases which need to be handled by the kernel, one for `Quot.ind`, and one for `Quot.lift`.
+-->
 
 `Quot` はカーネルでハンドルするべき2つの特殊なケースを導入します。1つは `Quot.ind` で、もう一つは `Quot.lift` の場合です。
 
-<!-- Both `Quot.ind` and `Quot.lift` deal with application of a function `f` to an argument `(a : α)`, where the `a` is a component of some `Quot r`, formed with `Quot.mk .. a`.  -->
+<!--
+Both `Quot.ind` and `Quot.lift` deal with application of a function `f` to an argument `(a : α)`, where the `a` is a component of some `Quot r`, formed with `Quot.mk .. a`. 
+-->
 
 `Quot.ind` と `Quot.lift` はどちらも関数 `f` の引数 `(a : α)` への適用に対応しており、ここで `a` は `Quot r` の構成要素であり、`Quot.mk .. a` によって形成されます。
 
-<!-- To execute the reduction, we need to pull out the argument that is the `f` element and the argument that is the `Quot` where we can find `(a : α)`, then apply the function `f` to `a`. Finally, we reapply any arguments that were part of some outer expression not related to the invocation of `Quot.ind` or `Quot.lift`. -->
+<!--
+To execute the reduction, we need to pull out the argument that is the `f` element and the argument that is the `Quot` where we can find `(a : α)`, then apply the function `f` to `a`. Finally, we reapply any arguments that were part of some outer expression not related to the invocation of `Quot.ind` or `Quot.lift`.
+-->
 
 この簡約を実行するには、`f` の要素である引数と、`(a : α)` が見つかる `Quot` 要素である引数を取り出し、`a` に関数 `f` を適用する必要があります。最後に、`Quot.ind` や `Quot.lift` の呼び出しとは関係のない外部式の一部であった引数を再適用します。
 
-<!-- Since this is only a reduction step, we rely on the type checking phases done elsewhere to provide assurances that the expression as a whole is well typed. -->
+<!--
+Since this is only a reduction step, we rely on the type checking phases done elsewhere to provide assurances that the expression as a whole is well typed.
+-->
 
 これは簡約のステップにすぎないため、式全体が適切に型付けされていることを保証するために他の場所で行われる型チェックの段階に頼ります。
 
-<!-- The type signatures for `Quot.ind` and `Quot.mk` are recreated below, mapping the elements of the telescope to what we should find as the arguments. The elements with a `*` are the ones we're interested in for reduction. -->
+<!--
+The type signatures for `Quot.ind` and `Quot.mk` are recreated below, mapping the elements of the telescope to what we should find as the arguments. The elements with a `*` are the ones we're interested in for reduction.
+-->
 
 以下に `Quot.ind` と `Quot.mk` の型シグネチャを再作成し、テレスコープの要素を引数として見つけるべきものにマッピングしています。`*` が付いている要素は簡約のために必要なものです。
 
diff --git a/src/type_checking/type_inference.md b/src/type_checking/type_inference.md
index d29f175..eecedb9 100644
--- a/src/type_checking/type_inference.md
+++ b/src/type_checking/type_inference.md
@@ -32,7 +32,7 @@ We will also look at a number of additional correctness assertions that Lean's k
 If you're following Lean's implementation and using the locally nameless approach, you should not run into bound variables during type inference, because all open binders will be instantiated with the appropriate free variables.
 -->
 
-Lean の実装に従ってローカルに名前を持たないアプローチを使う場合、型推論中で束縛変数に遭遇することはないでしょう。というのもすべての開いた束縛子は適切な自由変数でインスタンス化されているからです。
+Lean の実装に従って locally nameless なアプローチを使う場合、型推論中で束縛変数に遭遇することはないでしょう。というのもすべての開いた束縛子は適切な自由変数でインスタンス化されているからです。
 
 <!--
 When we come across a binder, we need to traverse into the body to determine the body's type. There are two main approaches one can take to preserve the information about the binder type; the one used by Lean proper is to create a free variable that retains the binder's type information, replace the corresponding bound variables with the free variable using instantiation, and then enter the body. This is nice, because we don't have to keep track of a separate piece of state for a typing context.