HoTT學習筆記1：類型論基礎

目錄：類型論驛站寫作計劃

The HoTT Book

===========重要概念對照表============

類型 邏輯 集合 同倫

----------- 命題 -------- 集合 ---------- 空間

-------- 證明 -------- 元素 ---------- 點

--------- 謂詞-------- 集合族 -------- 纖維化

--- 條件式證明 -元素族--------- 截面

----------- ----- -- ---------

-------- ------ 不交並 -------- 余積

-------- ------ 對子集合 ------ 積空間

-------- ----- 函數集合 ------ 函數空間

----- ----不交和 ------- 總空間

----- ----積 -------------截面空間

------------ 等於 --- --路徑空間

1. 類型論和集合論的區別

作為數學的基礎語言之一，同倫類型論是Zermelo-Fraenkel集合論（ZFC）的競爭對手。類型論和集合論的重要區別羅列如下：

• 集合論的基礎有兩個層次：一階邏輯的演繹系統，以及用一階邏輯闡述的特定理論，如ZFC，的公理。類型論本身就是一個演繹系統，不需要在一個超然的結構中闡述。
• 集合論有兩個重要概念：集合與命題；類型論只有一個核心概念：類型。命題也是一種類型（見上表）。證明一個命題就是構造一個類型的對象的過程。
• 類型論里的 是一個判斷（judgment），我們不能證偽它。集合論里的 是一個命題。我們可以證實或證偽它。 一般來說， 是 唯一且確定的類型。而「子集」只是兩個對象 和 之間可能存在的關係。
• 在類型論中，等於關係（equality）是一個類型。例如對於 ，如果類型 有棲居對象（be inhabited），那麼我們稱 和 是命題等同（propositionally equal）的。

此外，在類型論中還有一個判斷/定義等同（judgmental/definitional equality），記為 。例如我們定義類型為 的函數 ，那麼 和 就是定義等同的，在這種情況下我們標記為 。

判斷需要基於假設（assumptions），假設構成了語境（context）。如果類型 表示的是一個命題，我們可以省去它的證明的名稱，如把 寫成 . 但這裡的等於不是判斷等同。判斷等同不能作為假設，也不能被證明。

在類型論中，規則（rules），而不是公理（axioms），是最重要的。我們可以把規則視為棋牌規則，把公理視為初始棋子的布局。

2. 函數類型（function types）

抽象（abstraction）：給定類型為 的表達式 ，其中可能出現 ，我們定義函數如下：

歸約（reduction）（計算規則）：

擴展（expansion）：對於任意一個函數 ，我們都可以做如下抽象：

避免使用乘積類型的一個方式是柯里化（Currying），類型為 的函數可以柯里化為類型為 的函數。例如 可以改寫為 .

3. 宇宙和類型族（universes and families）

宇宙是元素為類型的類型。如果按樸素集合論的想法，我們可以構想出所有宇宙的宇宙 ，這會導致羅素悖論（Russells paradox），為了避免羅素悖論。我們引入了宇宙的層級概念：

Coq 中我們有時候會見到 ，但這其實只是 的縮寫，這種縮寫法被稱為典型歧義（typical ambiguity）。此外，我們還假定宇宙是累積的（cumulative）： .

如果要描寫一組依賴類型 的類型，我們可以使用函數 ，我們把這樣的函數稱為類型族（或依賴類型，dependent types）。

4. 依賴函數類型（dependent function types, 類型）

依賴函數類型的元素是值域類型依定義域元素的變化而變化的函數。由於也可以將其視為類型的笛卡兒積（Cartesian product），所以一般我們簡稱為 類型。

給定類型 和類型族 ，我們可以構建依賴函數 。其他的標記方式有：

如果 是一個常類型族，那麼依賴函數類型就是普通的函數類型：

Variables A B:Type.Check (forall (a:A), B).A -> B : Type

1.5 乘積類型（product types）

如果 ，那麼我們定義 ，稱之為笛卡兒積。 的元素是對子 。我們再定義一個零元乘積類型（nullary product type），稱其為單位類型（unit type） . 單位類型的元素是一個特殊元素 。

類型論中類型引入的通用模式：

1. 形成法則（formation rules）：類型如何形成
2. 構子，構造法則（construction rules）：類型的元素如何構造
3. 消除子，消除法則（elimination rules）：如何使用類型的元素
4. 計演算法則， 歸約（computation rules, -reduction）：消除子如何作用於構造子的
5. （非必要的）唯一性原則， 擴張（uniqueness principle, -expansion）：以該類型為定義域或值域的映射的唯一性；如果唯一性原則不作為判斷等於法則，仍可以作為命題等於關係而得到證明，這就是命題唯一性原則。

乘積類型的投射函數（projection functions）的類型：

投射函數的定義：

使用遞歸子（recursor）來定義投射函數：

單位類型的遞歸子：

對遞歸子的定義加以推廣從而可以定義作用於乘積類型的依賴函數（實質上是柯里化）：

設 ，我們通過 來定義 ：

我們可以藉助這個定義來證明命題唯一性原則（ 中的每一個元素等同於一個對子）：

對於任何一個 ，我們都有一個自反元素 . 藉助這個自反元素，我們可以定義：

