直観主義型理論

直観主義型理論（構成的型理論、またはマーティン＝レーフ型理論（MLTT）とも呼ばれる）は型理論であり、数学の代替的な基礎です。直観主義型理論は、スウェーデンの数学者で哲学者のペル・マーティン＝レーフによって考案され、1972年に初めて発表されました。型理論には複数のバージョンがあります。マーティン＝レーフは理論の内包的変種と外延的変種の両方を提案し、初期の非述語的バージョンはジラールのパラドックスによって矛盾が示され、述語的バージョンに取って代わられました。ただし、すべてのバージョンは、依存型を使用する構成的論理のコア設計を維持しています。

Martin-Löf は、数学的構成主義の原理に基づいて型理論を設計しました。構成主義では、存在証明には必ず「証人」が含まれている必要があります。したがって、「1000 より大きい素数が存在する」という証明は、素数であり、かつ 1000 より大きい特定の数を識別する必要があります。直観主義型理論は、BHK 解釈を内部化することでこの設計目標を達成しました。その結果、証明は、調査、比較、および操作できる数学的オブジェクトになります。

直観主義型理論の型構築子は、論理接続子と 1 対 1 に対応するように構築されました。たとえば、含意 ( ) と呼ばれる論理接続子は、関数 ( ) の型に対応します。この対応は、カリー - ハワード同型性と呼ばれます。以前の型理論もこの同型性に従っていましたが、マーティン - ローフの型理論は、依存型を導入することでこれを述語論理に拡張した最初の理論でした。 ${\displaystyle A\implies B}$${\displaystyle A\to B}$

直観主義型理論には 3 つの有限型があり、これらは 5 つの異なる型コンストラクタを使用して構成されます。集合論とは異なり、型理論はフレーゲの論理の上に構築されません。したがって、型理論の各機能は、数学と論理の両方の機能として二重の役割を果たします。

型理論に詳しくなく、集合論を知っている人のために簡単にまとめると、集合に要素が含まれるのと同じように、型には項が含まれます。項は 1 つの型にのみ属します。やなどの項は、 4 などの標準的な項に計算 (「簡約」) されます。詳細については、型理論に関する記事を参照してください。${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$

有限型は 3 つあります。0型には 0 個の項が含まれます。1型には1個の標準項が含まれます。2 型には2個の標準項が含まれます。

0型には 0 個の項が含まれているため、空の型とも呼ばれます。これは、存在できないものを表すために使用されます。また、 と書かれ、証明できないものを表します (つまり、その証明は存在できません)。その結果、否定はそれに対する関数として定義されます: 。 ${\displaystyle \bot}$${\displaystyle \neg A:=A\to \bot }$

同様に、1型は 1 つの標準項を含み、存在を表します。これは単位型とも呼ばれます。

最後に、2型には 2 つの標準用語が含まれます。これは、2 つの値の間の明確な選択を表します。これはブール値には使用されますが、命題には使用されません。

代わりに、命題は特定の型で表されます。たとえば、真の命題は1型で表され、偽の命題は0型で表されます。ただし、これらが唯一の命題であると主張することはできません。つまり、直観主義型理論の命題には排中律は当てはまりません。

Σ 型には順序付きペアが含まれます。一般的な順序付きペア (または 2 組) 型と同様に、Σ 型は他の 2 つの型 、 、およびの直積を記述できます。論理的には、このような順序付きペアは の証明と の証明を保持するため、このような型は と記述されることがあります。 ${\displaystyle A\times B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A\wedge B}$

Σ 型は、依存型付けのため、通常の順序付きペア型よりも強力です。順序付きペアでは、2 番目の項の型は最初の項の値に依存する場合があります。たとえば、ペアの最初の項は自然数で、2 番目の項の型は最初の項と同じ長さの実数のシーケンスである可能性があります。このような型は次のように記述されます。

${\displaystyle \sum _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)}$

集合論の用語を使用すると、これはインデックス付きの集合の非結合和集合に似ています。通常の直積の場合、2 番目の項の型は最初の項の値に依存しません。したがって、直積を表す型は次のように記述されます。 ${\displaystyle {\mathbb {N} }\times {\mathbb {R} }}$

${\displaystyle \sum _{n{\mathbin {:}}{\mathbb {N} }}{\mathbb {R} }}$

ここで重要なのは、最初の項の値は2 番目の項の型に依存しないことです。 ${\displaystyle n}$${\displaystyle {\mathbb {R} }}$

