類型論

類型論，數學、邏輯和電腦科學以下的一個分支，是研究不同類型系統及其表達形式的學科。某些類型系統適合用作數學基礎，取代數學家一般使用的集合論，其中最具影響力的有阿隆佐·邱奇的有類型λ演算和佩爾·馬丁-洛夫的直覺類型論。許多函數語言和電腦協助定理驗證（英語：Proof assistant）工具都建立在類型論的基礎上，如Agda、Coq、Idris、Lean等等。

類型論的核心概念是，每一條合乎語法規則的表達式（或稱「項」）都有其所屬的「類型」。通過結合多個基礎類型，可以定義更加複雜的類型。如此得出的類型可以代表林林總總的數學結構，如自然數、群、拓撲空間等等。在集合論中，這些結構都是含有元素（或稱成員）的集合，它的定義純粹就是指定其所含的所有元素。在類型論中，這些結構的定義並不羅列屬於它的所有項，而是指定如何建構它的項的一套規則。

集合論建基於一階邏輯，有「集合」和「命題」兩個主要概念。任何一套集合論公理（如策梅洛-弗蘭克爾集合論）和命題都是以一階邏輯的語言所表達。類型論則只有「類型」的概念，每一條邏輯命題都是一個類型。要證明任何一條命題，就需要建構屬於此類型的項，是為命題為類型原理。換言之，證明定理的過程只不過是建構符合指定數學結構的數學物件的過程的一個特例。^[1]

概覽

類型論有許多種，底下更細分許多變體，本文只能以直覺類型論為例做基本的入門介紹，而不詳細羅列每一種變體。

項與類型

在類型論中，每一個數學對象都有其所屬的類型（籠統地來說，這個類型的獨一無二的）。每次加入新的變量時，必須同時指定其所屬的類型。舉例說，「設x為自然數」可寫作

${\displaystyle x:\mathbb {N} }$

讀作「項x的類型是${\displaystyle \mathbb {N} }$」。這在形式上似乎和集合論中的${\displaystyle x\in \mathbb {N} }$（「x是集合${\displaystyle \mathbb {N} }$的元素」）無所差異，但後者是一階邏輯中具備真值的一條「命題」，而前者則是一個純粹的「斷言」，並不是一條有待證明的命題。^[1]

類型建構規則

每一種類型論都指定了如何建構新類型（及其項）的一套規則，通過這些規則所得出的式子都是合理的斷言，不須證明。以下歸納每一個新類型定義的組成部分：^[1]

1. 建構規則：如何建構符合某種格式的新類型。例如，當A和B分別為類型的時候，可以建構有序對類型A × B，亦可建構函數類型A → B。
2. 建構式，或稱引入規則：如何建構屬於這一類型的項。例如，從a : A和b : B這兩個項，就可以建構A × B的項，記作(a, b)。
3. 消去式，或稱消去規則：如何使用屬於這一類型的項。例如，設A, B, C為類型，對應於每一個函數g : A → (B → C)，都有一個函數f : A × B → C。這條規則指定了如何使用A × B的項。
4. 運算規則：消去式如何應用在建構式上。例如，設a, b, c分別為A, B, C的項，則f( (a, b) )定義為等同g(a)(b)。
5. 唯一原理（可有可無）：規定指入某個類型或從某個類型指出的函數是唯一的。比如，「A × B的每一個項都可以唯一地表達為(a, b)」。在設計類型論的時候，可以把唯一原理列入類型的建構規則之中，亦可省略之，而視其為有待證明的命題。

以上是類型論的基本規則，可理解為類型論的語法，它並不包含數學公理。這和集合論有所不同：除了一階邏輯本身的推理規則以外，集合論還加入了一組有關集合的公理（如策梅羅-弗蘭克爾公理系統）。最基本的類型論不需公理即可當做邏輯和數學推理使用，但在有需要時，同樣也可以加上額外的公理。類型論中的公理是不通過建構規則而接納的斷言，因此有些公理會產生無法通過運算規則簡化的式子，從而影響該類型系統的可計算性。

常見類型

