之前在講解Curry-Howard correspondence時
我用的理論基礎是CoC
而CoC最大的問題在於：
它無法證明數學歸納法
為什麼呢？
首先來看看CoC中的自然數
還記得我最最前面在untyped lambda那篇介紹的定義嗎……

\[Nat: (X: Prop) \to (X \to X) \to X \to X \\ 0 \stackrel{def}{\equiv} \lambda X: Prop. \lambda f: X \to X. \lambda x: X. x \\ \texttt{succ} \stackrel{def}{\equiv} \lambda n: Nat. \lambda X: Prop. \lambda f: X \to X. \lambda x: X. f (n X f x)\]

問題在於
我們定義了一堆自然數
卻沒有定義這些數字之間的關係
\((X: Type_0) \to (X \to X) \to X \to X\)這個型別太弱了
無法表示這樣的事實：
一旦一述詞對於每個自然數\(n\)
\(\texttt{succ} \: n\)都成立
而且它成立於0
那麼它對每個自然數都成立
更精確地說
\(Nat\)的型別提供的資訊太少了
這是我們想要的數學歸納法和上面所定義\(Nat\)型別的比較：

\[\begin{array}{llllllllll} (X: Prop \to Prop) & \to & ((n: Nat) \to & X n & \to & X (\texttt{succ} \: n) & ) & \to & X 0 & \to (X: Nat) \to X n \\ (X: Prop) & \to & ( & X & \to & X & ) & \to & X & \to X \end{array}\]

怎麼辦呢？
我們可以使用醜陋但有效的方法：
直接在理論上定義新的type
這樣的type根據定義即符合數學歸納法

這邊有個或許不是很重要
但又有點重要的問題
這些新的type要屬於\(Prop\)還是\(Type_n\)
這問題的答案其實有點技術性
但總而言之是假如我想把它放在\(Prop\)內
這樣的型別系統作為邏輯很容易變成反古典的
也就是說它和雙重否定律不相容
因此定義在\(Type_n\)會是比較好的選擇
事實上
我接下來會完全捨棄\(Prop\)這個sort
而是跟循MLTT的傳統
只提供\(Type_n\)

接下來我要介紹一些這樣定義出來的型別
我將不從自然數開始
而是首先介紹些比較簡單的型別
例如\(A + B\)或是\(A \times B\)之類的
除此之外
我會先介紹它們的recursor
而非更廣義的inductor
現在我還無法解釋它們之間的不同
但到了下一篇文章一切都會變得明朗
目前只要知道我簡化了很多概念就是了