直覺類型理論（又稱構造類型理論，或馬丁-勒夫類型理論）是一種類型理論，也是數學的另一種基礎。所有的版本都保留了構造邏輯的核心設計，即使用依賴類型。

馬丁-勒夫根據數學建構主義的原則設計了這個類型理論。建構主義要求任何存在證明都要包含一個證人。因此，任何關于存在大于1000的素數的證明都必須確定一個既是素數又大于1000的具體數字。直觀類型理論通過內化BHK解釋完成了這個設計目標。一個有趣的結果是，證明成為可以被檢查、比較和操作的數學對象。信念類型理論的類型構建器是按照與邏輯連接詞的一對一對應關系來構建的。例如，邏輯連接詞被稱為暗示().這種對應關系被稱為庫里-霍華德同構。以前的類型理論也遵循這種同構，但馬丁-勒夫的類型理論是xxx個通過引入從屬類型將其擴展到謂詞邏輯的類型理論。類型理論直覺型類型理論有3個有限類型，然后用5個不同的類型構造器組成。與集合理論不同，類型理論不是建立在像弗雷格的邏輯之上的。因此，類型理論的每一個特征都是作為數學和邏輯的特征而承擔雙重職責。如果你不熟悉類型理論而知道集合理論，那么快速的總結就是。類型包含術語，就像集合包含元素一樣。術語屬于一種且僅屬于一種類型。術語如計算（減少）到像4這樣的典型術語。更多內容請參見類型理論一文。0類型，1類型和2類型有3個有限類型。0型包含0個術語。1型包含1個規范術語。而2類型包含2個規范術語。因為0類型包含0個術語，它也被稱為空類型。它被用來表示任何不存在的東西。

它也可以寫成{displaystyle/bot}，表示任何無法證明的東西。并代表任何無法證明的東西。(也就是說，它的證明不能存在。)因此，否定被定義為對它的一個函數。同樣地，1類型包含1個典型術語，代表存在。它也被稱為單位類型。它通常代表可以被證明的命題，因此，有時被寫成最后，2類型包含2個典范術語。它代表兩個值之間的明確選擇。它用于布爾值，但不用于命題。命題被認為是1類型，可以被證明為永遠沒有證明（0類型），也可以不被證明。(在直覺類型理論中，排除中間法則對命題不成立)。

Σ-類型包含有序對。與典型的有序對（或2元組）類型一樣，Σ類型可以描述笛卡爾乘積。Σ-類型比典型的有序對類型更強大，因為有依賴類型。在有序對中，第二項的類型可以取決于xxx項的值。例如，一對中的xxx項可能是一個自然數，第二項的類型可能是一個長度等于xxx項的向量。這樣的類型將被寫成。用集合理論的術語來說，這類似于集合的索引不相交聯合。在通常的有序對的情況下，第二項的類型并不取決于xxx項的值。因此，描述笛卡爾乘積的類型是這里需要注意的是，xxx項的值。{displaystylen}，在這里必須注意，xxx項的值，n，并不取決于第二個項的類型。Σ-類型可以用來建立數學和其他學科中使用的更長的依賴類型的圖元。