以下列出幾種常見的基本類型，除了全類和（依賴）函數類型以外，它們都是最後介紹的歸納類型（英語：Inductive type）的特例。這些類型既可以表達數學結構，又可以表達命題。類型的項可以是某個數學結構的成員，也可以是某條命題的證明。這就是命題為類型原理。

全類

類型論規定，在介紹新的符號時，必須馬上指定它的類型，如「設${\displaystyle n:\mathbb {N} }$」。同樣，當我們說「設A為類型」的時候也一樣要指定A自己的類型。然而，A本身就已經是一個類型，那麼類型的類型是甚麼？類型論中有「全類」的概念，每個全類的項都是類型。由於全類本身也是一個類型，如果所有類型都屬於同一個全類的話，就不可避免產生吉拉爾悖論（英語：Girard's paradox）（羅素悖論在類型論中的體現）。因此，類型論一般都會假設存在無限層全類，記作𝒰₀, 𝒰₁, 𝒰₂，如此類推。每一層全類都是它上一層全類的項：𝒰_i : 𝒰_i+1。「設A為類型」的意思其實是「設A : 𝒰_i」，其中層級i可以明確指定，但一般可以從前文後理推斷出來，所以下標往往省略不寫。同理，當我們說「對於所有類型A」，意思其實是「對於所有第i層全類下的類型A」。有些類型系統規定，𝒰_i下的所有項也是𝒰_i+1的項，這種累積性屬性對設計一個類型系統來說有利有弊，在此並不詳述。

以上解釋的是羅素式全類。塔斯基式全類是另一種繞過悖論的方法，它主張每個A : 𝒰要經過一個明確的強制轉換函數才能成為一個類型El(A)。

函數類型

類型論將函數視為一種基礎類型，而不像集合論一樣定義為笛卡爾積的符合某些規定的子集。每一個函數都屬於一個類型：假設A, B為類型，可以建構函數類型A → B。要定義這一類型的某個項，共有兩種方法。第一種是直接定義：先給函數取名，例如f，然後對於任意項a : A，將f(a)定義為一條可能含有a並且類型為B的公式Φ。f的定義可以讀成「給我任何一個a : A，我都可以給你一個Φ : B」。另一種方法是λ抽象化，直接寫(λ (a : A), Φ) : A → B，避開給函數取名。

從命題為類型原理的角度來看，函數可以用來表達邏輯蘊涵。假如p, q分別是代表命題的類型，那麼p → q就代表了「當p為真，則q為真」這一命題。要證明此命題，對於p的每個項（即證明），須給出q的一個項。

依賴類型

依賴函數類型，又稱Π類型，是普通函數類型的推廣，使得函數的對應域類型可以依賴於輸入值。對於任何類型A和一族類型B : A → 𝒰（即對於任何a : A都有一個可能不同的類型B(a)），都可以建構依賴類型

${\displaystyle \prod _{a:A}B(a).}$

要定義依賴類型的某個項（即某個依賴函數），同樣有兩種方法。直接定義：取名f，對於任意項a : A，將f(a)定義為一條可能含有a並且類型為B(a)的公式Φ。λ抽象化：直接寫

${\displaystyle \lambda (a:A),\Phi :\prod _{a:A}B(a).}$

假如A是任意類型而p : A → 𝒰是一族代表命題的類型，那麼${\displaystyle \prod _{a:A}p(a)}$就代表了「對於所有a : A，p(a)為真」這一命題。

空類型

空類型記作⊥或0，它沒有任何相應的建構式，也就是說，它沒有任何項。空類型的消去規則是，對於任何類型A，都有一個函數false_elim : ⊥ → A。根據命題為類型原理，空類型可以詮釋為「假」命題，它不存在任何證明。設p為代表命題的類型，則p → ⊥代表「非p」這一命題，記作¬p。假設⊥有一個項h，而p為任何代表命題的類型，那麼通過空類型的消去規則就可以得出false_elim h : p。這意味着無論甚麼命題都可以證明是真的，是為爆炸原理。

單值類型

單值類型記作⊤或1，它只有一條建構式，因此只含唯一的單個項，記作「∗ : 1」。假如有一個函數f : 1 → A，則可以說A有一個項f(∗)，亦稱「A是有棲居對象的類型」（類型論區分「有棲居對象」和「非空」這兩個概念）。