Σ 型は、数学で使用されるより長い依存型タプルや、ほとんどのプログラミング言語で使用されるレコードまたは構造体を構築するために使用できます。依存型 3 タプルの例としては、2 つの整数と、最初の整数が 2 番目の整数よりも小さいことの証明があり、次の型で記述されます。

${\displaystyle \sum _{m{\mathbin {:}}{\mathbb {Z} }}{\sum _{n{\mathbin {:}}{\mathbb {Z} }}((m<n)={\text{True}})}}$

依存型付けにより、Σ 型は存在量指定子の役割を果たすことができます。「型 の が存在し、 が証明されている」という文は、最初の項目が型 の値で、2 番目の項目が の証明である順序付きペア の型になります。2 番目の項目 ( の証明) の型は、順序付きペアの最初の部分 ( ) の値に依存することに注意してください。その型は次のようになります。 ${\displaystyle n}$${\displaystyle {\mathbb {N} }}$${\displaystyle P(n)}$${\displaystyle n}$${\displaystyle {\mathbb {N} }}$${\displaystyle P(n)}$${\displaystyle P(n)}$${\displaystyle n}$

${\displaystyle \sum _{n{\mathbin {:}}{\mathbb {N} }}P(n)}$

Π 型には関数が含まれます。一般的な関数型と同様に、入力型と出力型で構成されます。ただし、戻り値の型が入力値に依存できるという点で、一般的な関数型よりも強力です。型理論の関数は、集合論とは異なります。集合論では、引数の値を順序付きペアのセットで検索します。型理論では、引数が項に代入され、その項に計算 (「縮約」) が適用されます。

例として、自然数 が与えられると実数を 含むベクトルを返す関数の型は次のように記述されます。${\displaystyle n}$${\displaystyle n}$

${\displaystyle \prod _{n{\mathbin {:}}{\mathbb {N} }}\operatorname {Vec} ({\mathbb {R} },n)}$

出力の型が入力値に依存しない場合、関数の型は単に と表記されることが多いです。したがって、は自然数から実数への関数の型です。このような Π 型は論理的含意に対応します。論理的命題は型 に対応し、A の証明を受け取り B の証明を返す関数を含みます。この型は次のようにより一貫して表記できます。 ${\displaystyle \to }$${\displaystyle {\mathbb {N} }\to {\mathbb {R} }}$${\displaystyle A\implies B}$${\displaystyle A\to B}$

${\displaystyle \prod _{a{\mathbin {:}}A}B}$

Π型は、全称量化の論理でも使用されます。「型 のすべてに対して、が証明されている」という文は、型から の証明への関数になります。したがって、関数の値が与えられた場合、その値に対して成立する証明が生成されます。型は次のようになります。 ${\displaystyle n}$${\displaystyle {\mathbb {N} }}$${\displaystyle P(n)}$${\displaystyle n}$${\displaystyle {\mathbb {N} }}$${\displaystyle P(n)}$${\displaystyle n}$${\displaystyle P(\,\cdot \,)}$

${\displaystyle \prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)}$

