From 8240193ab00c86ccad1b62ffc941451e1543b1ff Mon Sep 17 00:00:00 2001
From: Fangyi Zhou <me@fangyi.io>
Date: Tue, 7 May 2019 16:39:18 +0100
Subject: [PATCH] Connectives: Use new format to put English before Chinese

---
 src/plfa/Connectives.lagda | 572 +++++++++++++++++++++++--------------
 1 file changed, 360 insertions(+), 212 deletions(-)

diff --git a/src/plfa/Connectives.lagda b/src/plfa/Connectives.lagda
index 82d0308bd..a2cd968d5 100644
--- a/src/plfa/Connectives.lagda
+++ b/src/plfa/Connectives.lagda
@@ -18,18 +18,14 @@ module plfa.Connectives where
      exercises from the final sections on distributivity
      and exponentials? -->
 
-本章节介绍基础的逻辑运算符。我们使用逻辑运算符与数据类型之间的对应关系，即*命题即类型*原理（Propositions as Types）。
 {::comment}
 This chapter introduces the basic logical connectives, by observing a
 correspondence between connectives of logic and data types, a
 principle known as _Propositions as Types_:
 {:/}
 
-  * *合取*（Conjunction）即是*积*（Product）
-  * *析取*（Disjunction）即是*和*（Sum）
-  * *真*（True）即是*单元类型*（Unit Type）
-  * *假*（False）即是*空类型*（Empty Type）
-  * *蕴含*（Implication）即是*函数空间*（Function Space）
+本章节介绍基础的逻辑运算符。我们使用逻辑运算符与数据类型之间的对应关系，
+即*命题即类型*原理（Propositions as Types）。
 
 {::comment}
   * _conjunction_ is _product_,
@@ -39,12 +35,18 @@ principle known as _Propositions as Types_:
   * _implication_ is _function space_.
 {:/}
 
+  * *合取*（Conjunction）即是*积*（Product）
+  * *析取*（Disjunction）即是*和*（Sum）
+  * *真*（True）即是*单元类型*（Unit Type）
+  * *假*（False）即是*空类型*（Empty Type）
+  * *蕴含*（Implication）即是*函数空间*（Function Space）
 
-## 导入
 {::comment}
 ## Imports
 {:/}
 
+## 导入
+
 \begin{code}
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
@@ -56,18 +58,21 @@ open plfa.Isomorphism.≃-Reasoning
 \end{code}
 
 
-## 合取即是积
 {::comment}
 ## Conjunction is product
 {:/}
 
-给定两个命题 `A` 和 `B`，其合取 `A × B` 成立当 `A` 成立和 `B` 成立。
-我们将这样的概念形式化，使用如下的归纳类型：
+## 合取即是积
+
 {::comment}
 Given two propositions `A` and `B`, the conjunction `A × B` holds
 if both `A` holds and `B` holds.  We formalise this idea by
 declaring a suitable inductive type:
 {:/}
+
+给定两个命题 `A` 和 `B`，其合取 `A × B` 成立当 `A` 成立和 `B` 成立。
+我们将这样的概念形式化，使用如下的归纳类型：
+
 \begin{code}
 data _×_ (A B : Set) : Set where
 
@@ -77,19 +82,22 @@ data _×_ (A B : Set) : Set where
       -----
     → A × B
 \end{code}
-`A × B` 成立的证明由 `⟨ M , N ⟩` 的形式表现，其中 `M` 是 `A` 成立的证明，
-`N` 是 `B` 成立的证明。
 {::comment}
 Evidence that `A × B` holds is of the form `⟨ M , N ⟩`, where `M`
 provides evidence that `A` holds and `N` provides evidence that `B`
 holds.
 {:/}
 
-给定 `A × B` 成立的证明，我们可以得出 `A` 成立或者 `B` 成立。
+`A × B` 成立的证明由 `⟨ M , N ⟩` 的形式表现，其中 `M` 是 `A` 成立的证明，
+`N` 是 `B` 成立的证明。
+
 {::comment}
 Given evidence that `A × B` holds, we can conclude that either
 `A` holds or `B` holds:
 {:/}
+
+给定 `A × B` 成立的证明，我们可以得出 `A` 成立或者 `B` 成立。
+
 \begin{code}
 proj₁ : ∀ {A B : Set}
   → A × B
@@ -104,17 +112,20 @@ proj₂ : ∀ {A B : Set}
 proj₂ ⟨ x , y ⟩ = y
 \end{code}
 
-如果 `L` 是 `A × B` 成立的证据, 那么 `proj₁ L` 是 `A` 成立的证据，
-`proj₂ L` 是 `B` 成立的证据。
 {::comment}
 If `L` provides evidence that `A × B` holds, then `proj₁ L` provides evidence
 that `A` holds, and `proj₂ L` provides evidence that `B` holds.
 {:/}
 
-等价地，我们亦可以将合取定义为一个记录类型：
+如果 `L` 是 `A × B` 成立的证据, 那么 `proj₁ L` 是 `A` 成立的证据，
+`proj₂ L` 是 `B` 成立的证据。
+
 {::comment}
 Equivalently, we could also declare conjunction as a record type:
 {:/}
+
+等价地，我们亦可以将合取定义为一个记录类型：
+
 \begin{code}
 record _×′_ (A B : Set) : Set where
   field
@@ -122,31 +133,31 @@ record _×′_ (A B : Set) : Set where
     proj₂′ : B
 open _×′_
 \end{code}
-在这里，记录的构造
 {::comment}
 Here record construction
 {:/}
 
+在这里，记录的构造
+
     record
       { proj₁′ = M
       ; proj₂′ = N
       }
 
-对应
 {::comment}
 corresponds to the term
 {:/}
 
+对应
+
     ⟨ M , N ⟩
 
-其中 `M` 是 `A` 类型的项，`N` 是 `B` 类型的项。
 {::comment}
 where `M` is a term of type `A` and `N` is a term of type `B`.
 {:/}
 
-当 `⟨_,_⟩` 在等式右手边的项中出现的时候，我们将其称作*构造器*（Constructor），
-当它出现在等式左边时，我们将其称作*析构器*（Destructor）。我们亦可将 `proj₁` 和 `proj₂`
-称作析构器，因为它们起到相似的效果。
+其中 `M` 是 `A` 类型的项，`N` 是 `B` 类型的项。
+
 {::comment}
 When `⟨_,_⟩` appears in a term on the right-hand side of an equation
 we refer to it as a _constructor_, and when it appears in a pattern on
@@ -155,12 +166,10 @@ We may also refer to `proj₁` and `proj₂` as destructors, since they
 play a similar role.
 {:/}
 
-其他的术语将 `⟨_,_⟩` 称作*引入*（Introduce）合取，将 `proj₁` 和 `proj₂` 称作*消去*（Eliminate）合取。
-前者亦记作 `×-I`，后者 `×-E₁` 和 `×-E₂`。如果我们从上到下来阅读这些规则，引入和消去
-正如其名字所说的那样：第一条*引入*一个运算符，所以运算符出现在结论中，而不是假设中；
-第二条*消去*一个带有运算符的式子，而运算符出现在假设中，而不是结论中。引入规则描述了
-运算符在什么情况下成立——即怎么样*定义*一个运算符。消去规则描述了运算符成立时，可以得出
-什么样的结论——即怎么样*使用*一个运算符。
+当 `⟨_,_⟩` 在等式右手边的项中出现的时候，我们将其称作*构造器*（Constructor），
+当它出现在等式左边时，我们将其称作*析构器*（Destructor）。我们亦可将 `proj₁` 和 `proj₂`
+称作析构器，因为它们起到相似的效果。
+
 {::comment}
 Other terminology refers to `⟨_,_⟩` as _introducing_ a conjunction, and
 to `proj₁` and `proj₂` as _eliminating_ a conjunction; indeed, the
@@ -176,46 +185,55 @@ elimination rule describes what we may conclude when the connective
 holds---how to _use_ the connective.
 {:/}
 