雙值類型

雙值類型記作${\displaystyle \mathbb {B} }$或2，它有兩條構件式，因此有兩個項，記作「0₂, 1₂ : 2」。雙值類型就是函數式編程中的布林，其兩個項可以分別理解為「如果假」和「如果真」兩個情況。函數f : 2 → A可以理解為「如果真，輸出f(1₂) : A，否則輸出f(0₂) : A」。

積類型

積類型所表達的是有序對的概念。從兩個類型A, B可以建構出它們的積類型A × B。它有一條建構式：從兩個項a : A和b : B可以建構出積類型的項(a, b) : A × B。對應於每一個函數g : A → (B → C)，都有一個函數f : A × B → C。

積類型可以詮釋為邏輯與：假如類型A, B, C都是命題，則函數f : A × B → C可以理解為「假如同時有A的證明和B的證明，就可以用f得出C的證明」。更簡短地說，「A與B為真時，則C為真」。

餘積類型

餘積類型所表達的是不交並的概念。從兩個類型A, B可以建構出它們的餘積類型A + B。它有兩條建構式：從一個項a : A可以建構出inl(a) : A + B，從一個項b : B則可以建構出inr(b) : A + B。要建構函數f : A + B → C，須指定兩個函數g₀ : A → C和g₁ : B → C，使得f(inl(a))定義為g₀(a)，f(inr(b))定義為g₁(b)。

餘積類型可以詮釋為邏輯或：假如類型A, B, C都是命題，則函數f : A + B → C可以理解為「假如有A的證明，或者有B的證明，只需其一就可以用f得出C的證明」。更簡短地說，「A或B為真時，則C為真」。

上文介紹的雙值類型可視為餘積類型的特例，等同於1 + 1。

依賴對類型

依賴對類型，又稱Σ類型，是積類型的推廣，使得每個項(a, b)中的第二個對象b的類型可以依賴於a。對於任何類型A和一族類型B : A → 𝒰，可以建構依賴對類型

${\displaystyle \sum _{a:A}B(a).}$

它的項的格式是(a, b)，其中a : A，而b : B(a)。

假如A是任意類型而p : A → 𝒰是一族代表命題的類型，那麼${\displaystyle \sum _{a:A}p(a)}$就代表了「存在a : A使得p(a)為真」這一命題。值得注意的是，這種存在比經典數學中的存在更強，因為類型論要求我們明確提供見證p(a)為真的那個項a，而經典數學則無此要求（比如可以婉轉地證明「不可能不存在這樣的a」）。這意味着，最純粹的類型論表達的是一種構成主義數學。通過引入各種公理，如排中律和選擇公理，類型論仍然可以靈活地表達非構成主義的經典數學。

自然數

類型論一般按照皮亞諾算術來定義自然數${\displaystyle \mathbb {N} }$。它共有兩條建構式：

• ${\displaystyle 0:\mathbb {N} }$，自然數的起始點
• ${\displaystyle {\mathsf {succ}}:\mathbb {N} \to \mathbb {N} }$，自然數的後繼函數

任何自然數，要麼是0，要麼是某個自然數的後繼（即等於${\displaystyle {\mathsf {succ}}(n)}$，其中${\displaystyle n:\mathbb {N} }$）。一、二、三分別表達為${\displaystyle {\mathsf {succ}}(0)}$、${\displaystyle {\mathsf {succ}}({\mathsf {succ}}(0))}$、${\displaystyle {\mathsf {succ}}({\mathsf {succ}}({\mathsf {succ}}(0)))}$，如此類推。

要定義某個函數${\displaystyle f:\mathbb {N} \to A}$，須指定一個起始項g₀ : A以及一個「下一步」函數${\displaystyle g_{\mathsf {succ}}:\mathbb {N} \to A\to A}$，使得f(0)定義為g₀，並且對於任何${\displaystyle n:\mathbb {N} }$，${\displaystyle f({\mathsf {succ}}(n))}$定義為${\displaystyle g_{\mathsf {succ}}(n)(f(n))}$，也就是以0為起始點利用數學歸納法做一個遞歸性的定義。比如，以下是「奇偶」函數${\displaystyle {\mathsf {oddeven}}:\mathbb {N} \to {\boldsymbol {2}}}$的定義：

