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 using (ℕ)
open import Function using (_∘_)
open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality; _⇔_)
open plfa.part1.Isomorphism.≃-Reasoning

合取即是积

给定两个命题 A 和 B，其合取 A × B 成立当 A 成立和 B 成立。 我们用一个合适的数据类型将这样的概念形式化：

record _×_ (A B : Set) : Set where
  constructor ⟨_,_⟩
  field
    proj₁ : A
    proj₂ : B
open _×_

A × B 成立的证明由 ⟨ M , N ⟩ 的形式表现，其中 M 是 A 成立的证明， N 是 B 成立的证明。

记录构造 record { proj₁ = M ; proj₂ = N } 对应了项 ⟨ M , N ⟩， 其中 M 是类型为 A 的项，N 是类型为 B 的项。 构造子声明（constructor）让我们可以用 ⟨ M , N ⟩ 来代替完整的记录构造。

给定 A × B 成立的证明，我们可以使用投影 proj₁ 和 proj₂ 分别得出 A 成立和 B 成立。

如果 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
η-× w = refl

对于记录类型来说，η-相等性由定义成立。 在证明 η-× 时，我们不需要对于 w 进行模式匹配，而得出 η-相等性成立。

我们设置合取的优先级，使它与除了析取之外结合的都不紧密：

infixr 2 _×_

因此，m ≤ n × n ≤ p 解析为 (m ≤ n) × (n ≤ p)。

或者，我们可以将合取定义为数据类型，其投影则由以使用模式匹配定义的函数得来。

data _×′_ (A B : Set) : Set where

  ⟨_,_⟩′ :
      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

记录类型 _×_ 和数据类型 _×′_ 很相似。 两者的差异之一在于，对于记录类型 η-相等性由定义可得； 而对于数据类型，我们必须使用模式匹配来得出：

η-×′ : ∀ {A B : Set} (w : A ×′ B) → ⟨ proj₁′ w , proj₂′ w ⟩′ ≡ w
η-×′ ⟨ x , y ⟩′ = refl

左手边的模式匹配时必须的，因为用 ⟨ x , y ⟩′ 来代替 w 使得命题相等性的两边都化简至相同的项。 由定义得出的 η-相等性更加便于使用，因此在只有一个构造子时， 我们更倾向于使用记录类型而不是数据类型。

给定两个类型 A 和 B，我们将 A × B 称为 A 与 B 的积。 在集合论中它也被称作笛卡尔积（Cartesian Product），在计算机科学中它对应记录（Record）类型。 如果类型 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 函数亦是如此（忽略命名）。

×-comm : ∀ {A B : Set} → A × B ≃ B × A
×-comm =
  record
    { to       =  λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ }
    ; from     =  λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ }
    ; from∘to  =  λ{ w → refl }
    ; to∘from  =  λ{ w → 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 = λ{ w → refl }
    ; to∘from = λ{ w → 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) 同构。

-- 请将代码写在此处

真即是单元类型

恒真 ⊤ 恒成立。我们将这个概念用空记录类型来形式化：

record ⊤ : Set where
  constructor tt

⊤ 成立的证明由 tt 的形式构成。

记录构造 record {} 对应了项 tt。构造子声明使得我们可以用 tt 来表示。

恒真有引入规则，但没有消去规则。给定一个 ⊤ 成立的证明，我们不能得出任何有趣的结论。 因为恒真恒成立，知道恒真成立不会给我们带来新的知识。

η-× 的 零元形式是 η-⊤，其断言了任何 ⊤ 类型的值一定等于 tt。 在证明 η-⊤ 时，我们不需要对于 w 进行模式匹配：

η-⊤ : ∀ (w : ⊤) → tt ≡ w
η-⊤ w = refl

Agda 知道任何类型为 ⊤ 的值必须为 tt，所以认识我们需要一个类型为 ⊤ 的值的时候， 我们可以让 Agda 来自行推断：

truth : ⊤
truth = _

或者，我们可以将恒真定义为数据类型：

data ⊤′ : Set where

  tt′ :
    --
    ⊤′

与积类型一样，记录类型的 ⊤ 与数据类型的 ⊤′ 没有太大差异，但是 η-相等性对于记录类型由定义可得。

η-⊤′ : ∀ (w : ⊤′) → tt′ ≡ w
η-⊤′ tt′ = refl

左手边的模式匹配时必须的，因为用 tt′ 来代替 w 使得命题相等性的两边都化简至相同的项。 与积类型的情况一样，由定义得出的 η-相等性更加便于使用，因此在只有一个构造子时， 我们更倾向于使用记录类型而不是数据类型。

我们将 ⊤ 称为单元（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 没有任何可能的值，因此等式显然成立。

我们也可以在嵌套模式中使用 () 。 例如，⟨ () , tt ⟩ 是 ⊥ × ⊤ 的模式.

我们将 ⊥ 成为空（Empty）类型。实际上，⊥ 类型没有成员。 例如，下面的函数枚举了所有 ⊥ 类型的参数：

⊥-count : ⊥ → ℕ
⊥-count ()

同样，荒谬模式告诉我们没有值可以来匹配类型 ⊥。

对于数来说，0 是加法的幺元。对应地，空是和的幺元（在同构意义下）。

练习 ⊥-identityˡ （推荐）

证明空在同构意义下是和的左幺元。

-- 请将代码写在此处

练习 ⊥-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 → 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 = λ{ _ → 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 → refl }
    ; 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₂ w ⟩ 转换为 inj₂ z，但我们也可以返回 inj₂ w 作为嵌入证明的变种。我们在这里只能证明嵌入， 而不能证明同构，因为 from 函数必须丢弃 z 或者 w 其中的一个。

在一般的逻辑学方法中，两条分配律都以等价的形式给出，每一边都蕴涵了另一边：

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  左右双箭头 (\<=>)

  1. 此段内容由 Propositions as Types（命题即类型）改编而来， 作者：Philip Wadler，发表于 《ACM 通讯》，2015 年 9 月↩︎