Well-founded type

在看 OTT 的時候發現只有 bottom, unit, bool 這三種基本的 type 跟 \Sigma{}, \prod{}, \mbox{W}, 前面五種都好理解, 然而最後一個 W-types 就夠了嗎? 結果回頭看了 Martin-Lof 的 ITT, 以及 Peter Dybjer, Anton Setzer 寫的東西以及 McBride 做的 Ornament 三個 constructor 之一的 arg 就是 W-types …