• g₀定義為0₂
• ${\displaystyle g_{\mathsf {succ}}:\mathbb {N} \to {\boldsymbol {2}}\to {\boldsymbol {2}}}$的定義：對於所有${\displaystyle n:\mathbb {N} }$，
  • ${\displaystyle g_{\mathsf {succ}}(n)(0_{\boldsymbol {2}})}$定義為${\displaystyle 1_{\boldsymbol {2}}}$
  • ${\displaystyle g_{\mathsf {succ}}(n)(1_{\boldsymbol {2}})}$定義為${\displaystyle 0_{\boldsymbol {2}}}$

這裏我們也用到了雙值類型2的消去式。其他常見函數，例如「雙倍」函數${\displaystyle {\mathsf {double}}:\mathbb {N} \to \mathbb {N} }$以及加法${\displaystyle +:\mathbb {N} \to \mathbb {N} \to \mathbb {N} }$等二元運算都有類似的定義。

等同類型

類型論有至少三種可以理解為「等同」的概念。第一種是「符號等同」，又稱「從定義上等同」，例如用1定義為代替${\displaystyle {\mathsf {succ}}(0)}$的符號，這記作${\displaystyle 1:\equiv {\mathsf {succ}}(0)}$。自然數一節中的「定義為」就屬於此種等同，也可以用:≡表示。這種等同是為了給符號賦予含義，但它本身不含任何額外的數學意義。

第二種是「斷言等同」，即在展開兩個符號的定義，並用類型論建構規則運算以後，兩者的公式完全吻合，記作「a ≡ b」。例如，通過oddeven的定義，可做運算：

${\displaystyle {\mathsf {oddeven}}(1)\equiv g_{\mathsf {succ}}(0)({\mathsf {oddeven}}(0))\equiv g_{\mathsf {succ}}(0)(g_{0})\equiv g_{\mathsf {succ}}(0)(0_{\boldsymbol {2}})\equiv 1_{\boldsymbol {2}}.}$

若a ≡ b，則在任何式子中出現的a都可以直接替換為b。此種等同屬於斷言，並不是邏輯命題，而是重複應用類型論語法規則後所得的符號等同。在類型論中，不允許說「假設a ≡ 1」，因為在設符號${\displaystyle a:\mathbb {N} }$的時候，如果還沒有給n賦予定義值，那就應該做定義「a :≡ 1」；反之如果n已經被賦予定義值（比如1），那就輪不到我們假設其數值。假如將類型論的規則視為某種代數系統，那麼斷言等同就正是該系統中的普通等同關係，類似於一個群的元素之間的等同。

第三種是「命題等同」。有時，兩條公式就算在展開定義和運算之後，仍然不完全吻合，但它們具有相同的語義。舉例來說，對於所有${\displaystyle n:\mathbb {N} }$，n + 1和1 + n這兩條公式無論如何運算都不會斷言等同，因為自然數加法的定義本身就區分先後順序。故此，我們不能寫「對於所有${\displaystyle n:\mathbb {N} }$，n + 1 ≡ 1 + n」。然而，對於任何特定的自然數n，例如2，我們可以通過運算得出「2 + 1 ≡ 1 + 2」。這種從定義上不同但從含義上相同的現象，正正就是內涵和外延之分，邏輯學家戈特洛布·弗雷格稱之為意涵與指稱（英語：Sense and reference）之分。

針對這第三種等同關係，類型論有一種意義重大的「等同類型」。對於任何兩條類型相同的公式p, q : A，都有一個類型Id_A(p, q)，指的是「p等於q」這一命題。在不怕混淆的情況下，可以使用更熟悉的寫法「p =_A q」，其中類型下標A往往可以省略。根據命題為類型原理，要證明此命題，就必須提供它的項（此命題為真的見證物）。等同類型只有一條建構式：對於任何項a : A，可以建構refl_a : a =_A a，稱為「自反」。由於斷言等同的公式都可以隨意互換，所以只要有a ≡ b，那就自動有a =_A b。要證明「對於所有${\displaystyle n:\mathbb {N} }$，n + 1 = 1 + n」這一命題，就必須給出這樣的項：