=-型は 2 つの項から作成されます。 および のような 2 つの項が与えられた場合、新しい型 を作成できます。その新しい型の項は、そのペアが同じ標準項に簡約されることの証明を表します。したがって、と はどちらも標準項 に計算されるため、型 の項が存在することになります。直観主義型理論では、=-型を導入する方法は 1 つしかなく、それは反射性によるものです。 ${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$${\displaystyle 2+2=2\cdot 2}$${\displaystyle 2+2}$${\displaystyle 2\cdot 2}$${\displaystyle 4}$${\displaystyle 2+2=2\cdot 2}$

${\displaystyle \operatorname {refl} {\mathbin {:}}\prod _{a{\mathbin {:}}A}(a=a).}$

項が同じ標準項に還元されないような = 型を作成することは可能ですが、その新しい型の項を作成することはできません。実際、 の項を作成できた場合は、 の項を作成することもできます。これを関数に入れると、型 の関数が生成されます。 は直観主義型理論による否定の定義方法であるため、または最終的にとなります。 ${\displaystyle 1=2}$${\displaystyle 1=2}$${\displaystyle \bot }$${\displaystyle 1=2\to \bot }$${\displaystyle \ldots \to \bot }$${\displaystyle \neg (1=2)}$${\displaystyle 1\neq 2}$

証明の等価性は証明理論において活発に研究されている分野であり、ホモトピー型理論やその他の型理論の発展につながっています。

帰納的型を使用すると、複雑で自己参照的な型を作成できます。たとえば、自然数の連結リストは、空のリストか、自然数と別の連結リストのペアのいずれかです。帰納的型は、ツリー、グラフなどの無制限の数学的構造を定義するために使用できます。実際、自然数型は、別の自然数 またはその後継として、帰納的型として定義できます。${\displaystyle 0}$

帰納的型は、ゼロや後継関数などの新しい定数を定義します。 には定義がなく、置換を使用して評価できないため、や などの項は自然数の標準的な項になります。 ${\displaystyle 0{\mathbin {:}}{\mathbb {N} }}$${\displaystyle S{\mathbin {:}}{\mathbb {N} }\to {\mathbb {N} }}$${\displaystyle S}$${\displaystyle S0}$${\displaystyle SSS0}$

帰納的型の証明は帰納法によって可能になります。新しい帰納的型にはそれぞれ独自の帰納的規則が伴います。すべての自然数の述語を証明するには、次の規則を使用します。 ${\displaystyle P(\,\cdot \,)}$

${\displaystyle {\operatorname {{\mathbb {N} }-elim} }\,{\mathbin {:}}P(0)\,\to \left(\prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)\to P(S(n))\right)\to \prod _{n{\mathbin {:}}{\mathbb {N} }}P(n)}$

直観主義型理論における帰納的型は、整基礎木の型である W 型に基づいて定義されます。型理論におけるその後の研究では、より不明瞭な種類の自己参照性を持つ型を扱うために、共帰納的型、帰納的再帰、帰納的帰納的型が生成されました。より高次の帰納的型では、項間の等式を定義できます。

ユニバース型は、他の型コンストラクタで作成されたすべての型についての証明を記述することを可能にする。ユニバース型内のすべての項は、 と帰納的型コンストラクタの任意の組み合わせで作成された型にマッピングすることができる。しかし、パラドックスを避けるために、 には任意の に対してにマッピングされる項はない。^[1]${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle 0,1,2,\Sigma ,\Pi ,=,}$${\displaystyle {\mathcal {U}}_{n}}$${\displaystyle {\mathcal {U}}_{n}}$${\displaystyle {\mathcal {n}}\in \mathbb {N} }$

すべての「小さなタイプ」と についての証明を書くには、 を使用する必要があります。これには の項が含まれますが、 自体の項は含まれません。同様に、 についても です。宇宙には述語的階層があるため、任意の固定定数宇宙に対する証明を定量化するには、 を使用できます。 ${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle {\mathcal {U}}_{1}}$${\displaystyle {\mathcal {U}}_{0}}$${\displaystyle {\mathcal {U}}_{1}}$${\displaystyle {\mathcal {U}}_{2}}$${\displaystyle k}$${\displaystyle {\mathcal {U}}_{k+1}}$

宇宙のタイプは、タイプ理論の扱いにくい特徴です。マーティン＝レーフの元のタイプ理論は、ジラールのパラドックスを説明するために変更する必要がありました。その後の研究では、「超宇宙」、「マーロ宇宙」、非予言的宇宙 などのトピックが取り上げられました。

直観主義型理論の正式な定義は、判断を使用して記述されます。たとえば、「が型であり、が型である場合、は型である」というステートメントには、「が型である」、「および」、および「... である場合、...」という判断があります。この表現は判断ではなく、定義される型です。 ${\displaystyle A}$${\displaystyle B}$${\displaystyle \textstyle \sum _{a:A}B}$${\displaystyle \textstyle \sum _{a:A}B}$

型理論のこの第 2 レベルは、特に等価性に関して混乱を招く可能性があります。項の等価性の判断があり、 と表現される場合があります。これは、2 つの項が同じ標準項に簡約されるというステートメントです。型の等価性の判断もあり、 と表現される場合があります。これは、 のすべての要素が型の要素であり、その逆も同様であることを意味します。型レベルでは、と が同じ値に簡約されるという証明がある場合、型があり、その型には項が含まれます。(この型の項は、項の等価性の判断を使用して生成されます。)最後に、英語レベルの等価性があります。これは、標準項 を指すために「4」という単語と記号「 」を使用するためです。このような同義語は、Martin-Löf によって「定義上等しい」と呼ばれます。 ${\displaystyle 4=2+2}$${\displaystyle A=B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle 4=2+2}$${\displaystyle 4}$${\displaystyle 2+2}$${\displaystyle 4}$${\displaystyle SSSS0}$