可以定義依賴函數的能力，意味著要想證明一個乘積里所有元素都擁有一個特徵，只需證明其典型元素（有序對子）擁有此特徵即可。針對全局應用以上原則，可以得到對於乘積類型的歸納（induction）函數。設 ，我們有

我們可以認為定義在對子上的依賴函數是通過笛卡爾乘積上的歸納原則（induction principle）獲取的。遞歸子實際上是 為常量時的一種特殊的歸納。歸納描述了乘積類型中元素的使用方法，所以也稱為依賴消除子（dependent eliminator），遞歸則被稱為無依賴消除子（non-dependent eliminator）。

1.6 依賴對子類型（dependent pair types, -types）

依賴對子類型是對乘積類型的推廣。在集合論里它對應著不交和（見開頭的概念對照表）。對於類型 和類型族 ，我們可以用以下方式標記依賴對子類型：

對於 ， . 若 不在 中出現，那麼依賴對子類型就坍塌成無依賴對子類型，即普通的乘積類型。

依賴對子類型的第一和第二投射函數分別定義為：

1.7 陪積類型（coproduct type）

對於 ，我們引入 作為它們的陪積類型。陪積類型對應著集合論里的不交並（disjoint union）。我們同時也引入一個零元的情況：空類型 .

構建 的元素有兩種方法，一是通過左單射（left injection） 得到 ，一是通過右單射（right injection） 得到 。空類型無從構建元素。

@inl : forall A B : Type, A -> A + B@inr : forall A B : Type, B -> A + B

要想構建一個定義域類型為 的無依賴函數 ，我們需要兩個函數： ，然後再將 定義為：

因此，函數 是通過分類分析（case analysis）來定義的。我們定義陪積類型的遞歸子如下：

的遞歸子是 （無需給出定義等式，因為空類型是沒有元素的），邏輯上對應著爆炸原理（ex falso quodlibet）。

1.8 布爾值的類型（The type of booleans）

布爾值的類型 只有兩個元素 。我們本可以通過陪積類型和單位類型來定義它： 。

和經典數學不同的是，布爾值不被視為真值或命題。

1.9 自然數（The natural numbers）

自然數類型 是無限類型（infinite types）的典型例子。通過自然數，我們可以遞歸地定義函數，並採用歸納法來進行證明（在這裡遞歸和歸納含義相近）。若要構建一個無依賴函數 ，我們只需要提供一個起點（starting point） 以及一個「下一步」（next step）函數 ：

我們稱 是通過原始遞歸（primitive recursion）來定義的。例如，我們可以用原始遞歸來定義函數 ：

1.10 模式匹配和遞歸（pattern matching and recursion）

對於陪積，我們可以用兩種方式定義函數 。第一種方式是使用遞歸子：

第二種方式是採用等式定義法：

從後者到前者，我們可以使用 抽象便捷地定義函數：

如果我們在自然數上遞歸，可以使用下列方式定義函數：

其中 , .

採用這種方式來遞歸地定義函數，或推廣至通過歸納來定義依賴函數，被稱為模式匹配（pattern matching）定義法。

1.11 命題作為類型（propositions as types）

從「命題作為類型」的角度來看，證明不再僅僅是數學推理的過程，證明本身也是一個數學對象。下面是一些用自然語言描述的命題及其類型論對應表示：

• 真：
• 假：
• 且 ：
• 或 ：
• 若 則 ：
• 當且僅當 ：
• 非 ：

最自然的類型論中的「命題作為類型」邏輯是構建主義/直覺主義邏輯，它不包括排中律。但類型論提供了「公設/公理自由」（axiomatic freedom），雖然在自然的直覺主義邏輯里沒有排中律，但這並不代表它「不承認」排中律。在適當的情境下我們仍然可以把排中律作為公理加入到邏輯系統里。

上面的命題-類型對應只考慮了命題邏輯。為了探討謂詞邏輯里的命題和類型的對應關係，我們有：

• 對於所有 ， 成立：
• 存在一個 使得 成立：

此外，藉助類型論中的宇宙概念，我們還可以表達高階邏輯：

但值得注意的是，雖然我們有 ，即 和 是邏輯等同（logically equivalent）的。但它們的功能差別很大，所以兩者並不是「類型等同」的。

反過來看，類型也可以視為命題，通過提供一個元素作為證明。這樣的命題有時被讀為「 是被棲居的（ is inhabited）」。

1.12 等同類型（Identity type）

根據類型論，命題「兩個同類型的元素 是等同（equal）的」必須對應著某個類型。這就是等同類型（equality/identity types）。等同類型是依賴於 的兩個副本的類型族。

而 就是表達上述命題的類型。這種等同關係是「命題等同」，而非之前討論的「判斷等同」。

除此以外，我們還可以將 的證據（witness）視為空間 上 和 之間的路徑（path）。兩點之間的路徑不止一條，所以兩個元素的等同也可以有不止一個證據。

等同類型是同倫類型論中最難理解的類型。因此這份筆記里僅僅對其做一個簡單的介紹，後續我會專門記錄一篇關於等同類型的筆記。

以上就是同倫類型論大致的類型論基礎，它和 Coq 的類型論還是有著細微的差別的，例如在同倫類型論中，沒有專門的命題宇宙 。

目錄：類型論驛站寫作計劃