${\displaystyle {\mathsf {add\_one\_eq\_one\_add}}:\prod _{n:\mathbb {N} }(n+1=_{\mathbb {N} }1+n).}$

要建構這樣的項，須展開1和加號的定義，然後結合利用依賴類型、自然數和等同類型的建構和消去式。再舉一例，${\displaystyle 0=_{\mathbb {N} }1}$也是一條合乎語法的等同類型，但它所代表的是一條假命題，所以它不含任何項。

歸納類型

歸納類型是定義新類型的一套規則，以上介紹的0、1、2、${\displaystyle \mathbb {N} }$、A × B、a =_A b等都是其特例。要定義一個歸納類型，必須列出它的建構式。每一條建構式不但可以直接輸出該類型的項（如∗ : 1），它的輸出項還能依賴於某個變數（如inl : A → A + B），甚至歸納性地依賴於該類型自己的項（如${\displaystyle {\mathsf {succ}}:\mathbb {N} \to \mathbb {N} }$），從而建構出無限大的數學結構。歸納類型代表了由它的建構式所自由生成的結構，也就是說，它的項正好都是從無開始，通過重複應用任一條建構式後所得的。本文不試圖詳列歸納類型的嚴格定義。

舉例來說，我們可以用歸納類型來定義整數${\displaystyle \mathbb {Z} }$。它有兩條建構式：

• ${\displaystyle {\mathsf {ofNat}}:\mathbb {N} \to \mathbb {Z} }$，從每一個自然數可建構一個對應的非負整數
• ${\displaystyle {\mathsf {negSucc}}:\mathbb {N} \to \mathbb {Z} }$，從每一個自然數可建構一個對應的負整數（理解為−(n + 1)）

要建構某一個整數，須先指定用哪一條建構式，然後指定一個自然數。

再以么半群為例，它只有一條比較長的建構式，為方便閱讀以文字寫出：

• 一個類型G，一個乘法函數G × G → G（記作(a, b) ↦ a * b），一個單位元e : G，以及以下兩項條件的證明：
  • 對於任何x : G，x * e = x且e * x = x
  • 對於任何x, y, z : G，x * (y * z) = (x * y) * z

要建構某一個么半群，只須提供這單一條建構式所規定的所有項。

同倫類型論

主條目：同倫類型論

同倫類型論是類型論底下一個活躍的研究范疇，它主張從同倫論的角度視每一個類型為（拓撲）空間，並且從范疇論的角度視類型為高維廣群。符拉基米爾·弗沃特斯基在研究餘調和∞廣群的時候，多次遇到某些證明含有錯誤，但在同行評審的過程中成為了漏網之魚，這促使他意識到電腦自動驗證證明的重要性。另一方面，他發現數學家常年以來普遍使用的策梅洛-弗蘭克爾集合論並不能作為滿足現代數學論證的日常用途的數學基礎。因此他利用Coq證明協助器，在構造演算（類型論的一種）的基礎之上研發出基於一價公理上的新數學基礎。

基本概念

在這樣的框架下，類型的項可以想像成空間裏的點，而兩個項之間等同則可以想像成兩個點之間有一條路徑。假如類型A中有兩項等同p : a =_A b，這可以理解為「p是始於a而終於b的路徑」。等同類型的對稱性意味着存在p⁻¹ : b =_A a，可以理解為「p⁻¹是始於b且終於a的路徑」。當然，每個項都有自己的自反路徑refl_a : a =_A a，可以理解為停留在a上不動的路徑。

利用等同類型的遞移關係，可以從p : a =_A b和q : b =_A c得出p ∘ q : a =_A c。理解為路徑的話，路徑p和路徑q可以複合（串聯）起來形成一條始於a而終於c的路徑p ∘ q。假如我們複合p和它的對稱，就會得出p⁻¹ ∘ p : a =_A a。不過，這一條路徑往b點跑了一個來回，並不完全等同refl_a，儘管兩者都是同一條命題的證明。這體現了同倫類型論所強調的「證明相關性」。

