アイデンティティタイプ

型理論では、恒等型は等式の概念を表す。これは「判断的等式」と区別するために命題的等式とも呼ばれる。型理論における等式は複雑なトピックであり、ホモトピー型理論などの分野で研究されてきた。^[1]

同一性型は、型理論における2つの異なる平等の概念のうちの1つです。^[2] より基本的な概念は「判断的平等」であり、これは判断です。

恒等型は、判断的等価性でできること以上のことができます。判断的等価性では示せない「すべてに対して」を示すために使用できます。これは、「R」と呼ばれる自然数の除去子 (または「再帰子」) を使用して実現されます。 ${\displaystyle x,x+1=1+x}$

「R」関数を使用すると、自然数に関する新しい関数を定義できます。その新しい関数「P」は、「(λ x:nat . x+1 = 1+x)」と定義されます。他の引数は、帰納的証明の各部分のように機能します。引数「PZ : P 0」は基本ケース「0+1 = 1+0」になり、これは「refl nat 1」という用語です。引数「PS : P n → P (S n)」は帰納的ケースになります。基本的に、これは、「x+1 = 1+x」の「x」が標準値に置き換えられると、式は「refl nat (x+1)」と同じになることを意味します。

アイデンティティ型は複雑で、型理論の研究対象です。すべてのバージョンでコンストラクタ「refl」は一致していますが、そのプロパティとエリミネータ関数は大きく異なります。

「外延的」バージョンでは、任意のアイデンティティ型を判断的等式に変換できます。計算バージョンは、トーマス・シュトライヒャーによる「公理 K」として知られています。^[3] これらは最近あまり人気がありません。

マーティン・ホフマンとトーマス・シュトライヒャーは、イデア型理論では同一性型のすべての項が同じでなければならないと主張した。^[4]

恒等型に関する研究でよく使われる分野としては、ホモトピー型理論^[5]とその立方体型理論がある。