-（上面一段内容由此处改编得来：*Propositions as Types*，作者：Philip Wadler，发表于 《ACM 通讯》，2015 年 9 月）
+其他的术语将 `⟨_,_⟩` 称作*引入*（Introduce）合取，将 `proj₁` 和 `proj₂` 称作*消去*（Eliminate）合取。
+前者亦记作 `×-I`，后者 `×-E₁` 和 `×-E₂`。如果我们从上到下来阅读这些规则，引入和消去
+正如其名字所说的那样：第一条*引入*一个运算符，所以运算符出现在结论中，而不是假设中；
+第二条*消去*一个带有运算符的式子，而运算符出现在假设中，而不是结论中。引入规则描述了
+运算符在什么情况下成立——即怎么样*定义*一个运算符。消去规则描述了运算符成立时，可以得出
+什么样的结论——即怎么样*使用*一个运算符。
+
 {::comment}
 (The paragraph above was adopted from "Propositions as Types", Philip Wadler,
 _Communications of the ACM_, December 2015.)
 {:/}
 
-在这样的情况下，先使用析构器，再使用构造器将结果重组，得到还是原来的积。
+（上面一段内容由此处改编得来：*Propositions as Types*，作者：Philip Wadler，
+发表于 《ACM 通讯》，2015 年 9 月）
+
 {::comment}
 In this case, applying each destructor and reassembling the results with the
 constructor is the identity over products:
 {:/}
+
+在这样的情况下，先使用析构器，再使用构造器将结果重组，得到还是原来的积。
+
 \begin{code}
 η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
 η-× ⟨ x , y ⟩ = refl
 \end{code}
-左手边的模式匹配是必要的。用 `⟨ x , y ⟩` 来替换 `w` 让等式的两边可以化简成相同的项。
 {::comment}
 The pattern matching on the left-hand side is essential, since
 replacing `w` by `⟨ x , y ⟩` allows both sides of the
 propositional equality to simplify to the same term.
 {:/}
 
-我们设置合取的优先级，使它与除了析取之外结合的都不紧密：
+左手边的模式匹配是必要的。用 `⟨ x , y ⟩` 来替换 `w` 让等式的两边可以化简成相同的项。
+
 {::comment}
 We set the precedence of conjunction so that it binds less
 tightly than anything save disjunction:
 {:/}
+
+我们设置合取的优先级，使它与除了析取之外结合的都不紧密：
+
 \begin{code}
 infixr 2 _×_
 \end{code}