從拓撲空間的角度來看，由於p⁻¹ ∘ p沿着同一條線來回跑，所以它可以連續「縮小」至原地不動的refl_a，而不怕中途被某個「孔」勾住。這種路徑與路徑之間的連續變換稱為同倫，亦可視為始於p⁻¹ ∘ p而終於refl_a的一條二維路徑，記作

p⁻¹ ∘ p =_{a =A a} refl_a.

循同樣的規律，很自然地有二維路徑之間的三維路徑（同倫間的同倫），三維路徑之間的四維路徑，等等。

從抽象代數的角度來看，路徑之間的複合可以視為乘法，自反路徑refl_a可以視為單位元，而任何路徑p的對稱p⁻¹可以視為反元素。這類似於群的結構，但有兩點差異。第一，不是任何兩條路徑都可以複合，因為其中一條的終點必須是另一條的起點，意味着這只是一個廣群而不是群。第二，p⁻¹ ∘ p只是和refl_a同倫等價而不是完全等同，因而反元素（結合律同理）只是在同倫意義上得到滿足，故此只能說是弱廣群。整體來說，這種具有無限層的類型結構形成弱∞廣群（英語：∞-groupoid）。

任何函數f : A → B都會將命題等同的兩個項對映至兩個命題等同的項，從范疇論的角度可以說類型論中的函數都是函子，而從拓撲學的角度則可以說每個函數都是連續的。

拓撲學的纖維化和范疇論的等價等等概念同樣也有類型論的模擬。

一價公理

在拓撲學中，假如兩個空間是同倫等價的，那麼它們的許多拓撲性質也會是相同的。因為同倫這一概念在類型論中也有對應的「等價」概念，所以我們可以寫下「類型A, B : 𝒰是等價的」這樣的命題，記作A ≃ B。

在一般「非形式化」的數學推理當中，也就是不糾結於數學基礎細節的時候，數學家往往會濫用符號，隨意互換兩個等價但嚴格來說不完全等同的對象。例如，群論所研究的是同構意義上不同的群的性質，而拓撲學所研究的是同胚意義上不同的空間的性質。換言之，數學家一般並不在乎兩個等價結構之間定義上的細節差異。例如，實數到底是以戴德金分割還是柯西序列來表示並不重要，更重要的是它的抽象性質，特別是在與另一個等價結構互換以後仍然不變的性質。傳統的集合論把所有結構都以層層相疊的集合來表達，無法做這種符合結構主義（英語：Structuralism (philosophy of mathematics)）的數學推理。

類型論對類型的定義恰好遵循結構主義，但在「兩個等價的類型可以互換」這一問題上，我們只能對於每一對等價類型A ≃ B逐一證明。弗沃特斯基因此提出在純粹的類型論上加入一條新的公理，稱為一價公理：

(A =_𝒰 B) ≃ (A ≃ B),

可以讀成

「等同」等價於「等價」。

一價公理推廣了同一個全類以下兩個類型之間的等同關係。它要求同倫類型論下的所有定義都不違背類型間的同倫等價。對於任何同倫等價e : A ≃ B和任何項t : P(A)，其中P(A)是利用A建構出的類型，都可得出一個對應的項e^∗t : P(B)。

以一價公理作為數學基礎，終於能夠對常用的數學推理手法做嚴謹的形式化表述。

更高歸納類型

更高歸納類型是在同倫類型論的框架下對歸納類型的推廣。更高歸納類型的建構式不但可以像普通歸納類型一樣建構新的項（點），它還能夠建構新的等同類型的項（兩點之間的路徑）。例如，我們可以定義拓撲學意義的圓${\displaystyle \mathbb {S} ^{1}}$，它有兩條建構式：

• ${\displaystyle {\mathsf {base}}:\mathbb {S} ^{1}}$，圓的基點
• ${\displaystyle {\mathsf {loop}}:{\mathsf {base}}=_{\mathbb {S} ^{1}}{\mathsf {base}}}$，從基點至基點的路徑

