在類型理論中，如果一個系統具有從創建該類型的常量和函數中創建新類型的設施，那么它就具有歸納類型。該功能的作用類似于編程語言中的數據結構，并允許類型理論增加數字、關系和樹等概念。顧名思義，歸納類型可以是自指的，但通常只允許結構性遞歸的方式。標準的例子是使用Peano的編碼對自然數進行編碼。歸納式nat:Type:=|0:nat|S:nat->nat。在這里，一個自然數是由常數0或通過將函數S應用于另一個自然數而產生的。S是繼任函數，表示在一個數上加1。因此，0是0，S0是1，S（S0）是2，S（S（S0））是3，以此類推。自引入以來，歸納類型已經被擴展到編碼越來越多的結構，同時仍然是預測性的并支持結構遞歸。

歸納類型通常帶有一個函數來證明關于它們的屬性。因此，nat可能帶有。nat_elim:(forallP:nat->Prop,(P0)->(foralln,Pn->P(Sn))->(foralln,Pn))。這是nat類型的結構遞歸的預期函數。

W-類型是直覺類型理論（ITT）中的有根有據的類型。它們概括了自然數、列表、二叉樹和其他樹形數據類型。讓U是一個類型的宇宙。給定一個類型A：U和一個依賴族B：A→U，我們可以形成一個W類型.類型A可以被認為是被定義的歸納類型的（可能是無限多的）構造函數的標簽，而B表示每個構造函數的（可能是無限的）arity。W-類型（resp.M-類型）也可以被理解為井底之蛙（resp.非井底之蛙），其節點由元素a：A標記，由a標記的節點有B（a）多條子樹。每個W型與一個所謂的多項式漏斗的初始代數同構。讓0、1、2等為有限類型，居民為11：1、12、22：2等。我們可以把自然數定義為W型與f:2→U的定義是：f(12)=0（代表零的構造函數，不需要參數），f(22)=1（代表繼承函數，需要一個參數）。

我們可以在一個類型A：U上定義列表為{displaystylef(operatorname{inr}(a))}則對應于空列表的構造函數。的值對應于將a追加到另一個列表的開頭的構造函數。通用W型的元素的構造函數W-類型的消除規則與樹的結構歸納法類似。如果，只要有一個屬性（在命題即類型的解釋下），那么對某棵樹的所有子樹都成立，對該樹也成立，那么它對所有樹都成立。在擴展類型理論中，W-類型（resp.M-類型）可以被定義為多項式漏斗的初始集合體（resp.最終集合體），直至同構。在這種情況下，初始性（res.finality）的屬性直接對應于適當的歸納原則。在具有單等價公理的擴展類型理論中，這種對應關系直到同構（命題平等）才成立。M-類型是W-類型的對偶，它們代表硬幣