Connectives: 合取、析取与蕴涵
module plfa.part1.Connectives where
本章节介绍基础的逻辑运算符。我们使用逻辑运算符与数据类型之间的对应关系， 即命题即类型（Propositions as Types）原理。
- 合取（Conjunction）即是积（Product）
- 析取（Disjunction）即是和（Sum）
- 真（True）即是单元类型（Unit Type）
- 假（False）即是空类型（Empty Type）
- 蕴涵（Implication）即是函数空间（Function Space）
导入
import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl) open Eq.≡-Reasoning open import Data.Nat.Base using (ℕ) open import Function.Base using (_∘_) open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality; _⇔_) open plfa.part1.Isomorphism.≃-Reasoning
合取即是积
给定两个命题 A 和 B，其合取 A × B 成立当 A 成立和 B 成立。 我们用一个合适的数据类型将这样的概念形式化：
data _×_ (A B : Set) : Set where ⟨_,_⟩ : A → B ----- → A × B
A × B 成立的证明由 ⟨ M , N ⟩ 的形式表现，其中 M 是 A 成立的证明， N 是 B 成立的证明。
给定 A × B 成立的证明，我们可以得出 A 成立和 B 成立。
proj₁ : ∀ {A B : Set} → A × B ----- → A proj₁ ⟨ x , y ⟩ = x proj₂ : ∀ {A B : Set} → A × B ----- → B proj₂ ⟨ x , y ⟩ = y
如果 L 是 A × B 成立的证据, 那么 proj₁ L 是 A 成立的证据， proj₂ L 是 B 成立的证据。
当 ⟨_,_⟩ 在等式右手边的项中出现的时候，我们将其称作构造子（Constructor）， 当它出现在等式左边时，我们将其称作解构子（Destructor）。我们亦可将 proj₁ 和 proj₂ 称作解构子，因为它们起到相似的效果。
其他的术语将 ⟨_,_⟩ 称作引入（Introduce）合取，将 proj₁ 和 proj₂ 称作消去（Eliminate）合取。 前者亦记作 ×-I，后者 ×-E₁ 和 ×-E₂。如果我们从上到下来阅读这些规则，引入和消去 正如其名字所说的那样：第一条引入一个运算符，所以运算符出现在结论中，而不是假设中； 第二条消去一个带有运算符的式子，而运算符出现在假设中，而不是结论中。引入规则描述了 运算符在什么情况下成立——即怎么样定义一个运算符。消去规则描述了运算符成立时，可以得出 什么样的结论——即怎么样使用一个运算符。1
在这样的情况下，先使用解构子，再使用构造子将结果重组，得到还是原来的积。
η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w η-× ⟨ x , y ⟩ = refl
左手边的模式匹配是必要的。用 ⟨ x , y ⟩ 来替换 w 让等式的两边可以化简成相同的项。
我们设置合取的优先级，使它与除了析取之外结合的都不紧密：
infixr 2 _×_
因此，m ≤ n × n ≤ p 解析为 (m ≤ n) × (n ≤ p)。
Alternatively, we can declare conjunction as a record type:
record _×′_ (A B : Set) : Set where constructor ⟨_,_⟩′ field proj₁′ : A proj₂′ : B open _×′_
The record construction record { proj₁′ = M ; proj₂′ = N } corresponds to the term ⟨ M , N ⟩ where M is a term of type A and N is a term of type B. The constructor declaration allows us to write ⟨ M , N ⟩′ in place of the record construction.
The data type _×_ and the record type _×′_ behave similarly. One difference is that for data types we have to prove η-equality, but for record types, η-equality holds by definition. While proving η-×′, we do not have to pattern match on w to know that η-equality holds:
η-×′ : ∀ {A B : Set} (w : A ×′ B) → ⟨ proj₁′ w , proj₂′ w ⟩′ ≡ w η-×′ w = refl
It can be very convenient to have η-equality definitionally, and so the standard library defines _×_ as a record type. We use the definition from the standard library in later chapters.
给定两个类型 A 和 B，我们将 A × B 称为 A 与 B 的积。 在集合论中它也被称作笛卡尔积（Cartesian Product），在计算机科学中它对应记录类型。 如果类型 A 有 m 个不同的成员，类型 B 有 n 个不同的成员， 那么类型 A × B 有 m * n 个不同的成员。这也是它被称为积的原因之一。 例如，考虑有两个成员的 Bool 类型，和有三个成员的 Tri 类型：
data Bool : Set where true : Bool false : Bool data Tri : Set where aa : Tri bb : Tri cc : Tri
那么，Bool × Tri 类型有如下的六个成员：
⟨ true , aa ⟩ ⟨ true , bb ⟩ ⟨ true , cc ⟩
⟨ false , aa ⟩ ⟨ false , bb ⟩ ⟨ false , cc ⟩下面的函数枚举了所有类型为 Bool × Tri 的参数：
×-count : Bool × Tri → ℕ ×-count ⟨ true , aa ⟩ = 1 ×-count ⟨ true , bb ⟩ = 2 ×-count ⟨ true , cc ⟩ = 3 ×-count ⟨ false , aa ⟩ = 4 ×-count ⟨ false , bb ⟩ = 5 ×-count ⟨ false , cc ⟩ = 6
类型上的积与数的积有相似的性质——它们满足交换律和结合律。 更确切地说，积在在同构意义下满足交换律和结合率。
对于交换律，to 函数将有序对交换，将 ⟨ x , y ⟩ 变为 ⟨ y , x ⟩，from 函数亦是如此（忽略命名）。 在 from∘to 和 to∘from 中正确地实例化要匹配的模式是很重要的。 使用 λ w → refl 作为 from∘to 的定义是不可行的，to∘from 同理。
×-comm : ∀ {A B : Set} → A × B ≃ B × A ×-comm = record { to = λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ } ; from = λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ } ; from∘to = λ{ ⟨ x , y ⟩ → refl } ; to∘from = λ{ ⟨ y , x ⟩ → refl } }
满足交换律和在同构意义下满足交换律是不一样的。比较下列两个命题：
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 ⟩。
对于结合律来说，to 函数将两个有序对进行重组：将 ⟨ ⟨ x , y ⟩ , z ⟩ 转换为 ⟨ x , ⟨ y , z ⟩ ⟩， from 函数则为其逆。同样，左逆和右逆的证明需要在一个合适的模式来匹配，从而可以直接化简：
×-assoc : ∀ {A B C : Set} → (A × B) × C ≃ A × (B × C) ×-assoc = record { to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → ⟨ x , ⟨ y , z ⟩ ⟩ } ; from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → ⟨ ⟨ x , y ⟩ , z ⟩ } ; from∘to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → refl } ; to∘from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → refl } }
满足结合律和在同构意义下满足结合律是不一样的。比较下列两个命题：
(m * n) * p ≡ m * (n * p)
(A × B) × C ≃ A × (B × C)举个例子，(ℕ × Bool) × Tri 与 ℕ × (Bool × Tri) 不同，但是两个类型之间 存在同构。例如 ⟨ ⟨ 1 , true ⟩ , aa ⟩，一个前者的成员，与 ⟨ 1 , ⟨ true , aa ⟩ ⟩， 一个后者的成员，相对应。
练习 ⇔≃×（实践）
证明之前定义的 A ⇔ B 与 (A → B) × (B → A) 同构。
-- 请将代码写在此处
真即是单元类型
恒真 ⊤ 恒成立。我们将这个概念用合适的数据类型来形式化：
data ⊤ : Set where tt : -- ⊤
⊤ 成立的证明由 tt 的形式构成。
恒真有引入规则，但没有消去规则。给定一个 ⊤ 成立的证明，我们不能得出任何有趣的结论。 因为恒真恒成立，知道恒真成立不会给我们带来新的知识。
η-× 的 零元形式是 η-⊤，其断言了任何 ⊤ 类型的值一定等于 tt：
η-⊤ : ∀ (w : ⊤) → tt ≡ w η-⊤ tt = refl
左手边的模式匹配是必要的。将 w 替换为 tt 让等式两边可以化简为相同的值。
record ⊤′ : Set where constructor tt′
The record construction record {} corresponds to the term tt. The constructor declaration allows us to write tt′.
⊤ and the record type ⊤′ behave similarly, but η-equality holds by definition for the record type. While proving η-⊤′, we do not have to pattern match on w—Agda knows it is equal to tt′:η-⊤′ : ∀ (w : ⊤′) → tt′ ≡ w η-⊤′ w = reflAgda knows that any value of type
⊤′ must be tt′, so any time we need a value of type ⊤′, we can tell Agda to figure it out:truth′ : ⊤′ truth′ = _
我们将 ⊤ 称为单元（Unit Type）类型。实际上，⊤ 类型只有一个成员 tt。 例如，下面的函数枚举了所有 ⊤ 类型的参数：
⊤-count : ⊤ → ℕ ⊤-count tt = 1
对于数来说，1 是乘法的幺元。对应地，单元是积的幺元（在同构意义下）。对于左幺元来说， to 函数将 ⟨ tt , x ⟩ 转换成 x， from 函数则是其反函数。左逆的证明需要 匹配一个合适的模式来化简：
⊤-identityˡ : ∀ {A : Set} → ⊤ × A ≃ A ⊤-identityˡ = record { to = λ{ ⟨ tt , x ⟩ → x } ; from = λ{ x → ⟨ tt , x ⟩ } ; from∘to = λ{ ⟨ tt , x ⟩ → refl } ; to∘from = λ{ x → refl } }
幺元和在同构意义下的幺元是不一样的。比较下列两个命题：
1 * m ≡ m
⊤ × A ≃ A在第一种情况下，我们可能有 m 是 2，那么 1 * m 和 m 都为 2。 在第二种情况下，我们可能有 A 是 Bool，但是 ⊤ × Bool 和 Bool 是不同的。 例如：⟨ tt , true ⟩ 是前者的成员，其对应后者的成员 true。
右幺元可以由积的交换律得来：
⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A ⊤-identityʳ {A} = ≃-begin (A × ⊤) ≃⟨ ×-comm ⟩ (⊤ × A) ≃⟨ ⊤-identityˡ ⟩ A ≃-∎
我们在此使用了同构链，与等式链相似。
析取即是和
给定两个命题 A 和 B，析取 A ⊎ B 在 A 成立或者 B 成立时成立。 我们将这个概念用合适的归纳类型来形式化：
data _⊎_ (A B : Set) : Set where inj₁ : A ----- → A ⊎ B inj₂ : B ----- → A ⊎ B
A ⊎ B 成立的证明有两个形式： inj₁ M，其中 M 是 A 成立的证明，或者 inj₂ N，其中 N 是 B 成立的证明。
给定 A → C 和 B → C 成立的证明，那么给定一个 A ⊎ B 的证明，我们可以得出 C 成立：
case-⊎ : ∀ {A B C : Set} → (A → C) → (B → C) → A ⊎ B ----------- → C case-⊎ f g (inj₁ x) = f x case-⊎ f g (inj₂ y) = g y
对 inj₁ 和 inj₂ 进行模式匹配，是我们使用析取成立的证明的常见方法。
当 inj₁ 和 inj₂ 在等式右手边出现的时候，我们将其称作构造子， 当它出现在等式左边时，我们将其称作解构子。我们亦可将 case-⊎ 称作解构子，因为它们起到相似的效果。其他术语将 inj₁ 和 inj₂ 称为引入析取， 将 case-⊎ 称为消去析取。前者亦被称为 ⊎-I₁ 和 ⊎-I₂，后者 ⊎-E。
对每个构造子使用解构子得到的是原来的值：
η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → case-⊎ inj₁ inj₂ w ≡ w η-⊎ (inj₁ x) = refl η-⊎ (inj₂ y) = refl
更普遍地来说，我们亦可对于析取使用一个任意的函数：
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
左手边的模式匹配是必要的。用 inj₁ x 来替换 w 让等式的两边可以化简成相同的项， inj₂ y 同理。
我们设置析取的优先级，使它与任何已经定义的运算符都结合的不紧密：
infixr 1 _⊎_
因此 A × C ⊎ B × C 解析为 (A × C) ⊎ (B × C)。
给定两个类型 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 的参数：
⊎-count : Bool ⊎ Tri → ℕ ⊎-count (inj₁ true) = 1 ⊎-count (inj₁ false) = 2 ⊎-count (inj₂ aa) = 3 ⊎-count (inj₂ bb) = 4 ⊎-count (inj₂ cc) = 5
类型上的和与数的和有相似的性质——它们满足交换律和结合律。 更确切地说，和在在同构意义下是交换和结合的。
练习 ⊎-comm （推荐）
证明和类型在同构意义下满足交换律。
-- 请将代码写在此处
练习 ⊎-assoc（实践）
证明和类型在同构意义下满足结合律。
-- 请将代码写在此处
假即是空类型
恒假 ⊥ 从不成立。我们将这个概念用合适的归纳类型来形式化：
data ⊥ : Set where -- 没有语句！
没有 ⊥ 成立的证明。
与 ⊤ 相对偶，⊥ 没有引入规则，但是有消去规则。因为恒假从不成立， 如果它一旦成立，我们就进入了矛盾之中。给定 ⊥ 成立的证明，我们可以得出任何结论！ 这是逻辑学的基本原理，又由中世纪的拉丁文词组 ex falso 为名。小孩子也由诸如 「如果猪有翅膀，那我就是示巴女王」的词组中知晓。我们如下将它形式化：
⊥-elim : ∀ {A : Set} → ⊥ -- → A ⊥-elim ()
这是我们第一次使用荒谬模式（Absurd Pattern） ()。在这里，因为 ⊥ 是一个没有成员的类型，我们用 () 模式来指明这里不可能匹配任何这个类型的值。
case-⊎ 的零元形式是 ⊥-elim。类比的来说，它应该叫做 case-⊥， 但是我们在此使用标准库中使用的名字。
uniq-⊎ 的零元形式是 uniq-⊥，其断言了 ⊥-elim 和任何取 ⊥ 的函数是等价的。
uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w uniq-⊥ h ()
使用荒谬模式断言了 w 没有任何可能的值，因此等式显然成立。
我们将 ⊥ 成为空（Empty）类型。实际上，⊥ 类型没有成员。 例如，下面的函数枚举了所有 ⊥ 类型的参数：
⊥-count : ⊥ → ℕ ⊥-count ()
同样，荒谬模式告诉我们没有值可以来匹配类型 ⊥。
对于数来说，0 是加法的幺元。对应地，空是和的幺元（在同构意义下）。
练习 ⊥-identityˡ （推荐）
证明空在同构意义下是和的左幺元。
-- 请将代码写在此处
Exercise ⊥-identityʳ (practice)
练习 ⊥-identityʳ（实践）
证明空在同构意义下是和的右幺元。
-- 请将代码写在此处
蕴涵即是函数
给定两个命题 A 和 B，其蕴涵 A → B 在任何 A 成立的时候，B 也成立时成立。 我们用函数类型来形式化蕴涵，如本书中通篇出现的那样。
A → B 成立的证据由下面的形式组成：
λ (x : A) → N其中 N 是一个类型为 B 的项，其包括了一个类型为 A 的自由变量 x。 给定一个 A → B 成立的证明 L，和一个 A 成立的证明 M，那么 L M 是 B 成立的证明。 也就是说，A → B 成立的证明是一个函数，将 A 成立的证明转换成 B 成立的证明。
换句话说，如果知道 A → B 和 A 同时成立，那么我们可以推出 B 成立：
→-elim : ∀ {A B : Set} → (A → B) → A ------- → B →-elim L M = L M
在中世纪，这条规则被叫做 modus ponens，它与函数应用相对应。
定义一个函数，不管是带名字的定义或是使用 Lambda 抽象，被称为引入一个函数， 使用一个函数被称为消去一个函数。
引入后接着消去，得到的还是原来的值：
η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f η-→ f = refl
蕴涵比其他的运算符结合得都不紧密。因此 A ⊎ B → B ⊎ A 被解析为 (A ⊎ B) → (B ⊎ A)。
给定两个类型 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 的参数：
→-count : (Bool → Tri) → ℕ →-count f with f true | f false ... | aa | aa = 1 ... | aa | bb = 2 ... | aa | cc = 3 ... | bb | aa = 4 ... | bb | bb = 5 ... | bb | cc = 6 ... | cc | aa = 7 ... | cc | bb = 8 ... | cc | cc = 9
类型上的幂与数的幂有相似的性质，很多数上成立的关系式也可以在类型上成立。
对应如下的定律：
(p ^ n) ^ m ≡ p ^ (n * m)我们有如下的同构：
A → (B → C) ≃ (A × B) → C两个类型可以被看作给定 A 成立的证据和 B 成立的证据，返回 C 成立的证据。 这个同构有时也被称作柯里化（Currying）。右逆的证明需要外延性：
currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C) currying = record { to = λ{ f → λ{ ⟨ x , y ⟩ → f x y }} ; from = λ{ g → λ{ x → λ{ y → g ⟨ x , y ⟩ }}} ; from∘to = λ{ f → refl } ; to∘from = λ{ g → extensionality λ{ ⟨ x , y ⟩ → refl }} }
柯里化告诉我们，如果一个函数有取一个数据对作为参数， 那么我们可以构造一个函数，取第一个参数，返回一个取第二个参数，返回最终结果的函数。 因此，举例来说，下面表示加法的形式：
_+_ : ℕ → ℕ → ℕ和下面的一个带有一个数据对作为参数的函数是同构的：
_+′_ : (ℕ × ℕ) → ℕAgda 对柯里化进行了优化，因此 2 + 3 是 _+_ 2 3 的简写。在一个对有序对进行优化的语言里， 2 +′ 3 可能是 _+′_ ⟨ 2 , 3 ⟩ 的简写。
对应如下的定律：
p ^ (n + m) = (p ^ n) * (p ^ m)我们有如下的同构：
(A ⊎ B) → C ≃ (A → C) × (B → C)命题如果 A 成立或者 B 成立，那么 C 成立，和命题如果 A 成立，那么 C 成立以及 如果 B 成立，那么 C 成立，是一样的。左逆的证明需要外延性：
→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C)) →-distrib-⊎ = record { to = λ{ f → ⟨ f ∘ inj₁ , f ∘ inj₂ ⟩ } ; from = λ{ ⟨ g , h ⟩ → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } } ; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } } ; to∘from = λ{ ⟨ g , h ⟩ → refl } }
对应如下的定律：
(p * n) ^ m = (p ^ m) * (n ^ m)我们有如下的同构：
A → B × C ≃ (A → B) × (A → C)命题如果 A 成立，那么 B 成立和 C 成立，和命题如果 A 成立，那么 B 成立以及 如果 A 成立，那么 C 成立，是一样的。左逆的证明需要外延性和积的 η-× 规则：
→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C) →-distrib-× = record { to = λ{ f → ⟨ proj₁ ∘ f , proj₂ ∘ f ⟩ } ; from = λ{ ⟨ g , h ⟩ → λ x → ⟨ g x , h x ⟩ } ; from∘to = λ{ f → extensionality λ{ x → η-× (f x) } } ; to∘from = λ{ ⟨ g , h ⟩ → refl } }
分配律
在同构意义下，积对于和满足分配律。验证这条形式的代码和之前的证明相似：
×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C) ×-distrib-⊎ = record { to = λ{ ⟨ inj₁ x , z ⟩ → (inj₁ ⟨ x , z ⟩) ; ⟨ inj₂ y , z ⟩ → (inj₂ ⟨ y , z ⟩) } ; from = λ{ (inj₁ ⟨ x , z ⟩) → ⟨ inj₁ x , z ⟩ ; (inj₂ ⟨ y , z ⟩) → ⟨ inj₂ y , z ⟩ } ; from∘to = λ{ ⟨ inj₁ x , z ⟩ → refl ; ⟨ inj₂ y , z ⟩ → refl } ; to∘from = λ{ (inj₁ ⟨ x , z ⟩) → refl ; (inj₂ ⟨ y , z ⟩) → refl } }
和对于积不满足分配律，但满足嵌入：
⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C) ⊎-distrib-× = record { to = λ{ (inj₁ ⟨ x , y ⟩) → ⟨ inj₁ x , inj₁ y ⟩ ; (inj₂ z) → ⟨ inj₂ z , inj₂ z ⟩ } ; from = λ{ ⟨ inj₁ x , inj₁ y ⟩ → (inj₁ ⟨ x , y ⟩) ; ⟨ inj₁ x , inj₂ z ⟩ → (inj₂ z) ; ⟨ inj₂ z , _ ⟩ → (inj₂ z) } ; from∘to = λ{ (inj₁ ⟨ x , y ⟩) → refl ; (inj₂ z) → refl } }
我们在定义 from 函数的时候可以有选择。给定的定义中，它将 ⟨ inj₂ z , inj₂ z′ ⟩ 转换为 inj₂ z，但我们也可以返回 inj₂ z′ 作为嵌入证明的变种。我们在这里只能证明嵌入， 而不能证明同构，因为 from 函数必须丢弃 z 或者 z′ 其中的一个。
在一般的逻辑学方法中，两条分配律都以等价的形式给出，每一边都蕴涵了另一边：
A × (B ⊎ C) ⇔ (A × B) ⊎ (A × C)
A ⊎ (B × C) ⇔ (A ⊎ B) × (A ⊎ C)但当我们考虑提供上述蕴涵证明的函数时，第一条对应同构而第二条只能对应嵌入， 揭示了有些定理比另一个更加的「正确」。
练习 ⊎-weak-× （推荐）
证明如下性质成立：
postulate ⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
这被称为弱分配律（Weak Distributive Law）。给出相对应的分配律，并解释分配律与弱分配律的关系。
-- 请将代码写在此处
练习 ⊎×-implies-×⊎（实践）
证明合取的析取蕴涵了析取的合取：
postulate ⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
反命题成立吗？如果成立，给出证明；如果不成立，给出反例。
-- 请将代码写在此处
标准库
标准库中可以找到与本章节中相似的定义：
import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩) import Data.Unit using (⊤; tt) import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎) import Data.Empty using (⊥; ⊥-elim) import Function.Bundles using (_⇔_)
标准库中使用 _,_ 构造数据对，而我们使用 ⟨_,_⟩。前者在从数据对构造三元对或者更大的 元组时更加的方便，允许 a , b , c 作为 (a, (b , c)) 的记法。但它与其他有用的记法相冲突， 比如说 Lists 中的 [_,_] 记法表示两个元素的列表， 或者 DeBruijn 章节中的 Γ , A 来表示环境的扩展。 标准库中的 _⇔_ 和我们的相似，但使用起来比较不便， 因为它可以根据任意的相等性定义进行参数化。
Unicode
本章节使用下列 Unicode：
× U+00D7 乘法符号 (\x)
⊎ U+228E 多重集并集 (\u+)
⊤ U+22A4 向下图钉 (\top)
⊥ U+22A5 向上图钉 (\bot)
η U+03B7 希腊小写字母 ETA (\eta)
₁ U+2081 下标 1 (\_1)
₂ U+2082 下标 2 (\_2)
⇔ U+21D4 左右双箭头 (\<=>)此段内容由 Propositions as Types（命题即类型）改编而来， 作者：Philip Wadler，发表于 《ACM 通讯》，2015 年 9 月↩︎