這第二條建構式所建構的是有別於常值路徑${\displaystyle {\mathsf {refl}}_{\mathsf {base}}:{\mathsf {base}}=_{\mathbb {S} ^{1}}{\mathsf {base}}}$的另一條（一維）路徑，為這一類型賦予了不平凡的拓撲結構。

再舉一例，我們可以定義拓撲學意義的球面${\displaystyle \mathbb {S} ^{2}}$，它同樣有兩條建構式：

• ${\displaystyle {\mathsf {base}}:\mathbb {S} ^{2}}$，球面的基點
• ${\displaystyle {\mathsf {surf}}:{\mathsf {refl}}_{\mathsf {base}}=_{{\mathsf {base}}=_{\mathbb {S} ^{2}}{\mathsf {base}}}{\mathsf {refl}}_{\mathsf {base}}}$，非平凡的二維路徑

儘管定義裏只有基點和一條二維路徑，但是可以證明${\displaystyle \mathbb {S} ^{2}}$還有一條非平凡的三維路徑，其起點和終點都是refl_reflbase。這就是霍普夫纖維化，同時印證了，更高歸納類型的簡單定義也可以創造出複雜而不易預見的拓撲結構。

廣義地來說，更高歸納類型的建構式可以建構任何更高維度的路徑（同倫）。

類型論體系

主要

• 簡單類型λ演算，一種高階邏輯；
• 直覺類型論；
• 系統F;
• LF經常用來定義其他類型論；
• 構造演算及其衍生理論。

次要

• Automath（英語：Automath）；
• ST類型論;
• 組合邏輯的一些形式；
• λ立方體中定義的其他；
• 其他有類型λ演算;
• 其他純型別系統（英語：pure type system）。

活躍

• 正在研究中的同倫類型論

參閲

• 直覺類型論
• 有類型lambda演算
• 型別系統
• 域理論
• 範疇論

參考文獻

1. Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. 2013 [2022-12-27]. （原始內容存檔於2021-01-22） （英語）.

• Farmer, William M. The seven virtues of simple type theory. Journal of Applied Logic. 2008, 6 (3): 267–286. doi:10.1016/j.jal.2007.11.001.

延伸閱讀

• Andrews, Peter B. Introduction to Mathematical Logic and Type Theory: To Truth Through Proof 2nd ed. Kluwer Academic Publishers. 2002. MR 1932484. doi:10.1007/978-94-015-9934-4. 引文格式1維護：冗餘文字 (link)
• Cardelli, Luca, 1997, "Type Systems, （頁面存檔備份，存於互聯網檔案館）" in Allen B. Tucker, ed., The Computer Science and Engineering Handbook. CRC Press: 2208-2236.
• Mendelson, Elliot, 1997. Introduction to Mathematical Logic, 4th ed. Chapman & Hall.
• Pierce, Benjamin, 2002. Types and Programming Languages. MIT Press. ISBN 0-262-16209-1)
• Thompson, Simon, 1991. Type Theory and Functional Programming （頁面存檔備份，存於互聯網檔案館）. Addison-Wesley. ISBN 0-201-41667-0.
• Winskel, Glynn, 1993. The Formal Semantics of Programming Languages, An Introduction. MIT Press. ISBN 0-262-23169-7.

外部連結

• Stanford Encyclopedia of Philosophy: Type Theory（頁面存檔備份，存於互聯網檔案館）" -- by Thierry Coquand.
• National Institute of Standards and Technology: Abstract data type （頁面存檔備份，存於互聯網檔案館）
• A summary paper on the formal basis of ADTs, relationship to category theory, and list of good references （頁面存檔備份，存於互聯網檔案館）. Pages 3-4 appear relevant. Reference number [6] looks good, but it may not be available online.
• Constable, Robert L., 2002, "Naïve Computational Type Theory, （頁面存檔備份，存於互聯網檔案館）" in H. Schwichtenberg and R. Steinbruggen (eds.), Proof and System-Reliability: 213-259.
• The Nuprl Book: "Introduction to Type Theory. （頁面存檔備份，存於互聯網檔案館）"