IDタイプの証明との関連性

Aug 23 2020

建設的な型理論では、外延的アイデンティティタイプと内包的アイデンティティタイプを区別します。拡張IDタイプの住民は定数であるため、拡張IDタイプが証明とは無関係であることは自明です。$\textsf{eq}:\textsf{Eq}(a,b,A)$ (にとって $a,b:A$ そして $a=b:A$)。内包的アイデンティティタイプに関して、2つの質問があります。

  1. しましょう $A$ 任意のタイプであり、内包的アイデンティティタイプです $\textsf{Id}(a,b,A)$ (にとって $a,b:A$ そして $a=b:A$)証明とは無関係ですか?

  2. しましょう $A$ 証明に関係のないタイプである、 $\textsf{Id}(a,b,A)$ (にとって $a,b:A$ そして $a=b:A$)証明とは無関係ですか?

注:タイプ $A$ 証拠とは無関係であると言われています $A$ 満たす: $(\Pi x,y:A)\textsf{Id}(x,y,A)$

前もって感謝します!

回答

3 AndrásKovács Aug 23 2020 at 18:00

𝐴を任意のタイプとします。内包的アイデンティティタイプ𝖨𝖽(𝑎、𝑏、𝐴)(𝑎、𝑏:𝐴および𝑎=𝑏:𝐴)は証明とは無関係ですか?

これは、内包型理論では証明または反証できません。それを公理(ID証明の一意性、UIP)として追加することも、否定を意味する公理を追加することもできます。外延型理論は前者を行い、ホモトピー型理論は後者を行います。HoTTの一価公理は、UIPの否定を意味します。

𝐴を証明に関係のないタイプとします。𝖨𝖽(𝑎、𝑏、𝐴)(𝑎、𝑏:𝐴および𝑎=𝑏:𝐴の場合)証明に関係ありませんか?

はい。より一般的な扱いについては、HoTT本の補題3.3.4 、または第7章を参照してください。

一般に、タイプにはhレベルがあり、IDタイプの関連情報の量を測定します。レベル$0$ ユニットタイプと同等のタイプとレベルがあります $(n+1)$IDタイプがレベルnのタイプがあります。本では、レベルはから始まります$-2$ 歴史的な理由で、しかし時々人々はから始めます $0$。タイプがレベルにある場合$n$、それもレベルにあります $(n + 1)$、したがって、そのIDタイプもレベルにあります $n$。レベルにあるので$1$ は証明に関係がないことと同じであり、証明に関係のないタイプには証明に関係のないIDタイプがあります。

hレベルに関するこれらの結果は、HoTT固有の機能を必要とせずに、単純な内包型理論に当てはまります。