diff --git a/book.toml b/book.toml
index bc91183..7e17ede 100644
--- a/book.toml
+++ b/book.toml
@@ -7,6 +7,7 @@ title = "Mathematics in type theory 日本語訳"
 
 [output.html]
 git-repository-url = "https://github.com/lean-ja/math-in-type-theory-ja"
+mathjax-support = true
 
 # 日本語検索に対応していないため，無効にする
 [output.html.search]
diff --git a/src/c1_introduction.md b/src/c1_introduction.md
index a2c078a..f74d539 100644
--- a/src/c1_introduction.md
+++ b/src/c1_introduction.md
@@ -6,7 +6,7 @@
 
 <!-- **Definitions** (for example the real numbers, or $\pi$) and **true/false statements** (for example the statement of Fermat’s Last Theorem or the statement of the Riemann Hypothesis) are part of the science of mathematics: these are black and white things which have a completely rigorous meaning within some foundational system. -->
 
-**定義** (たとえば実数や $\pi$) や**命題** (たとえばフェルマーの最終定理やリーマン仮説のステートメント) は数学の科学の一部です：こういったものは，ある基礎的なシステムの中で完全に厳密な意味を持ち，白黒はっきりしています．
+**定義** (たとえば実数や π) や**命題** (たとえばフェルマーの最終定理やリーマン仮説のステートメント) は数学の科学の一部です：こういったものは，ある基礎的なシステムの中で完全に厳密な意味を持ち，白黒はっきりしています．
 
 <!-- **Proofs** are in some sense the currency of mathematics: proofs win prizes. Constructing them is an art, checking them is a science. This explains, very simply, why computer proof verification systems such as Lean, Coq, Isabelle/HOL, Agda… are much better at checking proofs than constructing them. -->
 