-因此，`m ≤ n × n ≤ p` 解析为 `(m ≤ n) × (n ≤ p)`。
 {::comment}
 Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)`.
 {:/}
 
-给定两个类型 `A` 和 `B`，我们将 `A × B` 称为 `A` 与 `B` 的*积*。
-在集合论中它也被称作*笛卡尔积*（Cartesian Product），在计算机科学中它对应*记录*类型。
-如果类型 `A` 有 `m` 个不同的成员，类型 `B` 有 `n` 个不同的成员，
-那么类型 `A × B` 有 `m * n` 个不同的成员。这也是它被称为积的原因之一。
-例如，考虑有两个成员的 `Bool` 类型，和有三个成员的 `Tri` 类型：
+因此，`m ≤ n × n ≤ p` 解析为 `(m ≤ n) × (n ≤ p)`。
 
 {::comment}
 Given two types `A` and `B`, we refer to `A × B` as the
@@ -228,6 +246,13 @@ then the type `A × B` has `m * n` distinct members.
 For instance, consider a type `Bool` with two members, and
 a type `Tri` with three members:
 {:/}
+
+给定两个类型 `A` 和 `B`，我们将 `A × B` 称为 `A` 与 `B` 的*积*。
+在集合论中它也被称作*笛卡尔积*（Cartesian Product），在计算机科学中它对应*记录*类型。
+如果类型 `A` 有 `m` 个不同的成员，类型 `B` 有 `n` 个不同的成员，
+那么类型 `A × B` 有 `m * n` 个不同的成员。这也是它被称为积的原因之一。
+例如，考虑有两个成员的 `Bool` 类型，和有三个成员的 `Tri` 类型：
+
 \begin{code}
 data Bool : Set where
   true  : Bool
@@ -238,19 +263,22 @@ data Tri : Set where
   bb : Tri
   cc : Tri
 \end{code}
-那么，`Bool × Tri` 类型有如下的六个成员：
 {::comment}
 Then the type `Bool × Tri` has six members:
 {:/}
 
+那么，`Bool × Tri` 类型有如下的六个成员：
+
     ⟨ true  , aa ⟩    ⟨ true  , bb ⟩    ⟨ true ,  cc ⟩
     ⟨ false , aa ⟩    ⟨ false , bb ⟩    ⟨ false , cc ⟩
 
-下面的函数枚举了所有类型为 `Bool × Tri` 的参数：
 {::comment}
 For example, the following function enumerates all
 possible arguments of type `Bool × Tri`:
 {:/}
+
+下面的函数枚举了所有类型为 `Bool × Tri` 的参数：
+
 \begin{code}
 ×-count : Bool × Tri → ℕ
 ×-count ⟨ true  , aa ⟩  =  1
@@ -261,8 +289,6 @@ possible arguments of type `Bool × Tri`:
 ×-count ⟨ false , cc ⟩  =  6
 \end{code}
 
-类型上的积与数的积有相似的性质——它们满足交换律和结合律。
-更确切地说，积在*忽略同构*的情况下是交换和结合的。
 {::comment}
 Product on types also shares a property with product on numbers in
 that there is a sense in which it is commutative and associative.  In
@@ -270,10 +296,9 @@ particular, product is commutative and associative _up to
 isomorphism_.
 {:/}
 
-对于交换律，`to` 函数将有序对交换，将 `⟨ x , y ⟩` 变为 `⟨ y , x ⟩`，`from`
-函数亦是如此（忽略命名）。
-在 `from∘to` 和 `to∘from` 中正确地实例化要匹配的模式是很重要的。
-使用 `λ w → refl` 作为 `from∘to` 的定义是不可行的，`to∘from` 同理。
+类型上的积与数的积有相似的性质——它们满足交换律和结合律。
+更确切地说，积在*忽略同构*的情况下是交换和结合的。
+
 {::comment}
 For commutativity, the `to` function swaps a pair, taking `⟨ x , y ⟩` to
 `⟨ y , x ⟩`, and the `from` function does the same (up to renaming).
@@ -281,6 +306,12 @@ Instantiating the patterns correctly in `from∘to` and `to∘from` is essential
 Replacing the definition of `from∘to` by `λ w → refl` will not work;
 and similarly for `to∘from`:
 {:/}
+
+对于交换律，`to` 函数将有序对交换，将 `⟨ x , y ⟩` 变为 `⟨ y , x ⟩`，`from`
+函数亦是如此（忽略命名）。
+在 `from∘to` 和 `to∘from` 中正确地实例化要匹配的模式是很重要的。
+使用 `λ w → refl` 作为 `from∘to` 的定义是不可行的，`to∘from` 同理。
+
 \begin{code}
 ×-comm : ∀ {A B : Set} → A × B ≃ B × A
 ×-comm =
@@ -292,19 +323,16 @@ and similarly for `to∘from`:
     }
 \end{code}
 
-满足*交换律*和*忽略同构*下满足*交换律*是不一样的。比较下列两个命题：
 {::comment}
 Being _commutative_ is different from being _commutative up to
 isomorphism_.  Compare the two statements:
 {:/}
 
+满足*交换律*和*忽略同构*下满足*交换律*是不一样的。比较下列两个命题：
+
     m * n ≡ n * m
     A × B ≃ B × A
 
-在第一个情况下，我们可能有 `m` 是 `2`、`n` 是 `3`，那么 `m * n` 和 `n * m` 都是 `6`。
-在第二个情况下，我们可能有 `A` 是 `Bool` 和 `B` 是 `Tri`，但是 `Bool × Tri` 和
-`Tri × Bool` *不是*一样的。但是存在一个两者之间的同构。例如：`⟨ true , aa ⟩` 是前者的成员，
-其对应后者的成员 `⟨ aa , true ⟩`。
 {::comment}
 In the first case, we might have that `m` is `2` and `n` is `3`, and
 both `m * n` and `n * m` are equal to `6`.  In the second case, we
@@ -314,14 +342,21 @@ the two types.  For instance, `⟨ true , aa ⟩`, which is a member of the
 former, corresponds to `⟨ aa , true ⟩`, which is a member of the latter.
 {:/}
 
-对于结合律来说，`to` 函数将两个有序对进行重组：将 `⟨ ⟨ x , y ⟩ , z ⟩` 转换为 `⟨ x , ⟨ y , z ⟩ ⟩`，
-`from` 函数则为其逆。同样，左逆和右逆的证明需要在一个合适的模式来匹配，从而可以直接化简：
+在第一个情况下，我们可能有 `m` 是 `2`、`n` 是 `3`，那么 `m * n` 和 `n * m` 都是 `6`。
+在第二个情况下，我们可能有 `A` 是 `Bool` 和 `B` 是 `Tri`，但是 `Bool × Tri` 和
+`Tri × Bool` *不是*一样的。但是存在一个两者之间的同构。例如：`⟨ true , aa ⟩` 是前者的成员，
+其对应后者的成员 `⟨ aa , true ⟩`。
+
 {::comment}
 For associativity, the `to` function reassociates two uses of pairing,
 taking `⟨ ⟨ x , y ⟩ , z ⟩` to `⟨ x , ⟨ y , z ⟩ ⟩`, and the `from` function does
 the inverse.  Again, the evidence of left and right inverse requires
 matching against a suitable pattern to enable simplification:
 {:/}
+
+对于结合律来说，`to` 函数将两个有序对进行重组：将 `⟨ ⟨ x , y ⟩ , z ⟩` 转换为 `⟨ x , ⟨ y , z ⟩ ⟩`，
+`from` 函数则为其逆。同样，左逆和右逆的证明需要在一个合适的模式来匹配，从而可以直接化简：
+
 \begin{code}
 ×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C)
 ×-assoc =
@@ -333,18 +368,16 @@ matching against a suitable pattern to enable simplification:
     }
 \end{code}
 
-满足*结合律*和*忽略同构*下满足*结合律*是不一样的。比较下列两个命题：
 {::comment}
 Being _associative_ is not the same as being _associative
 up to isomorphism_.  Compare the two statements:
 {:/}
 
+满足*结合律*和*忽略同构*下满足*结合律*是不一样的。比较下列两个命题：
+
     (m * n) * p ≡ m * (n * p)
     (A × B) × C ≃ A × (B × C)
 
-举个例子，`(ℕ × Bool) × Tri` 与 `ℕ × (Bool × Tri)` *不同*，但是两个类型之间
-存在同构。例如 `⟨ ⟨ 1 , true ⟩ , aa ⟩`，一个前者的成员，与 `⟨ 1 , ⟨ true , aa ⟩ ⟩`，
-一个后者的成员，相对应。
 {::comment}
 For example, the type `(ℕ × Bool) × Tri` is _not_ the same as `ℕ ×
 (Bool × Tri)`. But there is an isomorphism between the two types. For
@@ -352,20 +385,22 @@ instance `⟨ ⟨ 1 , true ⟩ , aa ⟩`, which is a member of the former,
 corresponds to `⟨ 1 , ⟨ true , aa ⟩ ⟩`, which is a member of the latter.
 {:/}
 
-#### 练习 `⇔≃×` （推荐）
+举个例子，`(ℕ × Bool) × Tri` 与 `ℕ × (Bool × Tri)` *不同*，但是两个类型之间
+存在同构。例如 `⟨ ⟨ 1 , true ⟩ , aa ⟩`，一个前者的成员，与 `⟨ 1 , ⟨ true , aa ⟩ ⟩`，
+一个后者的成员，相对应。
+
 {::comment}
 #### Exercise `⇔≃×` (recommended)
 {:/}
 
-证明[之前][plfa.Isomorphism#iff]定义的 `A ⇔ B` 与 `(A → B) × (B → A)` 同构。
+#### 练习 `⇔≃×` （推荐）
+
 {::comment}
 Show that `A ⇔ B` as defined [earlier][plfa.Isomorphism#iff]
 is isomorphic to `(A → B) × (B → A)`.
 {:/}
 
-\begin{code}
--- 请将代码写在此处。
-\end{code}
+证明[之前][plfa.Isomorphism#iff]定义的 `A ⇔ B` 与 `(A → B) × (B → A)` 同构。
 
 {::comment}
 \begin{code}
@@ -373,17 +408,23 @@ is isomorphic to `(A → B) × (B → A)`.
 \end{code}
 {:/}
 
+\begin{code}
+-- 请将代码写在此处。
+\end{code}
 
-## 真即是单元类型
 {::comment}
 ## Truth is unit
 {:/}
 
-恒真 `⊤` 恒成立。我们将这个概念用合适的归纳类型来形式化：
+## 真即是单元类型
+
 {::comment}
 Truth `⊤` always holds. We formalise this idea by
 declaring a suitable inductive type:
 {:/}
+
+恒真 `⊤` 恒成立。我们将这个概念用合适的归纳类型来形式化：
+
 \begin{code}
 data ⊤ : Set where
 
@@ -391,13 +432,12 @@ data ⊤ : Set where
     --
     ⊤
 \end{code}
-`⊤` 成立的证明由 `tt` 的形式构成。
 {::comment}
 Evidence that `⊤` holds is of the form `tt`.
 {:/}
 
-恒真有引入规则，但没有消去规则。给定一个 `⊤` 成立的证明，我们不能得出任何有趣的结论。
-因为恒真恒成立，知道恒真成立不会给我们带来新的知识。
+`⊤` 成立的证明由 `tt` 的形式构成。
+
 {::comment}
 There is an introduction rule, but no elimination rule.
 Given evidence that `⊤` holds, there is nothing more of interest we
@@ -405,37 +445,42 @@ can conclude.  Since truth always holds, knowing that it holds tells
 us nothing new.
 {:/}
 
-`η-×` 的 零元形式是 `η-⊤`，其断言了任何 `⊤` 类型的值一定等于 `tt`：
+恒真有引入规则，但没有消去规则。给定一个 `⊤` 成立的证明，我们不能得出任何有趣的结论。
+因为恒真恒成立，知道恒真成立不会给我们带来新的知识。
+
 {::comment}
 The nullary case of `η-×` is `η-⊤`, which asserts that any
 value of type `⊤` must be equal to `tt`:
 {:/}
+
+`η-×` 的 零元形式是 `η-⊤`，其断言了任何 `⊤` 类型的值一定等于 `tt`：
+
 \begin{code}
 η-⊤ : ∀ (w : ⊤) → tt ≡ w
 η-⊤ tt = refl
 \end{code}
-左手边的模式匹配是必要的。将 `w` 替换为 `tt` 让等式两边可以化简为相同的值。
 {::comment}
 The pattern matching on the left-hand side is essential.  Replacing
 `w` by `tt` allows both sides of the propositional equality to
 simplify to the same term.
 {:/}
 
-我们将 `⊤` 称为*单元*类型（Unit Type）。实际上，`⊤` 类型只有一个成员 `tt`。
-例如，下面的函数枚举了所有 `⊤` 类型的参数：
+左手边的模式匹配是必要的。将 `w` 替换为 `tt` 让等式两边可以化简为相同的值。
+
 {::comment}
 We refer to `⊤` as the _unit_ type. And, indeed,
 type `⊤` has exactly one member, `tt`.  For example, the following
 function enumerates all possible arguments of type `⊤`:
+
+我们将 `⊤` 称为*单元*类型（Unit Type）。实际上，`⊤` 类型只有一个成员 `tt`。
+例如，下面的函数枚举了所有 `⊤` 类型的参数：
+
 {:/}
 \begin{code}
 ⊤-count : ⊤ → ℕ
 ⊤-count tt = 1
 \end{code}
 
-对于数来说，1 是乘法的幺元。对应地，单元是积的幺元（*忽略同构*）。对于左幺元来说，
-`to` 函数将 `⟨ tt , x ⟩` 转换成 `x`， `from` 函数则是其反函数。左逆的证明需要
-匹配一个合适的模式来化简：
 {::comment}
 For numbers, one is the identity of multiplication. Correspondingly,
 unit is the identity of product _up to isomorphism_.  For left
@@ -443,6 +488,11 @@ identity, the `to` function takes `⟨ tt , x ⟩` to `x`, and the `from`
 function does the inverse.  The evidence of left inverse requires
 matching against a suitable pattern to enable simplification:
 {:/}
+
+对于数来说，1 是乘法的幺元。对应地，单元是积的幺元（*忽略同构*）。对于左幺元来说，
+`to` 函数将 `⟨ tt , x ⟩` 转换成 `x`， `from` 函数则是其反函数。左逆的证明需要
+匹配一个合适的模式来化简：
+
 \begin{code}
 ⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A
 ⊤-identityˡ =
@@ -454,18 +504,16 @@ matching against a suitable pattern to enable simplification:
     }
 \end{code}
 
-*幺元*和*忽略同构*的*幺元*是不一样的。比较下列两个命题：
 {::comment}
 Having an _identity_ is different from having an identity
 _up to isomorphism_.  Compare the two statements:
 {:/}
 
+*幺元*和*忽略同构*的*幺元*是不一样的。比较下列两个命题：
+
     1 * m ≡ m
     ⊤ × A ≃ A
 
-在第一种情况下，我们可能有 `m` 是 `2`，那么 `1 * m` 和 `m` 都为 `2`。
-在第二种情况下，我们可能有 `A` 是 `Bool`，但是 `⊤ × Bool` 和 `Bool` 是不同的。
-例如：`⟨ tt , true ⟩` 是前者的成员，其对应后者的成员 `true`。
 {::comment}
 In the first case, we might have that `m` is `2`, and both
 `1 * m` and `m` are equal to `2`.  In the second
@@ -475,10 +523,16 @@ For instance, `⟨ tt , true ⟩`, which is a member of the former,
 corresponds to `true`, which is a member of the latter.
 {:/}
 
-右幺元可以由积的交换律得来：
+在第一种情况下，我们可能有 `m` 是 `2`，那么 `1 * m` 和 `m` 都为 `2`。
+在第二种情况下，我们可能有 `A` 是 `Bool`，但是 `⊤ × Bool` 和 `Bool` 是不同的。
+例如：`⟨ tt , true ⟩` 是前者的成员，其对应后者的成员 `true`。
+
 {::comment}
 Right identity follows from commutativity of product and left identity:
 {:/}
+
+右幺元可以由积的交换律得来：
+
 \begin{code}
 ⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A
 ⊤-identityʳ {A} =
@@ -490,25 +544,28 @@ Right identity follows from commutativity of product and left identity:
     A
   ≃-∎
 \end{code}
-我们在此使用了同构链，与等式链相似。
 {::comment}
 Here we have used a chain of isomorphisms, analogous to that used for
 equality.
 {:/}
 
+我们在此使用了同构链，与等式链相似。
 
-## 析取即是和
 {::comment}
 ## Disjunction is sum
 {:/}
 
-给定两个命题 `A` 和 `B`，析取 `A ⊎ B` 在 `A` 成立或者 `B` 成立时成立。
-我们将这个概念用合适的归纳类型来形式化：
+## 析取即是和
+
 {::comment}
 Given two propositions `A` and `B`, the disjunction `A ⊎ B` holds
 if either `A` holds or `B` holds.  We formalise this idea by
 declaring a suitable inductive type:
 {:/}
+
+给定两个命题 `A` 和 `B`，析取 `A ⊎ B` 在 `A` 成立或者 `B` 成立时成立。
+我们将这个概念用合适的归纳类型来形式化：
+
 \begin{code}
 data _⊎_ (A B : Set) : Set where
 
@@ -522,19 +579,22 @@ data _⊎_ (A B : Set) : Set where
       -----
     → A ⊎ B
 \end{code}
-`A ⊎ B` 成立的证明有两个形式： `inj₁ M`，其中 `M` 是 `A` 成立的证明，或者
-`inj₂ N`，其中 `N` 是 `B` 成立的证明。
 {::comment}
 Evidence that `A ⊎ B` holds is either of the form `inj₁ M`, where `M`
 provides evidence that `A` holds, or `inj₂ N`, where `N` provides
 evidence that `B` holds.
 {:/}
 
-给定 `A → C` 和 `B → C` 成立的证明，那么给定一个 `A ⊎ B` 的证明，我们可以得出 `C` 成立：
+`A ⊎ B` 成立的证明有两个形式： `inj₁ M`，其中 `M` 是 `A` 成立的证明，或者
+`inj₂ N`，其中 `N` 是 `B` 成立的证明。
+
 {::comment}
 Given evidence that `A → C` and `B → C` both hold, then given
 evidence that `A ⊎ B` holds we can conclude that `C` holds:
 {:/}
+
+给定 `A → C` 和 `B → C` 成立的证明，那么给定一个 `A ⊎ B` 的证明，我们可以得出 `C` 成立：
+
 \begin{code}
 case-⊎ : ∀ {A B C : Set}
   → (A → C)
@@ -545,16 +605,13 @@ case-⊎ : ∀ {A B C : Set}
 case-⊎ f g (inj₁ x) = f x
 case-⊎ f g (inj₂ y) = g y
 \end{code}
-对 `inj₁` 和 `inj₂` 进行模式匹配，是我们使用析取成立的证明的常见方法。
 {::comment}
 Pattern matching against `inj₁` and `inj₂` is typical of how we exploit
 evidence that a disjunction holds.
 {:/}
 
-当 `inj₁` 和 `inj₂` 在等式右手边出现的时候，我们将其称作*构造器*，
-当它出现在等式左边时，我们将其称作*析构器*。我们亦可将 `case-⊎`
-称作析构器，因为它们起到相似的效果。其他术语将 `inj₁` 和 `inj₂` 称为*引入*析取，
-将 `case-⊎` 称为*消去*析取。前者亦被称为 `⊎-I₁` 和 `⊎-I₂`，后者 `⊎-E`。
+对 `inj₁` 和 `inj₂` 进行模式匹配，是我们使用析取成立的证明的常见方法。
+
 {::comment}
 When `inj₁` and `inj₂` appear on the right-hand side of an equation we
 refer to them as _constructors_, and when they appear on the
@@ -566,52 +623,59 @@ the former are sometimes given the names `⊎-I₁` and `⊎-I₂` and the
 latter the name `⊎-E`.
 {:/}
 
-对每个构造器使用析构器得到的是原来的值：
+当 `inj₁` 和 `inj₂` 在等式右手边出现的时候，我们将其称作*构造器*，
+当它出现在等式左边时，我们将其称作*析构器*。我们亦可将 `case-⊎`
+称作析构器，因为它们起到相似的效果。其他术语将 `inj₁` 和 `inj₂` 称为*引入*析取，
+将 `case-⊎` 称为*消去*析取。前者亦被称为 `⊎-I₁` 和 `⊎-I₂`，后者 `⊎-E`。
+
 {::comment}
 Applying the destructor to each of the constructors is the identity:
 {:/}
+
+对每个构造器使用析构器得到的是原来的值：
+
 \begin{code}
 η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w
 η-⊎ (inj₁ x) = refl
 η-⊎ (inj₂ y) = refl
 \end{code}
-更普遍地来说，我们亦可对于析取使用一个任意的函数：
 {::comment}
 More generally, we can also throw in an arbitrary function from a disjunction:
 {:/}
+
+更普遍地来说，我们亦可对于析取使用一个任意的函数：
+
 \begin{code}
 uniq-⊎ : ∀ {A B C : Set} (h : A ⊎ B → C) (w : A ⊎ B) →
   case-⊎ (h ∘ inj₁) (h ∘ inj₂) w ≡ h w
 uniq-⊎ h (inj₁ x) = refl
 uniq-⊎ h (inj₂ y) = refl
 \end{code}
-左手边的模式匹配是必要的。用 `inj₁ x` 来替换 `w` 让等式的两边可以化简成相同的项，
-`inj₂ y` 同理。
 {::comment}
 The pattern matching on the left-hand side is essential.  Replacing
 `w` by `inj₁ x` allows both sides of the propositional equality to
 simplify to the same term, and similarly for `inj₂ y`.
 {:/}
 
-我们设置析取的优先级，使它与任何已经定义的运算符都结合的不紧密：
+左手边的模式匹配是必要的。用 `inj₁ x` 来替换 `w` 让等式的两边可以化简成相同的项，
+`inj₂ y` 同理。
+
 {::comment}
 We set the precedence of disjunction so that it binds less tightly
 than any other declared operator:
 {:/}
+
+我们设置析取的优先级，使它与任何已经定义的运算符都结合的不紧密：
+
 \begin{code}
 infix 1 _⊎_
 \end{code}
-因此 `A × C ⊎ B × C` 解析为 `(A × C) ⊎ (B × C)`。
 {::comment}
 Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.
 {:/}
 
-给定两个类型 `A` 和 `B`，我们将 `A ⊎ B` 称为 `A` 与 `B` 的*和*。
-在集合论中它也被称作*不交并*（Disjoint Union），在计算机科学中它对应*变体记录*类型。
-如果类型 `A` 有 `m` 个不同的成员，类型 `B` 有 `n` 个不同的成员，
-那么类型 `A ⊎ B` 有 `m + n` 个不同的成员。这也是它被称为和的原因之一。
-例如，考虑有两个成员的 `Bool` 类型，和有三个成员的 `Tri` 类型，如之前的定义。
-那么，`Bool ⊎ Tri` 类型有如下的五个成员：
+因此 `A × C ⊎ B × C` 解析为 `(A × C) ⊎ (B × C)`。
+
 {::comment}
 Given two types `A` and `B`, we refer to `A ⊎ B` as the
 _sum_ of `A` and `B`.  In set theory, it is also sometimes
@@ -626,15 +690,24 @@ Then the type `Bool ⊎ Tri` has five
 members:
 {:/}
 
+给定两个类型 `A` 和 `B`，我们将 `A ⊎ B` 称为 `A` 与 `B` 的*和*。
+在集合论中它也被称作*不交并*（Disjoint Union），在计算机科学中它对应*变体记录*类型。
+如果类型 `A` 有 `m` 个不同的成员，类型 `B` 有 `n` 个不同的成员，
+那么类型 `A ⊎ B` 有 `m + n` 个不同的成员。这也是它被称为和的原因之一。
+例如，考虑有两个成员的 `Bool` 类型，和有三个成员的 `Tri` 类型，如之前的定义。
+那么，`Bool ⊎ Tri` 类型有如下的五个成员：
+
     inj₁ true     inj₂ aa
     inj₁ false    inj₂ bb
                   inj₂ cc
 
-下面的函数枚举了所有类型为 `Bool ⊎ Tri` 的参数：
 {::comment}
 For example, the following function enumerates all
 possible arguments of type `Bool ⊎ Tri`:
 {:/}
+
+下面的函数枚举了所有类型为 `Bool ⊎ Tri` 的参数：
+
 \begin{code}
 ⊎-count : Bool ⊎ Tri → ℕ
 ⊎-count (inj₁ true)   =  1
@@ -644,26 +717,25 @@ possible arguments of type `Bool ⊎ Tri`:
 ⊎-count (inj₂ cc)     =  5
 \end{code}
 
-类型上的和与数的和有相似的性质——它们满足交换律和结合律。
-更确切地说，和在*忽略同构*的情况下是交换和结合的。
 {::comment}
 Sum on types also shares a property with sum on numbers in that it is
 commutative and associative _up to isomorphism_.
 {:/}
 
-#### 练习 `⊎-comm` （推荐）
+类型上的和与数的和有相似的性质——它们满足交换律和结合律。
+更确切地说，和在*忽略同构*的情况下是交换和结合的。
+
 {::comment}
 #### Exercise `⊎-comm` (recommended)
 {:/}
 
-证明和类型在忽略同构下满足交换律。
+#### 练习 `⊎-comm` （推荐）
+
 {::comment}
 Show sum is commutative up to isomorphism.
 {:/}
 
-\begin{code}
--- 请将代码写在此处。
-\end{code}
+证明和类型在忽略同构下满足交换律。
 
 {::comment}
 \begin{code}
@@ -671,19 +743,21 @@ Show sum is commutative up to isomorphism.
 \end{code}
 {:/}
 
-#### 练习 `⊎-assoc`
+\begin{code}
+-- 请将代码写在此处。
+\end{code}
+
 {::comment}
 #### Exercise `⊎-assoc`
 {:/}
 
-证明和类型在忽略同构下满足结合律。
+#### 练习 `⊎-assoc`
+
 {::comment}
 Show sum is associative up to isomorphism.
 {:/}
 
-\begin{code}
--- 请将代码写在此处。
-\end{code}
+证明和类型在忽略同构下满足结合律。
 
 {::comment}
 \begin{code}
@@ -691,21 +765,22 @@ Show sum is associative up to isomorphism.
 \end{code}
 {:/}
 
-## 假即是空类型
+\begin{code}
+-- 请将代码写在此处。
+\end{code}
+
 {::comment}
 ## False is empty
 {:/}
 
-恒假 `⊥` 从不成立。我们将这个概念用合适的归纳类型来形式化：
+## 假即是空类型
+
 {::comment}
 False `⊥` never holds.  We formalise this idea by declaring
 a suitable inductive type:
 {:/}
 
-\begin{code}
-data ⊥ : Set where
-  -- 没有语句！
-\end{code}
+恒假 `⊥` 从不成立。我们将这个概念用合适的归纳类型来形式化：
 
 {::comment}
 FIXME: the code block is removed to make Agda not recognise this as code.
@@ -713,15 +788,17 @@ data ⊥ : Set where
   -- no clauses!
 {:/}
 
-没有 `⊥` 成立的证明。
+\begin{code}
+data ⊥ : Set where
+  -- 没有语句！
+\end{code}
+
 {::comment}
 There is no possible evidence that `⊥` holds.
 {:/}
 
-与 `⊤` 相对偶，`⊥` 没有引入规则，但是有消去规则。因为恒假从不成立，
-如果它一旦成立，我们就进入了矛盾之中。给定 `⊥` 成立的证明，我们可以得出任何结论！
-这是逻辑学的基本原理，又由中世纪的拉丁文词组 _ex falso_ 为名。小孩子也由诸如
-“如果猪有翅膀，那我就是示巴女王”的词组中知晓。我们如下将它形式化：
+没有 `⊥` 成立的证明。
+
 {::comment}
 Dual to `⊤`, for `⊥` there is no introduction rule but an elimination rule.
 Since false never holds, knowing that it holds tells us we are in a
@@ -731,6 +808,12 @@ medieval times by the Latin phrase _ex falso_, and known to children
 through phrases such as "if pigs had wings, then I'd be the Queen of
 Sheba".  We formalise it as follows:
 {:/}
+
+与 `⊤` 相对偶，`⊥` 没有引入规则，但是有消去规则。因为恒假从不成立，
+如果它一旦成立，我们就进入了矛盾之中。给定 `⊥` 成立的证明，我们可以得出任何结论！
+这是逻辑学的基本原理，又由中世纪的拉丁文词组 _ex falso_ 为名。小孩子也由诸如
+“如果猪有翅膀，那我就是示巴女王”的词组中知晓。我们如下将它形式化：
+
 \begin{code}
 ⊥-elim : ∀ {A : Set}
   → ⊥
@@ -738,8 +821,6 @@ Sheba".  We formalise it as follows:
   → A
 ⊥-elim ()
 \end{code}
-这是我们第一次使用*荒谬模式*（Absurd Pattern） `()`。在这里，因为 `⊥`
-是一个没有成员的类型，我们用 `()` 模式来指明这里不可能匹配任何这个类型的值。
 {::comment}
 This is our first use of the _absurd pattern_ `()`.
 Here since `⊥` is a type with no members, we indicate that it is
@@ -747,65 +828,74 @@ _never_ possible to match against a value of this type by using
 the pattern `()`.
 {:/}
 
-`case-⊎` 的零元形式是 `⊥-elim`。类比的来说，它应该叫做 `case-⊥`，
-但是我们在此使用标准库中使用的名字。
+这是我们第一次使用*荒谬模式*（Absurd Pattern） `()`。在这里，因为 `⊥`
+是一个没有成员的类型，我们用 `()` 模式来指明这里不可能匹配任何这个类型的值。
+
 {::comment}
 The nullary case of `case-⊎` is `⊥-elim`.  By analogy,
 we might have called it `case-⊥`, but chose to stick with the name
 in the standard library.
 {:/}
 
-`uniq-⊎` 的零元形式是 `uniq-⊥`，其断言了 `⊥-elim` 和任何取 `⊥` 的函数是等价的。
+`case-⊎` 的零元形式是 `⊥-elim`。类比的来说，它应该叫做 `case-⊥`，
+但是我们在此使用标准库中使用的名字。
+
 {::comment}
 The nullary case of `uniq-⊎` is `uniq-⊥`, which asserts that `⊥-elim`
 is equal to any arbitrary function from `⊥`:
 {:/}
+
+`uniq-⊎` 的零元形式是 `uniq-⊥`，其断言了 `⊥-elim` 和任何取 `⊥` 的函数是等价的。
+
 \begin{code}
 uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w
 uniq-⊥ h ()
 \end{code}
-使用荒谬模式断言了 `w` 没有任何可能的值，因此等式显然成立。
 {::comment}
 Using the absurd pattern asserts there are no possible values for `w`,
 so the equation holds trivially.
 {:/}
 
-我们将 `⊥` 成为*空*类型（Empty Type）。实际上，`⊥` 类型没有成员。
-例如，下面的函数枚举了所有 `⊥` 类型的参数：
+使用荒谬模式断言了 `w` 没有任何可能的值，因此等式显然成立。
+
 {::comment}
 We refer to `⊥` as the _empty_ type. And, indeed,
 type `⊥` has no members. For example, the following function
 enumerates all possible arguments of type `⊥`:
+
+我们将 `⊥` 成为*空*类型（Empty Type）。实际上，`⊥` 类型没有成员。
+例如，下面的函数枚举了所有 `⊥` 类型的参数：
+
 {:/}
 \begin{code}
 ⊥-count : ⊥ → ℕ
 ⊥-count ()
 \end{code}
-同样，荒谬模式告诉我们没有值可以来匹配类型 `⊥`。
 {::comment}
 Here again the absurd pattern `()` indicates that no value can match
 type `⊥`.
 {:/}
 
-对于数来说，0 是加法的幺元。对应地，空是和的幺元（*忽略同构*）。
+同样，荒谬模式告诉我们没有值可以来匹配类型 `⊥`。
+
 {::comment}
 For numbers, zero is the identity of addition. Correspondingly, empty
 is the identity of sums _up to isomorphism_.
 {:/}
 
-#### 练习 `⊥-identityˡ` （推荐）
+对于数来说，0 是加法的幺元。对应地，空是和的幺元（*忽略同构*）。
+
 {::comment}
 #### Exercise `⊥-identityˡ` (recommended)
 {:/}
 
-证明空在忽略同构下是和的左幺元。
+#### 练习 `⊥-identityˡ` （推荐）
+
 {::comment}
 Show empty is the left identity of sums up to isomorphism.
 {:/}
 
-\begin{code}
--- 请将代码写在此处。
-\end{code}
+证明空在忽略同构下是和的左幺元。
 
 {::comment}
 \begin{code}
@@ -813,19 +903,21 @@ Show empty is the left identity of sums up to isomorphism.
 \end{code}
 {:/}
 
-#### 练习 `⊥-identityʳ`
+\begin{code}
+-- 请将代码写在此处。
+\end{code}
+
 {::comment}
 #### Exercise `⊥-identityʳ`
 {:/}
 
-证明空在忽略同构下是和的右幺元。
+#### 练习 `⊥-identityʳ`
+
 {::comment}
 Show empty is the right identity of sums up to isomorphism.
 {:/}
 
-\begin{code}
--- 请将代码写在此处。
-\end{code}
+证明空在忽略同构下是和的右幺元。
 
 {::comment}
 \begin{code}
@@ -833,30 +925,34 @@ Show empty is the right identity of sums up to isomorphism.
 \end{code}
 {:/}
 
-## 蕴含即是函数 {#implication}
+\begin{code}
+-- 请将代码写在此处。
+\end{code}
+
 {::comment}
 ## Implication is function {#implication}
 {:/}
 
-给定两个命题 `A` 和 `B`，其蕴含 `A → B` 在任何 `A` 成立的时候，`B` 也成立时成立。
-我们用函数类型来形式化蕴含，如本书中通篇出现的那样。
+## 蕴含即是函数 {#implication}
+
 {::comment}
 Given two propositions `A` and `B`, the implication `A → B` holds if
 whenever `A` holds then `B` must also hold.  We formalise implication using
 the function type, which has appeared throughout this book.
 {:/}
 
-`A → B` 成立的证据由下面的形式组成：
+给定两个命题 `A` 和 `B`，其蕴含 `A → B` 在任何 `A` 成立的时候，`B` 也成立时成立。
+我们用函数类型来形式化蕴含，如本书中通篇出现的那样。
+
 
 {::comment}
 Evidence that `A → B` holds is of the form
 {:/}
 
+`A → B` 成立的证据由下面的形式组成：
+
     λ (x : A) → N
 
-其中 `N` 是一个类型为 `B` 的项，其包括了一个类型为 `A` 的自由变量 `x`。
-给定一个 `A → B` 成立的证明 `L`，和一个 `A` 成立的证明 `M`，那么 `L M` 是 `B` 成立的证明。
-也就是说，`A → B` 成立的证明是一个函数，将 `A` 成立的证明转换成 `B` 成立的证明。
 {::comment}
 where `N` is a term of type `B` containing as a free variable `x` of type `A`.
 Given a term `L` providing evidence that `A → B` holds, and a term `M`
@@ -865,11 +961,17 @@ providing evidence that `A` holds, the term `L M` provides evidence that
 converts evidence that `A` holds into evidence that `B` holds.
 {:/}
 
-换句话说，如果知道 `A → B` 和 `A` 同时成立，那么我们可以推出 `B` 成立：
+其中 `N` 是一个类型为 `B` 的项，其包括了一个类型为 `A` 的自由变量 `x`。
+给定一个 `A → B` 成立的证明 `L`，和一个 `A` 成立的证明 `M`，那么 `L M` 是 `B` 成立的证明。
+也就是说，`A → B` 成立的证明是一个函数，将 `A` 成立的证明转换成 `B` 成立的证明。
+
 {::comment}
 Put another way, if we know that `A → B` and `A` both hold,
 then we may conclude that `B` holds:
 {:/}
+
+换句话说，如果知道 `A → B` 和 `A` 同时成立，那么我们可以推出 `B` 成立：
+
 \begin{code}
 →-elim : ∀ {A B : Set}
   → (A → B)
@@ -878,40 +980,39 @@ then we may conclude that `B` holds:
   → B
 →-elim L M = L M
 \end{code}
-在中世纪，这条规则被叫做 _modus ponens_，它与函数应用相对应。
 {::comment}
 In medieval times, this rule was known by the name _modus ponens_.
 It corresponds to function application.
 {:/}
 
-定义一个函数，不管是带名字的定义或是使用 Lambda 抽象，被称为*引入*一个函数，
-使用一个函数被称为*消去*一个函数。
+在中世纪，这条规则被叫做 _modus ponens_，它与函数应用相对应。
+
 {::comment}
 Defining a function, with a named definition or a lambda abstraction,
 is referred to as _introducing_ a function,
 while applying a function is referred to as _eliminating_ the function.
 {:/}
 
-引入后接着消去，得到的还是原来的值：
+定义一个函数，不管是带名字的定义或是使用 Lambda 抽象，被称为*引入*一个函数，
+使用一个函数被称为*消去*一个函数。
+
 {::comment}
 Elimination followed by introduction is the identity:
 {:/}
+
+引入后接着消去，得到的还是原来的值：
+
 \begin{code}
 η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f
 η-→ f = refl
 \end{code}
 
-蕴含比其他的运算符结合得都不紧密。因此 `A ⊎ B → B ⊎ A` 被解析为 `(A ⊎ B) → (B ⊎ A)`。
 {::comment}
 Implication binds less tightly than any other operator. Thus, `A ⊎ B →
 B ⊎ A` parses as `(A ⊎ B) → (B ⊎ A)`.
 {:/}
 
-给定两个类型 `A` 和 `B`，我们将 `A → B` 称为从 `A` 到 `B` 的*函数*空间。
-它有时也被称作以 `B` 为底，`A` 为次数的*幂*。如果类型 `A` 有 `m` 个不同的成员，
-类型 `B` 有 `n` 个不同的成员，那么类型 `A × B` 有 `nᵐ` 个不同的成员。
-这也是它被称为幂的原因之一。例如，考虑有两个成员的 `Bool` 类型，和有三个成员的 `Tri` 类型，
-如之前的定义。那么，`Bool → Tri` 类型有如下的九个成员（三的平方）：
+蕴含比其他的运算符结合得都不紧密。因此 `A ⊎ B → B ⊎ A` 被解析为 `(A ⊎ B) → (B ⊎ A)`。
 
 {::comment}
 Given two types `A` and `B`, we refer to `A → B` as the _function_
@@ -923,16 +1024,25 @@ members, and type `B` has `n` distinct members, then the type
 type `Bool` with two members and a type `Tri` with three members,
 as defined earlier. The the type `Bool → Tri` has nine (that is,
 three squared) members:
+{:/}
+
+给定两个类型 `A` 和 `B`，我们将 `A → B` 称为从 `A` 到 `B` 的*函数*空间。
+它有时也被称作以 `B` 为底，`A` 为次数的*幂*。如果类型 `A` 有 `m` 个不同的成员，
+类型 `B` 有 `n` 个不同的成员，那么类型 `A × B` 有 `nᵐ` 个不同的成员。
+这也是它被称为幂的原因之一。例如，考虑有两个成员的 `Bool` 类型，和有三个成员的 `Tri` 类型，
+如之前的定义。那么，`Bool → Tri` 类型有如下的九个成员（三的平方）：
 
     λ{true → aa; false → aa}  λ{true → aa; false → bb}  λ{true → aa; false → cc}
     λ{true → bb; false → aa}  λ{true → bb; false → bb}  λ{true → bb; false → cc}
     λ{true → cc; false → aa}  λ{true → cc; false → bb}  λ{true → cc; false → cc}
 
-下面的函数枚举了所有类型为 `Bool → Tri` 的参数：
 {::comment}
 For example, the following function enumerates all possible
 arguments of the type `Bool → Tri`:
 {:/}
+
+下面的函数枚举了所有类型为 `Bool → Tri` 的参数：
+
 \begin{code}
 →-count : (Bool → Tri) → ℕ
 →-count f with f true | f false
@@ -947,35 +1057,40 @@ arguments of the type `Bool → Tri`:
 ...          | cc     | cc      =   9
 \end{code}
 
-类型上的幂与数的幂有相似的性质，很多数上成立的关系式也可以在类型上成立。
 {::comment}
 Exponential on types also share a property with exponential on
 numbers in that many of the standard identities for numbers carry
 over to the types.
 {:/}
 
-对应如下的定律：
+类型上的幂与数的幂有相似的性质，很多数上成立的关系式也可以在类型上成立。
+
 {::comment}
 Corresponding to the law
 {:/}
 
+对应如下的定律：
+
     (p ^ n) ^ m  ≡  p ^ (n * m)
 
-我们有如下的同构：
 {::comment}
 we have the isomorphism
 {:/}
 
+我们有如下的同构：
+
     A → (B → C)  ≃  (A × B) → C
 
-两个类型可以被看作给定 `A` 成立的证据和 `B` 成立的证据，返回 `C` 成立的证据。
-这个同构有时也被称作*柯里化*（Currying）。右逆的证明需要外延性：
 {::comment}
 Both types can be viewed as functions that given evidence that `A` holds
 and evidence that `B` holds can return evidence that `C` holds.
 This isomorphism sometimes goes by the name *currying*.
 The proof of the right inverse requires extensionality:
 {:/}
+
+两个类型可以被看作给定 `A` 成立的证据和 `B` 成立的证据，返回 `C` 成立的证据。
+这个同构有时也被称作*柯里化*（Currying）。右逆的证明需要外延性：
+
 \begin{code}
 currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
 currying =
@@ -987,52 +1102,60 @@ currying =
     }
 \end{code}
 
-柯里化告诉我们，如果一个函数有一对参数，我们可以构造一个函数，取第一个参数，返回一个取第二个参数，
-返回最终结果的函数。因此，举例来说，下面表示加法的形式：
 {::comment}
 Currying tells us that instead of a function that takes a pair of arguments,
 we can have a function that takes the first argument and returns a function that
 expects the second argument.  Thus, for instance, our way of writing addition
 {:/}
 
+柯里化告诉我们，如果一个函数有取一个数据对作为参数，
+那么我们可以构造一个函数，取第一个参数，返回一个取第二个参数，返回最终结果的函数。
+因此，举例来说，下面表示加法的形式：
+
     _+_ : ℕ → ℕ → ℕ
 
-和下面的一个带有一对参数的函数是同构的：
 {::comment}
 is isomorphic to a function that accepts a pair of arguments:
 {:/}
 
+和下面的一个带有一个数据对作为参数的函数是同构的：
+
     _+′_ : (ℕ × ℕ) → ℕ
 
-Agda 对柯里化进行了优化，因此 `2 + 3` 是 `_+_ 2 3` 的简写。在一个对有序对进行优化的语言里，
-`2 +′ 3` 可能是 `_+′_ ⟨ 2 , 3 ⟩` 的简写。
 {::comment}
 Agda is optimised for currying, so `2 + 3` abbreviates `_+_ 2 3`.
 In a language optimised for pairing, we would instead take `2 +′ 3` as
 an abbreviation for `_+′_ ⟨ 2 , 3 ⟩`.
 {:/}
 
-对应如下的定律：
+Agda 对柯里化进行了优化，因此 `2 + 3` 是 `_+_ 2 3` 的简写。在一个对有序对进行优化的语言里，
+`2 +′ 3` 可能是 `_+′_ ⟨ 2 , 3 ⟩` 的简写。
+
 {::comment}
 Corresponding to the law
 {:/}
 
+对应如下的定律：
+
     p ^ (n + m) = (p ^ n) * (p ^ m)
 
-我们有如下的同构：
 {::comment}
 we have the isomorphism:
 {:/}
 
+我们有如下的同构：
+
     (A ⊎ B) → C  ≃  (A → C) × (B → C)
 
-命题如果 `A` 成立或者 `B` 成立，那么 `C` 成立，和命题如果 `A` 成立，那么 `C` 成立以及
-如果 `B` 成立，那么 `C` 成立，是一样的。左逆的证明需要外延性：
 {::comment}
 That is, the assertion that if either `A` holds or `B` holds then `C` holds
 is the same as the assertion that if `A` holds then `C` holds and if
 `B` holds then `C` holds.  The proof of the left inverse requires extensionality:
 {:/}
+
+命题如果 `A` 成立或者 `B` 成立，那么 `C` 成立，和命题如果 `A` 成立，那么 `C` 成立以及
+如果 `B` 成立，那么 `C` 成立，是一样的。左逆的证明需要外延性：
+
 \begin{code}
 →-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
 →-distrib-⊎ =
@@ -1044,28 +1167,32 @@ is the same as the assertion that if `A` holds then `C` holds and if
     }
 \end{code}
 
-对应如下的定律：
 {::comment}
 Corresponding to the law
 {:/}
 
+对应如下的定律：
+
     (p * n) ^ m = (p ^ m) * (n ^ m)
 
-我们有如下的同构：
 {::comment}
 we have the isomorphism:
 {:/}
 
+我们有如下的同构：
+
     A → B × C  ≃  (A → B) × (A → C)
 
-命题如果 `A` 成立，那么 `B` 成立和 `C` 成立，和命题如果 `A` 成立，那么 `B` 成立以及
-如果 `A` 成立，那么 `C` 成立，是一样的。左逆的证明需要外延性和积的 `η-×` 规则：
 {::comment}
 That is, the assertion that if `A` holds then `B` holds and `C` holds
 is the same as the assertion that if `A` holds then `B` holds and if
 `A` holds then `C` holds.  The proof of left inverse requires both extensionality
 and the rule `η-×` for products:
 {:/}
+
+命题如果 `A` 成立，那么 `B` 成立和 `C` 成立，和命题如果 `A` 成立，那么 `B` 成立以及
+如果 `A` 成立，那么 `C` 成立，是一样的。左逆的证明需要外延性和积的 `η-×` 规则：
+
 \begin{code}
 →-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
 →-distrib-× =
@@ -1078,16 +1205,19 @@ and the rule `η-×` for products:
 \end{code}
 
 
-## 分配律
 {::comment}
 ## Distribution
 {:/}
 
-在忽略同构的情况下，积对于和满足分配律。验证这条形式的代码和之前的证明相似：
+## 分配律
+
 {::comment}
 Products distribute over sum, up to isomorphism.  The code to validate
 this fact is similar in structure to our previous results:
 {:/}
+
+在忽略同构的情况下，积对于和满足分配律。验证这条形式的代码和之前的证明相似：
+
 \begin{code}
 ×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
 ×-distrib-⊎ =
@@ -1107,10 +1237,12 @@ this fact is similar in structure to our previous results:
     }
 \end{code}
 
-和对于积不满足分配律，但满足嵌入：
 {::comment}
 Sums do not distribute over products up to isomorphism, but it is an embedding:
 {:/}
+
+和对于积不满足分配律，但满足嵌入：
+
 \begin{code}
 ⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C)
 ⊎-distrib-× =
@@ -1127,9 +1259,6 @@ Sums do not distribute over products up to isomorphism, but it is an embedding:
                  }
     }
 \end{code}
-我们在定义 `from` 函数的时候可以有选择。给定的定义中，它将 `⟨ inj₂ z , inj₂ z′ ⟩`
-转换为 `inj₂ z`，但我们也可以返回 `inj₂ z′` 作为嵌入证明的变种。我们在这里只能证明嵌入，
-而不能证明同构，因为 `from` 函数必须丢弃 `z` 或者 `z′` 其中的一个。
 {::comment}
 Note that there is a choice in how we write the `from` function.
 As given, it takes `⟨ inj₂ z , inj₂ z′ ⟩` to `inj₂ z`, but it is
@@ -1138,17 +1267,20 @@ an embedding rather than an isomorphism because the
 `from` function must discard either `z` or `z′` in this case.
 {:/}
 
-在一般的逻辑学方法中，两条分配律都以等价的形式给出，每一边都蕴含了另一边：
+我们在定义 `from` 函数的时候可以有选择。给定的定义中，它将 `⟨ inj₂ z , inj₂ z′ ⟩`
+转换为 `inj₂ z`，但我们也可以返回 `inj₂ z′` 作为嵌入证明的变种。我们在这里只能证明嵌入，
+而不能证明同构，因为 `from` 函数必须丢弃 `z` 或者 `z′` 其中的一个。
+
 {::comment}
 In the usual approach to logic, both of the distribution laws
 are given as equivalences, where each side implies the other:
 {:/}
 
+在一般的逻辑学方法中，两条分配律都以等价的形式给出，每一边都蕴含了另一边：
+
     A × (B ⊎ C) ⇔ (A × B) ⊎ (A × C)
     A ⊎ (B × C) ⇔ (A ⊎ B) × (A ⊎ C)
 
-但当我们考虑提供上述蕴含证明的函数时，第一条对应同构而第二条只能对应嵌入，
-揭示了有些定理比另一个更加的”正确“。
 {::comment}
 But when we consider the functions that provide evidence for these
 implications, then the first corresponds to an isomorphism while the
@@ -1156,29 +1288,32 @@ second only corresponds to an embedding, revealing a sense in which
 one of these laws is "more true" than the other.
 {:/}
 
+但当我们考虑提供上述蕴含证明的函数时，第一条对应同构而第二条只能对应嵌入，
+揭示了有些定理比另一个更加的”正确“。
+
 
-#### 练习 `⊎-weak-×` （推荐）
 {::comment}
 #### Exercise `⊎-weak-×` (recommended)
 {:/}
 
-证明如下性质成立：
+#### 练习 `⊎-weak-×` （推荐）
+
 {::comment}
 Show that the following property holds:
 {:/}
+
+证明如下性质成立：
+
 \begin{code}
 postulate
   ⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
 \end{code}
-这被称为*弱分配律*。给出相对应的分配律，并解释分配律与弱分配律的关系。
 {::comment}
 This is called a _weak distributive law_. Give the corresponding
 distributive law, and explain how it relates to the weak version.
 {:/}
 
-\begin{code}
--- 请将代码写在此处。
-\end{code}
+这被称为*弱分配律*。给出相对应的分配律，并解释分配律与弱分配律的关系。
 
 {::comment}
 \begin{code}
@@ -1186,28 +1321,33 @@ distributive law, and explain how it relates to the weak version.
 \end{code}
 {:/}
 
+\begin{code}
+-- 请将代码写在此处。
+\end{code}
+
+
 
-#### 练习 `⊎×-implies-×⊎`
 {::comment}
 #### Exercise `⊎×-implies-×⊎`
 {:/}
 
-证明合取的析取蕴含了析取的合取：
+#### 练习 `⊎×-implies-×⊎`
+
 {::comment}
 Show that a disjunct of conjuncts implies a conjunct of disjuncts:
 {:/}
+
+证明合取的析取蕴含了析取的合取：
+
 \begin{code}
 postulate
   ⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
 \end{code}
-反命题成立吗？如果成立，给出证明；如果不成立，给出反例。
 {::comment}
 Does the converse hold? If so, prove; if not, give a counterexample.
 {:/}
 
-\begin{code}
--- 请将代码写在此处。
-\end{code}
+反命题成立吗？如果成立，给出证明；如果不成立，给出反例。
 
 {::comment}
 \begin{code}
@@ -1215,15 +1355,22 @@ Does the converse hold? If so, prove; if not, give a counterexample.
 \end{code}
 {:/}
 
-## 标准库
+\begin{code}
+-- 请将代码写在此处。
+\end{code}
+
 {::comment}
 ## Standard library
 {:/}
 
-标准库中可以找到与本章节中相似的定义：
+## 标准库
+
 {::comment}
 Definitions similar to those in this chapter can be found in the standard library:
 {:/}
+
+标准库中可以找到与本章节中相似的定义：
+
 \begin{code}
 import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 import Data.Unit using (⊤; tt)
@@ -1231,11 +1378,6 @@ import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
 import Data.Empty using (⊥; ⊥-elim)
 import Function.Equivalence using (_⇔_)
 \end{code}
-标准库中使用 `_,_` 构造数据对，而我们使用 `⟨_,_⟩`。前者在从数据对构造三元对或者更大的
-元组时更加的方便，允许 `a , b , c` 作为 `(a, (b , c))` 的记法。但它与其他有用的记法相冲突，
-比如说 [Lists][plfa.Lists] 中的 `[_,_]` 记法表示两个元素的列表，或者 [DeBruijn][plfa.DeBruijn]
-章节中的 `Γ , A` 来表示环境的扩展。标准库中的 `_⇔_` 和我们的相似，但使用起来比较不便，
-因为它可以根据任意的相等性定义进行参数化。
 {::comment}
 The standard library constructs pairs with `_,_` whereas we use `⟨_,_⟩`.
 The former makes it convenient to build triples or larger tuples from pairs,
@@ -1249,6 +1391,12 @@ standard library is less convenient, since it is parameterised with
 respect to an arbitrary notion of equivalence.
 {:/}
 
+标准库中使用 `_,_` 构造数据对，而我们使用 `⟨_,_⟩`。前者在从数据对构造三元对或者更大的
+元组时更加的方便，允许 `a , b , c` 作为 `(a, (b , c))` 的记法。但它与其他有用的记法相冲突，
+比如说 [Lists][plfa.Lists] 中的 `[_,_]` 记法表示两个元素的列表，
+或者 [DeBruijn][plfa.DeBruijn] 章节中的 `Γ , A` 来表示环境的扩展。
+标准库中的 `_⇔_` 和我们的相似，但使用起来比较不便，
+因为它可以根据任意的相等性定义进行参数化。
 
 ## Unicode