在這個情況下，對任意型別 $t$ ，slice category $C/t$ 表示「到達 $t$ 的 morphism」所構成的範疇，也就是 $C/t$ 的 objects 與 triangle morphisms。

接著，我們要關心其中沒定義的 morphism，我們將基於此集合討論型別 $T$ 有多大。技術上來說，是指從 terminal object $1$ 出發的所有 morphisms（記為 $\text{Hom}_{C}(1, T)$ ），這些 morphisms 對應到內建的形式；以邏輯來說是指公理，而在函數式語言裡面，我們最常看到的定義公理的方式就是 data type！換句話說，型別的大小由建構子決定：

• $0$ 是 False / Empty type，沒有任何建構子
• $1$ 是 Unit type，只有一個建構子
• $2$ 是 Bool type，只有兩個建構子

依此類推可以知道有 $k$ 個單元建構子（即建構子 c 滿足 c : K ）的型別 K 可以解釋為 $k$ -type，接著 $2 \to T$ 的元素應該有幾個呢？答案是 $T \times T = T^2$ ，同理我們可以建立 $k \to T = T \times ... \times T = T^k$ 的關係式。

依此可以建立一個簡單的直覺是 c : T 表示 $+1$ ，而更加複雜的型別如 c : (2 -> T) -> T 就表示 $+T^2$ ，建構子的參數表現了型別增長的速度，決定了型別的大小。

一個常見的案例是自然數，我們通常定義 $z : \N$ 和 $s : \N \to \N$ 兩個建構子來表示自然數 $\N$ 。用 F-algebra 來表示，可以得到 $(1 + \mathbb{N}) \to \mathbb{N}$ ，從沒有循環參考的角度來看，當前 $\N$ 的大小即取決於上一個 $\N$ 的大小。畫出交換圖就可以了解到從基本點 $z$ 出發，只有 $s$ 一個方向可以前進，恰恰就是可數無限大的定義，是以看到這與歸納法的對應時，應當不會太過驚訝。

在 dependent type 語言裡面，data type 會變成 inductive data type，引入了更多的限制，而其中跟大小有關的限制就是這裡想要討論的。

Question. 在定義建構子時 c : (T -> T) -> T 有參數 $T^T$ ，試問 $T^T$ 有多大？

答案是不知道，因為我們根本還不知道 $T$ 到底是什麼。

當 $T$ 定義完畢之後，這個簽名用在函數上倒是沒有問題，因為其大小已經確定，不會遇到自我指涉引發的麻煩。

雖然可以用公理強迫 $T^T$ 有 size，但這樣做一來會破壞計算性；二來會顯著的複雜化 termination check。舉例來說，要是容許定義 c，就可以寫出

def foo (t : T) : T :=
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     match t with
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     | c f => f t

接著 foo (c foo) 就會陷入無限迴圈，為了要有強正規化，我們希望排除所有這類型的程式，比起一個一個去比對，直接禁止定義 c 這類的建構子可以更簡單的達成目的。Haskell/OCaml 的 data type 則不做此限制，因為它們不需要強正規化，這也是為什麼 dependent type 語言常説其 data type 是 inductive data type，並不輕易省略 inductive 這個詞，因為這樣定義的類型滿足 induction principle。

另外一提，Bauer 談到所有建構子都是為了符合 $c : \Pi_{x : B} (A \; x \to T) \to T$ 的形式，有興趣的讀者可以著手證明。此外 strictly positive 的遞迴定義可能更適合實現檢查機制。

典型的情況是 fibonacci 數列，展示了前面的型別大小如何與程式相關，常見的程式定義如下

def fib : Nat → Nat
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     | 0   => 1
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     | 1   => 1
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     | n+2 => fib n + fib (n+1)

為了抽出計算部分的代數，我們用 inductive type 定義其計算

inductive Fib (a : Type) : Nat → Type where
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     | z : a → Fib a 0
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     | o : a → Fib a 1
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                     | s : Fib a n → Fib a (n+1) → Fib a (n + 2)

可以看到 induction case 就是 $(2 \to F a) \to F a = {F a}^2 \to F a = F a \times F a \to F a$ ，所以對應的程式就是兩次呼叫 fib n + fib (n+1) 。當然，因為 fibonacci 還有一個利用矩陣計算的編碼

這個方法對應到 $O(n)$ 的演算法，因此 fibonacci 不一定要用分形遞迴計算。這件事也告訴了我們代數簽名有時候比我們具體的計算更寬鬆，上面的 inductive type 並未限制如何使用 s，也因此可以摺疊時可能存在更快的計算方式。這也說明了當遇到 c : (T -> T) -> T 一類的建構子時，其對應的計算難以寫出的問題，也就是前面沒辦法定義 $T^T$ 的大小的情形。