@@ -27,4 +27,4 @@
 
 <!-- The first one is a precise “scientific” question. A group is a set equipped with some extra structure, and which satisfies some axioms. The formal answer is on [Wikipedia’s page on groups](https://en.wikipedia.org/wiki/Group_(mathematics)#Definition). A group is a definition. But the second question is a different kind of question. Different people think about groups in different ways. Say $G$ is a group generated by an element x satisfying $x^5=x^8=1$. What can you say about $G$? If you are a mathematics undergraduate who has just seen the formal definition of a group, you can probably say nothing. If you have a more mature understanding of group theory, you instantly know that this group is trivial, because you have a far more sophisticated model of what is going on. Ideas are complicated, and human-dependent. A computer’s idea of what a group is, is literally a copy of the definition in Wikipedia, and this is one of the reasons that computers are currently bad at proving new theorems by themselves. You can develop a computer’s intuition by teaching it theorems about groups, or teaching it examples of groups, or trying to write AI’s which figure out group theory theorems or examples of groups automatically. But intuition is a very subtle thing, and I do not understand it at all well, so I will say no more about these ideas here. I think that the concept of a map being “canonical” is an idea rather than a definition — I think different mathematicians have different ways of thinking about this weasel word. In this post I’m going to talk about how the three other concepts are implemented in type theory, in the Lean theorem prover. -->
 
-最初のものは正確な「科学的な」質問です．群とは，ある特別な構造を持ち，ある公理を満たす集合のことです．正式な答えは [Wikipediaの群についてのページ](https://en.wikipedia.org/wiki/Group_(mathematics)#Definition)にあります．群とは定義です．しかし，２つめの質問は種類の異なる質問です．群について考える方法は人によって異なります．$G$ が $x^5=x^8=1$ を満たす要素 $x$ によって生成される群だとします．$G$ について何が言えるでしょうか？もしあなたが数学の学部生で，群の形式的な定義を見たばかりなら，おそらく何も言えないでしょう．群論をより深く理解している人なら，即座にこの群が自明であることがわかるでしょう．何が起こっているのかについて，はるかに洗練されたモデルを有しているからです．アイデアは複雑で，人によって異なるものです．「群とは何であるか」という問いについてのコンピュータの理解は，文字通りウィキペディアの定義のコピーです．現在コンピュータは新しい定理を自力で証明することを苦手としていますが，その理由のひとつがこれです．コンピュータに群に関する定理を教えたり，群の例を教えたり，群論の定理や群の例を自動的に理解する AI を作ったりすることで，コンピュータの直感を発達させることができます．しかし直感というのはとても微妙なもので，私にはまったく理解できないので，ここではこういったアイデアについてはこれ以上語らないことにします．写像が canonical (正準) であるという概念は，定義というよりむしろアイデアだと思います．数学者によって，このイタチごっこのような言葉に対する考え方は違ってくるでしょう．この記事では，他の３つの概念 (定義，命題，証明) が型理論や Lean theorem proverでどのように実装されているかについてお話しようと思います．
+最初のものは正確な「科学的な」質問です．群とは，ある特別な構造を持ち，ある公理を満たす集合のことです．正式な答えは [Wikipediaの群についてのページ](https://en.wikipedia.org/wiki/Group_(mathematics)#Definition)にあります．群とは定義です．しかし，２つめの質問は種類の異なる質問です．群について考える方法は人によって異なります．\\(G\\) が \\(x^5=x^8=1\\) を満たす要素 \\(x\\) によって生成される群だとします．\\(G\\) について何が言えるでしょうか？もしあなたが数学の学部生で，群の形式的な定義を見たばかりなら，おそらく何も言えないでしょう．群論をより深く理解している人なら，即座にこの群が自明であることがわかるでしょう．何が起こっているのかについて，はるかに洗練されたモデルを有しているからです．アイデアは複雑で，人によって異なるものです．「群とは何であるか」という問いについてのコンピュータの理解は，文字通りウィキペディアの定義のコピーです．現在コンピュータは新しい定理を自力で証明することを苦手としていますが，その理由のひとつがこれです．コンピュータに群に関する定理を教えたり，群の例を教えたり，群論の定理や群の例を自動的に理解する AI を作ったりすることで，コンピュータの直感を発達させることができます．しかし直感というのはとても微妙なもので，私にはまったく理解できないので，ここではこういったアイデアについてはこれ以上語らないことにします．写像が canonical (正準) であるという概念は，定義というよりむしろアイデアだと思います．数学者によって，このイタチごっこのような言葉に対する考え方は違ってくるでしょう．この記事では，他の３つの概念 (定義，命題，証明) が型理論や Lean theorem proverでどのように実装されているかについてお話しようと思います．
diff --git a/src/c2_definitions_statements_proofs.md b/src/c2_definitions_statements_proofs.md
index a7f7e82..b5a3377 100644
--- a/src/c2_definitions_statements_proofs.md
+++ b/src/c2_definitions_statements_proofs.md
@@ -7,7 +7,7 @@
 
 <!-- I am certainly not qualified to explain how all this works in category theory. In set theory, let me just make one observation. A definition in set theory, for example the definition of the real numbers, or $\pi$, is a set. And a proof is a sequence of steps in *logic*. A definition and a proof seem to me to be two completely different things in set theory. A group is a mixture of these things — a group is an ordered quadruple $(G,m,i,e)$ satisfying some axioms, so it’s a set with some logic attached. -->
 
-私には，圏論でどのように数学の基礎付けを行うのかを説明する資格はありません．集合論について，ひとつだけ観察してみましょう．集合論における定義，たとえば実数や $\pi$ の定義は集合です．そして証明とは，論理のステップをつなげたものです．集合論において，定義と証明は全く異なるもののように私には思えます．群とは，定義と証明の混合物です．―― 群とは，順序付き4つ組 $(G,m,i,e)$ であって，特定の公理を満たすもののことです．つまり，論理が付属した集合です．
+私には，圏論でどのように数学の基礎付けを行うのかを説明する資格はありません．集合論について，ひとつだけ観察してみましょう．集合論における定義，たとえば実数や π の定義は集合です．そして証明とは，論理のステップをつなげたものです．集合論において，定義と証明は全く異なるもののように私には思えます．群とは，定義と証明の混合物です．―― 群とは，順序付き4つ組 \\((G,m,i,e)\\) であって，特定の公理を満たすもののことです．つまり，論理が付属した集合です．
 
 <!-- In type theory however, things are surprisingly different. All three things — definitions, true/false statements, and proofs — are *all the same kind of thing*! They are all **terms**. A group, a proof, the real numbers — they are all terms. This unification of definitions and proofs — of sets and logic — are what seems to make type theory a practical foundational system for teaching all undergraduate level mathematics to computers. -->
 
diff --git a/src/c3_universes_types_terms.md b/src/c3_universes_types_terms.md
index 16fd1a0..ba1ff0d 100644
--- a/src/c3_universes_types_terms.md
+++ b/src/c3_universes_types_terms.md
@@ -3,12 +3,11 @@
 
 <!-- In type theory, everything is a term. But some terms are types. Not every term is a type, but every term has a type. A colon is used to express the type of a term in Lean — the notation `x : T` means that `x` is a term of type `T`. For example, the real number $\pi$ (pi) is a term in Lean, and the real numbers ℝ is a type, and we have $\pi$ : ℝ , that is, $\pi$ is a term of type ℝ. In set theory one writes $\pi\in\mathbb{R}$ , in type theory we write $\pi$ : ℝ. They both express the same mathematical concept, namely “$\pi$ is a real number”. -->
 
-型理論では，すべてが項です．そしていくつかの項は型でもあります．すべての項が型であるわけではありませんが，すべての項は型を持っています．Lean では，コロンを使って項の型を表します．―― `x : T` という表記で，`x` が `T` という型の項であることを表します．たとえば，実数 $\pi$ は Lean の項であり，実数全体 $\mathbb{R}$ は型であり，`π : ℝ` が成り立ちます．つまり，$\pi$ は型 $\mathbb{R}$ の項です．集合論では $\pi\in\mathbb{R}$ と書きますが，型理論では `π : ℝ` と書きます．どちらも同じ数学的概念，つまり「$\pi$ は実数である」を表します．
+型理論では，すべてが項です．そしていくつかの項は型でもあります．すべての項が型であるわけではありませんが，すべての項は型を持っています．Lean では，コロンを使って項の型を表します．―― `x : T` という表記で，`x` が `T` という型の項であることを表します．たとえば，実数 π は Lean の項であり，実数全体 ℝ は型であり，`π : ℝ` が成り立ちます．つまり，π は型 ℝ の項です．集合論では π ∈ ℝ と書きますが，型理論では `π : ℝ` と書きます．どちらも同じ数学的概念，つまり「π は実数である」を表します．
 
 <!-- Now $\pi$ is a term but it’s not a type. In Lean, `x : π` makes no sense. In set theory, $x\in\pi$ does happen to make sense, but this is a weird coincidence because everything is a set. Furthermore, the actual elements of $\pi$ will depend on how the real numbers are implemented (as Dedekind cuts or Cauchy sequences, for example), and hence in set theory $x\in\pi$, whilst being syntactically valid in theory, has no mathematical meaning; it happens to make sense, but this is a quirk of the system. If you’re adamant that $x\in\pi$ should make sense then I say you’ve been brainwashed by set theory. Gauss and Euler will put you right: they were proving theorems about the real numbers before Cauchy and Dedekind came along with their sequences and cuts. There is no reason that $\pi$ needs to have elements, this is a quirk of the set-theoretic foundations of mathematics, and this quirk is eliminated in a type theoretic foundation. -->
 
-いま $\pi$ は項ですが，型ではありません. Lean では `x : π` は意味を持ちません．集合論では，$x\in\pi$ は意味を持ちますが，これは集合論において全てが集合であることに起因する，奇妙な偶然です．さらに，$\pi$ の実際の要素は，実数がどのように実装されるか（たとえばデデキント切断としてか，コーシー数列としてか）に依存するため，集合論での $x\in\pi$ は，構文的には意味を持つものの，数学的な意味はありません．たまたま意味をなすだけで，システムの癖に過ぎません．もし「 $x \in \pi$ には意味があるはずだ」
-とあなたが断固として言うなら，「あなたは集合論に洗脳されているのだ」と私は言うでしょう．ガウスとオイラーがあなたを正しい方向に導いてくれるでしょう：ガウスとオイラーは，コーシーとデデキントが数列と切断を導入する以前に，実数に関する定理を証明していました．$\pi$ が要素を持つべき理由はありません．これは数学の基礎に集合論を使った際の癖であり，その癖は型理論を使った場合には解消されます．
+いま π は項ですが，型ではありません. Lean では `x : π` は意味を持ちません．集合論では，x ∈ π は意味を持ちますが，これは集合論において全てが集合であることに起因する，奇妙な偶然です．さらに，π の実際の要素は，実数がどのように実装されるか（たとえばデデキント切断としてか，コーシー数列としてか）に依存するため，集合論での x ∈ π は，構文的には意味を持つものの，数学的な意味はありません．たまたま意味をなすだけで，システムの癖に過ぎません．もし「 x ∈ π には意味があるはずだ」とあなたが断固として言うなら，「あなたは集合論に洗脳されているのだ」と私は言うでしょう．ガウスとオイラーがあなたを正しい方向に導いてくれるでしょう：ガウスとオイラーは，コーシーとデデキントが数列と切断を導入する以前に，実数に関する定理を証明していました．π が要素を持つべき理由はありません．これは数学の基礎に集合論を使った際の癖であり，その癖は型理論を使った場合には解消されます．
 
 <!-- I claimed above that every term has a type. So what is the type of ℝ? It turns out that `ℝ : Type`. The real numbers are a term of a “universe” type called `Type` — the type theory analogue of the class of all sets. -->
 
@@ -16,7 +15,7 @@
 
 <!-- Many of the mathematical objects which mathematicians think of as definitions either have type `Type`, or have type `T` where `T : Type`. As a vague rule of thumb, the stuff which has elements (groups, rings, fields etc) has type `Type`, and the stuff which doesn’t have elements ($\pi$, $\sqrt{2}$ or an element $g$ of a general group) has type `T` where T is some type. As another vague rule of thumb, things we write using capital letters (a group, a ring,…) or fancy letters (the reals, the rationals) tend to have type `Type`, and things we write using small letters (an element g of a group, a real number r or an integer n) tend to have type `T` where T is what we think of as the set which contains these things. For example `2 : ℕ` and `ℕ : Type`, or if $g$ is an element of the group $G$ then in Lean we have `g : G` and `G : Type`. You can see that there is a three-layer hiearchy here — terms at the bottom, types above them, and the universe at the top. -->
 
-数学者が定義する数学的対象の多くは，型 `Type` を持つか，あるいは `T : Type` であるような型 `T` を持ちます．漠然とした経験則ですが，要素を持つもの（群，環，体など）は `Type` 型を持ち，要素を持たないもの（$\pi$, $\sqrt{2}$ や一般の群の要素 $g$）は `T` 型を持ちます．もう一つのあいまいな経験則として，大文字で書くもの（群や環など）や fancy letter（実数 ℝ や有理数 ℚ ）で書くものは `Type` 型を持ち，小文字で書くもの（群の要素 $g$ や実数 $r$, 整数 $n$）は `T` 型を持つ傾向にあります．たとえば `2 : ℕ` と `ℕ : Type` が成り立ちます．また $g$ が群 $G$ の要素であるとき，Lean では `g : G` と `G : Type` が成り立ちます．ここには３層の階層があります ―― 一番下に項があり，その上に型があり，最上部に宇宙があります．
+数学者が定義する数学的対象の多くは，型 `Type` を持つか，あるいは `T : Type` であるような型 `T` を持ちます．漠然とした経験則ですが，要素を持つもの（群，環，体など）は `Type` 型を持ち，要素を持たないもの（π, \\(\sqrt{2}\\) や一般の群の要素 \\(g\\)）は `T` 型を持ちます．もう一つのあいまいな経験則として，大文字で書くもの（群や環など）や fancy letter（実数 ℝ や有理数 ℚ ）で書くものは `Type` 型を持ち，小文字で書くもの（群の要素 \\(g\\) や実数 \\(r\\), 整数 \\(n\\)）は `T` 型を持つ傾向にあります．たとえば `2 : ℕ` と `ℕ : Type` が成り立ちます．また \\(g\\) が群 \\(g\\) の要素であるとき，Lean では `g : G` と `G : Type` が成り立ちます．ここには３層の階層があります ―― 一番下に項があり，その上に型があり，最上部に宇宙があります．
 
 <!-- * Universe : `Type` -->
 * 宇宙 : `Type`
@@ -31,7 +30,7 @@
 
 <!-- There is a standard use of the colon in mathematics — it’s in the notation for functions. If X and Y are sets (if you’re doing set theory) or types (if you’re doing type theory), then the notation for a function from `X` to `Y` is `f : X → Y`. This is actually consistent with Lean’s usage of the colon; Lean’s notation for the collection $\mathrm{Hom}(X,Y)$ of functions from `X` to `Y` is `X → Y` , which is a type (i.e. `X → Y : Type`, corresponding to the fact that set theorists think of $\mathrm{Hom}(X,Y)$ as a set), and `f : X → Y` means that `f` is a term of type `X → Y`, the type-theoretic version of $f \in \mathrm{Hom}(X,Y)$, and the way to say that `f` is a function from `X` to `Y` in type theory. -->
 
-数学におけるコロンの標準的な使い方があります．―― 関数を書くための記法です．`X` と `Y` が集合（集合論を使っている場合）または型（型理論を使っている場合）であるとき，`X` から `Y` への関数を `f : X → Y` と書きます．これは実は Lean におけるコロンの使い方と一致しています．`X` から `Y` への関数の集まり $\mathrm{Hom}(X,Y)$ に対する Lean の表記法は `X → Y` であり，これは型です．（つまり `X → Y : Type` です．これは集合論で $\mathrm{Hom}(X,Y)$ を集合と考えることに対応しています）`f : X → Y` は `f` が `X → Y` 型の項であることを意味し．集合論でいう $f \in \mathrm{Hom}(X,Y)$ に対応します．これは型理論において，`f` が `X` から `Y` への関数であることを書き表すやり方です．
+数学におけるコロンの標準的な使い方があります．―― 関数を書くための記法です．`X` と `Y` が集合（集合論を使っている場合）または型（型理論を使っている場合）であるとき，`X` から `Y` への関数を `f : X → Y` と書きます．これは実は Lean におけるコロンの使い方と一致しています．`X` から `Y` への関数の集まり \\(\mathrm{Hom}(X,Y)\\) に対する Lean の表記法は `X → Y` であり，これは型です．（つまり `X → Y : Type` です．これは集合論で \\(\mathrm{Hom}(X,Y)\\) を集合と考えることに対応しています）`f : X → Y` は `f` が `X → Y` 型の項であることを意味し．集合論でいう \\(f \in \mathrm{Hom}(X,Y)\\) に対応します．これは型理論において，`f` が `X` から `Y` への関数であることを書き表すやり方です．
 
 <!-- (Not for exam) Strictly speaking, universes are types, and types are terms, but this is a linguistic issue: often when people speak of types, they mean types which are not universes, and when people speak of terms they mean terms which are not types. But not always. This confused me when I was a beginner. -->
 
diff --git a/src/c4_theorems_proofs.md b/src/c4_theorems_proofs.md
index 5a3e9f1..49273bf 100644
--- a/src/c4_theorems_proofs.md
+++ b/src/c4_theorems_proofs.md
@@ -11,11 +11,11 @@
 
 <!-- This will all be clearer with examples. 2 + 2 = 4 is a Proposition, so we can write `2 + 2 = 4 : Prop`. But 2 + 2 = 5 is also a Proposition, so `2 + 2 = 5 : Prop` as well. I’ll say it again — Propositions do not have to be true! Propositions are true/false statements. Let’s see some more complex examples. -->
 
-例を見るとわかりやすいでしょう．$2 + 2 = 4$ は命題なので `2 + 2 = 4 : Prop` と書くことができます．しかし，$2 + 2 = 5$ も命題なので，`2 + 2 = 5 : Prop` と書くこともできます．何度も言いますが，命題が真である必要はありません！命題は真か偽かどちらかになる文のことです．もう少し複雑な例を見てみましょう．
+例を見るとわかりやすいでしょう．\\(2 + 2 = 4\\) は命題なので `2 + 2 = 4 : Prop` と書くことができます．しかし，\\(2 + 2 = 5\\) も命題なので，`2 + 2 = 5 : Prop` と書くこともできます．何度も言いますが，命題が真である必要はありません！命題は真か偽かどちらかになる文のことです．もう少し複雑な例を見てみましょう．
 
 <!-- The true/false statement that x+0=x for all natural numbers x is a Proposition: in Lean this can be expressed as `(∀ x : ℕ, x + 0 = x) : Prop` . A Proposition is a term of type `Prop` (just like the types we saw earlier were terms of type `Type`). Let RH denote the statement of the Riemann Hypothesis. Then `RH : Prop`. We don’t care if it’s true, false, independent of the axioms of mathematics, undecidable, whatever. A Proposition is a true/false statement. Let’s look at the part of Lean’s type theory hierarchy which lives in the `Prop` universe. -->
 
-「すべての自然数 $x$ について $x + 0 = x$ である」という文は命題です．Lean では，これは `(∀ x : ℕ, x + 0 = x) : Prop` と表せます．命題は `Prop` 型を持つ項です．（先ほど見てきた項が型 `Type` を持っていたのと同様です）RH をリーマン仮説のステートメントとします．すると `RH : Prop` となります．それが真か偽か，特定の数学の公理と独立であるか，決定不能であるか，等は問いません．命題とは真か偽かどちらかになる文のことです．Lean の型理論の階層のうち，`Prop` 宇宙に住む部分を見てみましょう．
+「すべての自然数 \\(x\\) について \\(x + 0 = x\\) である」という文は命題です．Lean では，これは `(∀ x : ℕ, x + 0 = x) : Prop` と表せます．命題は `Prop` 型を持つ項です．（先ほど見てきた項が型 `Type` を持っていたのと同様です）RH をリーマン仮説のステートメントとします．すると `RH : Prop` となります．それが真か偽か，特定の数学の公理と独立であるか，決定不能であるか，等は問いません．命題とは真か偽かどちらかになる文のことです．Lean の型理論の階層のうち，`Prop` 宇宙に住む部分を見てみましょう．
 
 <!-- * Universe: `Prop` -->
 * 宇宙 : `Prop`
diff --git a/src/c5_prop_type_proof_term.md b/src/c5_prop_type_proof_term.md
index 4369ea9..7018495 100644
--- a/src/c5_prop_type_proof_term.md
+++ b/src/c5_prop_type_proof_term.md
@@ -7,7 +7,7 @@
 
 <!-- In the [natural number game](http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/), I use this abuse of notation because I am trying to communicate to mathematicians. The statement `∀ x : ℕ, x + 0 = x` is a true statement, and I say things like “this is called `add_zero` in Lean”. In the natural number game I write statements such as `add_zero : ∀ x : ℕ, x + 0 = x`. But what this means is that the term called `add_zero` in Lean is a proof of `∀ x : ℕ, x + 0 = x`! The colon is being used in the type theory way. I am intentionally vague about this concept in the natural number game. I let mathematicians believe that `add_zero` is somehow equal to the “idea” that $x+0=x$ for all $x$. But what is going on under the hood is that `∀ x : ℕ, x + 0 = x` is a Proposition, which is a type, and `add_zero` is its proof, which is a term. Making a clear distinction between the statement of a theorem, and its proof, is important here. The statements are the types, the proofs are the terms. -->
 
-[natural number game (自然数ゲーム)](http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/) [^1]の中で，私は数学者を相手にしていたのでこのような表記の濫用を行っていました．`∀ x : ℕ, x + 0 = x` という文は真であり，「これは Lean では `add_zero` と呼ばれる」と私は言っていました．natural number game において，私は `add_zero : ∀ x : ℕ, x + 0 = x` と書いていました．しかし，これが何を意味するかといえば，Lean で `add_zero` と呼ばれる項が `∀ x : ℕ, x + 0 = x` の証明である，ということなのです！コロンは型理論的に使われています．私は natural number game では意図的にこの概念を曖昧にしました．`add_zero` はすべての $x$ に対して $x + 0 = x$ であるという「アイデア」と何らかの形で等しいと，数学者に信じさせたわけです．しかし裏では `∀ x : ℕ, x + 0 = x` は命題であり，型でもあり，`add_zero` はその証明であり，項でもあります．ここで重要なのは，定理のステートメントとその証明を区別することです．ステートメントは型であり，証明は項です．
+[natural number game (自然数ゲーム)](http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/) [^1]の中で，私は数学者を相手にしていたのでこのような表記の濫用を行っていました．`∀ x : ℕ, x + 0 = x` という文は真であり，「これは Lean では `add_zero` と呼ばれる」と私は言っていました．natural number game において，私は `add_zero : ∀ x : ℕ, x + 0 = x` と書いていました．しかし，これが何を意味するかといえば，Lean で `add_zero` と呼ばれる項が `∀ x : ℕ, x + 0 = x` の証明である，ということなのです！コロンは型理論的に使われています．私は natural number game では意図的にこの概念を曖昧にしました．`add_zero` はすべての \\(x\\) に対して \\(x + 0 = x\\) であるという「アイデア」と何らかの形で等しいと，数学者に信じさせたわけです．しかし裏では `∀ x : ℕ, x + 0 = x` は命題であり，型でもあり，`add_zero` はその証明であり，項でもあります．ここで重要なのは，定理のステートメントとその証明を区別することです．ステートメントは型であり，証明は項です．
 
 <!-- * Universe: `Prop` -->
 * 宇宙 : `Prop`
diff --git a/src/c6_elements_theorem.md b/src/c6_elements_theorem.md
index 211e232..1e552c5 100644
--- a/src/c6_elements_theorem.md
+++ b/src/c6_elements_theorem.md
@@ -3,12 +3,12 @@
 
 <!-- So our mental model of the statement `π : ℝ` is that `ℝ`, the type, is “a collection of stuff”, and `π`, the term, is a member of that collection. If we continue with this analogy, it says that the statement `2 + 2 = 4` is some kind of collection, and a proof of `2 + 2 = 4` is a member of that collection. In other words, Lean is suggesting that we model the true/false statement `2 + 2 = 4` as being some sort of a set, and a proof of `2 + 2 = 4` is an element of that set. Now in Lean, it is an inbuilt axiom that all proofs of a proposition are equal. So if `a : 2 + 2 = 4` and `b : 2 + 2 = 4` then `a = b`. This is because we’re working in the `Prop` universe — this is how Propositions behave in Lean. In the `Type` universe the analogue is not remotely true — we have `π : ℝ` and `37 : ℝ` and certainly $\pi\not=37$. This special quirk of the `Prop` universe is called “proof irrelevance”. Formally we could say that if `P : Prop`, if `a : P` and if `b : P` then `a = b`. Of course if a Proposition is false, then it has no proofs at all! It’s like the empty set. So Lean’s model of Propositions is that the true ones are like sets with $1$ element, and the false ones are like sets with $0$ elements. -->
 
-つまり `π : ℝ` というステートメントに対する私たちのメンタルモデルは，型である `ℝ` は「ものの集まり」であり，項である `π` はその集まりのメンバーである，ということです．このアナロジーを続けるなら，`2 + 2 = 4` というステートメントはある種の集まりであり，`2 + 2 = 4` の証明はそのメンバーです．言い換えれば，Lean は `2 + 2 = 4` をある種の集合であるとし，`2 + 2 = 4` の証明はその集合の要素であるとするようなモデルを提案しているのです．Lean では，ある命題の証明はすべて等しいという公理が組み込まれています．つまり `a : 2 + 2 = 4` かつ `b : 2 + 2 = 4` ならば `a = b` となります．これは `Prop` 宇宙の中だから起こることです ―― これが Lean における命題の振る舞いです．`Type` 宇宙の中ではこのようなことはありえません．―― `π : ℝ` かつ `37 : ℝ` ですが，$\pi\not=37$ です．この `Prop` 宇宙の特別な癖は「proof irrelevance (証明無関係)」と呼ばれます．形式的には，`P : Prop` に対して `a : P` かつ `b : P` ならば `a = b` である，と言い表せます．もちろん，ある命題が偽ならば，その命題には証明は全くありません！偽の命題は空集合のようなものです．つまり，Lean の命題のモデルは，真の命題は１つの要素を持つ集合のようなもので，偽の命題は $0$ 個の要素を持つ集合のようなものだと言っています．
+つまり `π : ℝ` というステートメントに対する私たちのメンタルモデルは，型である `ℝ` は「ものの集まり」であり，項である `π` はその集まりのメンバーである，ということです．このアナロジーを続けるなら，`2 + 2 = 4` というステートメントはある種の集まりであり，`2 + 2 = 4` の証明はそのメンバーです．言い換えれば，Lean は `2 + 2 = 4` をある種の集合であるとし，`2 + 2 = 4` の証明はその集合の要素であるとするようなモデルを提案しているのです．Lean では，ある命題の証明はすべて等しいという公理が組み込まれています．つまり `a : 2 + 2 = 4` かつ `b : 2 + 2 = 4` ならば `a = b` となります．これは `Prop` 宇宙の中だから起こることです ―― これが Lean における命題の振る舞いです．`Type` 宇宙の中ではこのようなことはありえません．―― `π : ℝ` かつ `37 : ℝ` ですが，π ≠ 37 です．この `Prop` 宇宙の特別な癖は「proof irrelevance (証明無関係)」と呼ばれます．形式的には，`P : Prop` に対して `a : P` かつ `b : P` ならば `a = b` である，と言い表せます．もちろん，ある命題が偽ならば，その命題には証明は全くありません！偽の命題は空集合のようなものです．つまり，Lean の命題のモデルは，真の命題は１つの要素を持つ集合のようなもので，偽の命題は 0 個の要素を持つ集合のようなものだと言っています．
 
 <!-- Recall that if `f : X → Y` then this means that `f` is a function from `X` to `Y`. Now say $P$ and $Q$ are Propositions, and let’s say that we know $P\implies Q$. What does this mean? It means that $P$ implies $Q$. It means that if $P$ is true, then $Q$ is true. It means that if we have a proof of $P$, we can make a proof of $Q$. It is a function from the proofs of $P$ to the proofs of $Q$. It is a function sending an element of $P$ to an element of $Q$. It is a term of type `P → Q`. Again: a proof $h$ of $P\implies Q$ is a term `h : P → Q`. This is why in the natural number game we use the `→` symbol to denote implication. -->
 
-`f : X → Y` であるとき，`f` は `X` から `Y` への関数であるということを思い出しましょう．ここで，$P$ と $Q$ を命題とし，$P\implies Q$ がわかっているとします．これは何を意味するでしょうか？これは $P$ ならば $Q$ であるということを意味します．$P$ が真であるとき，$Q$ も真だということです．$P$ の証明があれば，$Q$ の証明も作れるということです．$P\implies Q$ は $P$ の証明から $Q$ の証明を得る関数です．$P$ の要素を $Q$ の要素に送る関数です．`P → Q` 型を持つ項です．繰り返しますが，$P\implies Q$ の証明は `h : P → Q` という項 `h` です．natural number game で，私が `→` 記号を含意を表すのに使ったのは，このためです．
+`f : X → Y` であるとき，`f` は `X` から `Y` への関数であるということを思い出しましょう．ここで，\\(P\\) と \\(Q\\) を命題とし，\\(P\implies Q\\) がわかっているとします．これは何を意味するでしょうか？これは \\(P\\) ならば \\(Q\\) であるということを意味します．\\(P\\) が真であるとき，\\(Q\\) も真だということです．\\(P\\) の証明があれば，\\(Q\\) の証明も作れるということです．\\(P\implies Q\\) は \\(P\\) の証明から \\(Q\\) の証明を得る関数です．\\(P\\) の要素を \\(Q\\) の要素に送る関数です．`P → Q` 型を持つ項です．繰り返しますが，\\(P\implies Q\\) の証明は `h : P → Q` という項 `h` です．natural number game で，私が `→` 記号を含意を表すのに使ったのは，このためです．
 
 <!-- Let `false` denote a generic false statement (thought of as a set with $0$ elements), and let `true` denote a generic true statement (thought of as a set with $1$ element). Can we construct a term of type `false → false` or a term of type `true → true`? Sure — just use the identity function. In fact, in both cases there is a unique function — the hom sets have size $1$. Can we construct a term of type `false → true`? Sure, there is a function from the set with $0$ elements to a set with $1$ element, and again this function is unique. But can we construct a term of type `true → false`? No we can’t, because where do we send a proof of `true`? There are no proofs of `false` to send it to. So `true → false` is a set of size $0$. This corresponds to the standard truth table for `→`, where the first three statements we analysed were true and the last was false. -->
 
-`false` を一般的な偽の文（$0$ 個の要素を持つ集合と考えられる）とし，`true` を一般的な真の文（$1$ 個の要素を持つ集合と考えられる）とします．`false → false` 型の項，または `true → true` 型の項を作ることはできるでしょうか？もちろんです．―― 恒等関数を使えばよいだけです．実際，どちらの場合も関数は一意に定まります．―― hom 集合のサイズは $1$ です．`false → true` 型の項を作ることはできるでしょうか？もちろん，$0$ 個の要素を持つ集合から $1$ 個の要素を持つ集合への関数はあり，この関数も一意です．では `true → false` 型の項を作ることはできますか？これはできません．`true` の証明をどこに送ればいいのでしょうか？`false` の証明は存在しないので，送る先がありません．したがって `true → false` はサイズ $0$ の集合です．これは `→` の標準的な真理値表に相当し，最初に分析した３つの文は真で，最後の文は偽です．
+`false` を一般的な偽の文（0 個の要素を持つ集合と考えられる）とし，`true` を一般的な真の文（1 個の要素を持つ集合と考えられる）とします．`false → false` 型の項，または `true → true` 型の項を作ることはできるでしょうか？もちろんです．―― 恒等関数を使えばよいだけです．実際，どちらの場合も関数は一意に定まります．―― hom 集合のサイズは 1 です．`false → true` 型の項を作ることはできるでしょうか？もちろん，0 個の要素を持つ集合から 1 個の要素を持つ集合への関数はあり，この関数も一意です．では `true → false` 型の項を作ることはできますか？これはできません．`true` の証明をどこに送ればいいのでしょうか？`false` の証明は存在しないので，送る先がありません．したがって `true → false` はサイズ 0 の集合です．これは `→` の標準的な真理値表に相当し，最初に分析した３つの文は真で，最後の文は偽です．
diff --git a/src/c7_proof_fermat_theorem_function.md b/src/c7_proof_fermat_theorem_function.md
index 2443188..eed776f 100644
--- a/src/c7_proof_fermat_theorem_function.md
+++ b/src/c7_proof_fermat_theorem_function.md
@@ -3,7 +3,7 @@
 
 <!-- So what does a proof of `∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0` look like? Well, there is an arrow involved in that Proposition, so the statement of Fermat’s Last Theorem is some kind of set of the form $\mathrm{Hom}(A,B)$, which means that in Lean, a proof of Fermat’s Last Theorem is actually a function! And here is what that function does. It has four inputs. The first three inputs are natural numbers `x`, `y` and `z`. The fourth input is a proof: it is a proof of the Proposition `n > 2 ∧ x^n + y^n = z^n`. And the output of this function is a proof of the Proposition `x*y = 0`. This is quite an unconventional way to think about what the proof of Fermat’s Last Theorem is, and let me stress that it does not help at all with actually trying to understand the proof — but it is a completely consistent mental model for how mathematics works. Unifying the concept of a number and a proof — thinking of them both as terms — enables you to think of proofs as functions. Lean is a functional programming language, and in particular it is designed with functions at its heart. This, I believe, is why theorem provers such as Lean, Coq and Isabelle/HOL, which use type theory, are now moving ahead of provers such as Metamath and Mizar, which use set theory. -->
 
-では `∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0` の証明とはどのようなものでしょうか？この命題には矢印が含まれているので，フェルマーの最終定理のステートメントは $\mathrm{Hom}(A,B)$ という形の集合の一種です．Lean では，フェルマーの最終定理の証明は実際に関数です！その関数が何をするかは次の通りです．それは４つの入力を持ちます．最初の３つの入力は自然数 `x`, `y`, `z` です．４番目の入力は証明で，命題 `n > 2 ∧ x^n + y^n = z^n` の証明です．そして出力は命題 `x*y=0` の証明です．これは「フェルマーの最終定理の証明とは何か」という問いについてのきわめて型破りな考え方であり，証明を実際に理解しようとする際には全く役に立たないことを強調しておきましょう． ―― しかし，これは数学がどのように機能するかについての完全に一貫したメンタルモデルです．数と証明の概念を統一することで，―― つまり両方を項として考えることで，―― 証明を関数として考えることができます．Lean は関数型プログラミング言語であり，特に関数を中心に設計されています．現在 Lean や Coq や Isabelle/HOL といった型理論を使用する証明支援系が，Metamath や Mizar のような集合論を使用する証明支援系より進んでいるのは，このためだと私は確信しています．
+では `∀ x y z : ℕ, n > 2 ∧ x^n + y^n = z^n → x*y = 0` の証明とはどのようなものでしょうか？この命題には矢印が含まれているので，フェルマーの最終定理のステートメントは \\(\mathrm{Hom}(A,B)\\) という形の集合の一種です．Lean では，フェルマーの最終定理の証明は実際に関数です！その関数が何をするかは次の通りです．それは４つの入力を持ちます．最初の３つの入力は自然数 `x`, `y`, `z` です．４番目の入力は証明で，命題 `n > 2 ∧ x^n + y^n = z^n` の証明です．そして出力は命題 `x*y=0` の証明です．これは「フェルマーの最終定理の証明とは何か」という問いについてのきわめて型破りな考え方であり，証明を実際に理解しようとする際には全く役に立たないことを強調しておきましょう． ―― しかし，これは数学がどのように機能するかについての完全に一貫したメンタルモデルです．数と証明の概念を統一することで，―― つまり両方を項として考えることで，―― 証明を関数として考えることができます．Lean は関数型プログラミング言語であり，特に関数を中心に設計されています．現在 Lean や Coq や Isabelle/HOL といった型理論を使用する証明支援系が，Metamath や Mizar のような集合論を使用する証明支援系より進んでいるのは，このためだと私は確信しています．
 
 <!-- Prove a theorem! Write a function! -->
 
diff --git a/theme/header.hbs b/theme/header.hbs
deleted file mode 100644
index f5080b7..0000000
--- a/theme/header.hbs
+++ /dev/null
@@ -1,9 +0,0 @@
-<script src="https://polyfill.io/v3/polyfill.min.js?features=es6"></script>
-<script id="MathJax-script" async src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
-<script>
-  window.MathJax = {
-    tex: {
-      inlineMath: [['$', '$'], ['\\(', '\\)']]
-    }
-  };
-</script>
\ No newline at end of file