以下の判断の説明は、Nordström、Petersson、および Smith の議論に基づいています。

形式理論は型とオブジェクトを扱います。

型は次のように宣言されます。

• ${\displaystyle A\ {\mathsf {Type}}}$

次の場合、オブジェクトが存在し、型内にあります。

• ${\displaystyle a{\mathbin {:}}A}$

オブジェクトは等しい

• ${\displaystyle a=b}$

型は同じになる

• ${\displaystyle A=B}$

別の型のオブジェクトに依存する型が宣言されている

• ${\displaystyle (x{\mathbin {:}}A)B}$

置換によって除去される

• ${\displaystyle B[x/a]}$変数を内のオブジェクトに置き換えます。${\displaystyle x}$${\displaystyle a}$${\displaystyle B}$

別の型のオブジェクトに依存するオブジェクトは2つの方法で記述できます。オブジェクトが「抽象化」されている場合は、次のように記述します。

• ${\displaystyle [x]b}$

置換によって除去される

• ${\displaystyle b[x/a]}$変数を内のオブジェクトに置き換えます。${\displaystyle x}$${\displaystyle a}$${\displaystyle b}$

オブジェクトに依存するオブジェクトは、再帰型の一部として定数として宣言することもできます。再帰型の例は次のとおりです。

• ${\displaystyle 0{\mathbin {:}}\mathbb {N} }$
• ${\displaystyle S{\mathbin {:}}\mathbb {N} \to \mathbb {N} }$

ここで、はオブジェクトに依存する定数オブジェクトです。これは抽象化とは関連付けられていません。 のような定数は、等式を定義することで削除できます。ここで、加算との関係は等式を使用して定義され、 の再帰的な側面を処理するためにパターン マッチングを使用します。 ${\displaystyle S}$${\displaystyle S}$${\displaystyle S}$

${\displaystyle {\begin{aligned}\operatorname {add} &{\mathbin {:}}\ (\mathbb {N} \times \mathbb {N} )\to \mathbb {N} \\\operatorname {add} (0,b)&=b\\\operatorname {add} (S(a),b)&=S(\operatorname {add} (a,b)))\end{aligned}}}$

${\displaystyle S}$不透明な定数として操作されます。置換用の内部構造はありません。

したがって、オブジェクトとタイプ、およびこれらの関係は、理論内の式を表現するために使用されます。既存のオブジェクト、タイプ、および関係から新しいオブジェクト、タイプ、および関係を作成するには、次のスタイルの判断が使用されます。

慣例により、他のすべての型を表す型が存在します。これは(または) と呼ばれます。は型なので、そのメンバーはオブジェクトです。各オブジェクトを対応する型にマップする依存型が存在します。ほとんどのテキストでは は記述されません。文の文脈から、読者は が型を参照しているのか、それともが型に対応する のオブジェクトを参照しているのかをほぼ常に判断できます。${\displaystyle {\mathcal {U}}}$${\displaystyle \operatorname {Set} }$${\displaystyle {\mathcal {U}}}$${\displaystyle \operatorname {El} }$${\displaystyle \operatorname {El} }$${\displaystyle A}$${\displaystyle {\mathcal {U}}}$

これが理論の完全な基礎です。他のすべては導き出されたものです。

ロジックを実装するために、各命題には独自の型が与えられます。これらの型のオブジェクトは、命題を証明するさまざまな方法を表します。命題の証明がない場合、型にはオブジェクトがありません。命題に作用する「and」や「or」などの演算子は、新しい型と新しいオブジェクトを導入します。型と型に依存する型 も同様です。その依存型 のオブジェクトは、とのすべてのオブジェクトのペアに対して存在するように定義されます。または に証明がなく、 が空の型である場合、 を表す新しい型も空です。 ${\displaystyle A\times B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A}$${\displaystyle B}$${\displaystyle A\times B}$

これは、他の型 (ブール値、自然数など) とその演算子に対しても実行できます。

RAG Seelyは、カテゴリ理論の言語を使用して、型理論の基本モデルとして局所的カルテシアン閉カテゴリ（LCCC）の概念を導入しました。これは、Cartmellによる以前の研究に基づいて、HofmannとDybjerによってカテゴリとファミリーまたはカテゴリと属性に洗練されました。^[2]

