Example. 從 $1$ 出發 [tt-000I]

接著，我們要關心其中沒定義的 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$ 一個方向可以前進，恰恰就是可數無限大的定義，是以看到這與歸納法的對應時，應當不會太過驚訝。