族を持つカテゴリは、コンテキストのカテゴリC (オブジェクトがコンテキストであり、コンテキスト射が置換である) と、関手T  : C ^op → Fam ( Set ) を組み合わせたものです。

Fam ( Set ) は、オブジェクトが「インデックス セット」Aと関数B : X → Aのペアであり、射が関数${\displaystyle (A,B)}$f  : A → A'とg  : X → X'のペアであり、 B' _° g = f _° Bである、つまりf がB _aをB _{g ( a )}にマップする、セットのファミリのカテゴリです。

関数T はコンテキストGに型の集合⁠ ⁠${\displaystyle Ty(G)}$と、各⁠ ⁠${\displaystyle A:Ty(G)}$に対して項の集合⁠ ⁠ ⁠ を割り当てます。関数の公理では、これらが置換と調和して機能することが求められます。置換は通常、 ${\displaystyle Tm(G,A)}$Afまたはafの形式で記述されます。ここで、Aは⁠ ⁠ ⁠${\displaystyle Ty(G)}$の型、aは⁠ ⁠${\displaystyle Tm(G,A)}$の項、f はDからGへの置換です。ここで⁠ ⁠ ⁠${\displaystyle Af:Ty(D)}$および⁠ ⁠${\displaystyle af:Tm(D,Af)}$です。

カテゴリC には、終端オブジェクト (空のコンテキスト) と、右の要素が左の要素のコンテキスト内の型である、内包またはコンテキスト拡張と呼ばれる積の形式の最終オブジェクトが含まれている必要があります。Gがコンテキストであり、⁠ ⁠ で${\displaystyle A:Ty(G)}$ある場合、コンテキストDの間に、マッピングp  : D → G、q  : Tm ( D,Ap ) を持つオブジェクト⁠ ⁠最終が存在する必要があります。${\displaystyle (G,A)}$

Martin-Löf のような論理フレームワークは、コンテキスト依存の型と項の集合に対する閉包条件の形をとります。つまり、Set と呼ばれる型が存在し、各集合に型が存在し、型は従属する和と積の形式で閉じている必要がある、などです。

述語集合論などの理論は、集合の種類とその要素に関する閉包条件を表現します。つまり、それらは従属的な和と積を反映する演算と、さまざまな形式の帰納的定義の下で閉じていなければならないということです。

基本的な違いは、外延型理論と内包型理論である。外延型理論では、定義的（つまり計算的）等価性は、証明を必要とする命題的等価性と区別されない。結果として、外延型理論では、理論内のプログラムが終了しない可能性があるため、型チェックは決定不能になる。たとえば、そのような理論では、Yコンビネータに型を与えることができる。この詳細な例は、NordstömとPeterssonの「Martin-Löfの型理論におけるプログラミング」に記載されている。^[3]しかし、これは外延型理論が実用的なツールの基礎となることを妨げるものではない。たとえば、Nuprlは外延型理論に基づいている。

対照的に、内包的型理論では型チェックは決定可能であるが、内包的推論にはsetoidsまたは類似の構造を使用する必要があるため、標準的な数学概念の表現はやや面倒である。これなしでは扱いにくい、または表現できない一般的な数学的対象は多数あり、たとえば整数、有理数、実数などである。整数と有理数はsetoidsなしで表現できるが、この表現は扱いが難しい。コーシー実数はこれなしでは表現できない。^[4]

ホモトピー型理論は、この問題の解決に取り組んでいます。これにより、高次の帰納的型を定義できるようになります。これは、1 階のコンストラクタ (値またはポイント) だけでなく、要素間の等式 (パス)、等式間の等式 (ホモトピー)など、高次のコンストラクタを無限に定義します。

さまざまな形式の型理論が、数多くの証明支援系の基礎となる形式システムとして実装されてきました。多くはペル・マルティン＝レーフのアイデアに基づいていますが、機能の追加、公理の追加、または異なる哲学的背景を持つものも多くあります。たとえば、Nuprlシステムは計算型理論^[5]に基づいており、Coqは(共)帰納的構成の計算に基づいています。依存型は、 ATS、Cayenne、Epigram、Agda、^[6]、Idrisなどのプログラミング言語の設計にも取り入れられています。^[7]

Per Martin-Löf は、さまざまな時期に発表されたいくつかの型理論を構築しました。そのうちのいくつかは、その説明が記載されたプレプリントが専門家 ( Jean-Yves Girardや Giovanni Sambin など) に公開されるよりもずっと後のものでした。以下のリストは、印刷された形式で説明されているすべての理論をリストし、それらを互いに区別する主要な特徴を概説しようと試みたものです。これらすべての理論には、従属積、従属和、非結合​​和、有限型、自然数がありました。すべての理論には、従属積または従属和のいずれにも η 簡約を含まない同じ簡約規則がありましたが、MLTT79 では従属積の η 簡約が追加されました。

MLTT71 は、Per Martin-Löf によって作成された最初の型理論です。1971 年にプレプリントで発表されました。MLTT71 には 1 つの宇宙がありましたが、この宇宙自体に名前がありました。つまり、今日では「Type in Type」と呼ばれている型理論でした。Jean -Yves Girard はこのシステムに一貫性がないことを示し、プレプリントは公開されませんでした。

MLTT72 は、現在出版されている 1972 年のプレプリントで発表されました。^[8]その理論には、宇宙 V が 1 つあり、恒等型(=-型) はありませんでした。宇宙は、Vのオブジェクトの族と、たとえば V 自体のような V に含まれないオブジェクトとの従属積が、V に含まれるとは想定されないという意味で、「述語的」でした。宇宙はラッセルの『プリンキピア・マテマティカ』風で、つまり、「T∈V」や「t∈T」と直接書きます (Martin-Löf は、現代の「:」の代わりに「∈」記号を使用します)。つまり、「El」などの構成子を追加せずに書きます。

MLTT73 は、ペル・マルティン＝レーフが発表した型理論の最初の定義でした（論理コロキウム '73 で発表され、1975 年に出版されました^[9]）。彼が「命題」と表現する恒等型がありますが、命題とその他の型の間に実際の区別が導入されていないため、その意味は不明瞭です。後に J エリミネーターという名前が付けられるが、まだ名前がないものがあります（94 ～ 95 ページを参照）。この理論には、宇宙の無限列 V ₀、...、V _n、... があります。宇宙は、ラッセル風に述語的であり、非累積的です。実際、115 ページの系 3.10 では、 A∈V _mおよび B∈V _nが A と B が変換可能であるようなものである場合、 m  =  nであると述べています。これは、例えば、この理論でユニバレンシー公理を定式化することが難しいことを意味します。つまり、 V _iのそれぞれに縮約可能な型がありますが、 i ≠ jに対してV _iと V _{j を}接続する恒等型が存在しないため、それらを等しいと宣言する方法が不明です。

MLTT79は1979年に発表され、1982年に出版されました。^[10]この論文で、マーティン=レーフは依存型理論の判断の4つの基本的なタイプを導入しました。これはその後、そのようなシステムのメタ理論の研究の基礎となりました。彼はまた、その中でコンテキストを別の概念として導入しました（161ページを参照）。Jエリミネーター（MLTT73にすでに登場していましたが、この名前はありませんでした）を持つ同一性型がありますが、理論を「外延的」にする規則を持つ同一性型もあります（169ページ）。W型があります。累積的な述語宇宙の無限シーケンスがあります。

ビブリオポリス： 1984年のビブリオポリスという本には型理論についての議論があるが^[11] 、それはいくぶんオープンエンドであり、特定の選択肢のセットを表しているようには見えないため、それに関連する特定の型理論はない。

• 直観主義論理
• 型付きラムダ計算

• Martin-Löf, ペル州;サンビン、ジョバンニ (1984)。直観主義的タイプ理論(PDF)。ナポリ：ビブリオポリス。ISBN 978-8870881059. OCLC  12731401.

• Martin-Löf のノートによると、Giovanni Sambin が記録 (1980 年)
• ノードストローム、ベングト。ケント州ピーターソン。スミス、ヤン・M. (1990)。 Martin-Löf の型理論でのプログラミング。オックスフォード大学出版局。ISBN 9780198538141。
• トンプソン、サイモン (1991)。型理論と関数型プログラミング。Addison- Wesley。ISBN 0-201-41667-0。
• グランストロム、ヨハン G. (2011)。直観主義的型理論に関する論文。スプリンガー。ISBN 978-94-007-1735-0。

• EU タイプ プロジェクト: チュートリアル - タイプ サマー スクール 2005 の講義ノートとスライド
• n-カテゴリー - 定義の概要 -ジョン・バエズとジェームズ・ドランからロス・ストリートへの手紙、1995 年 11 月 29 日