[0002] 一価性公理

一価性公理(univalence axiom)はホモトピー型理論において最も重要な公理で、型理論をまさに「ホモトピー論的」なものに強制する公理である。非形式的には、型\(A,B:\mathcal {U}(i)\)に対して同一視型\(A=B\)と同値のなす型\(A\simeq B\)が同値になることを要請する。

一価性について述べるには同値の概念が不可欠である。同値の定義はいくつか考えられるが、本書では関数であって各点の逆像が可縮であるものという定義を採用する。型が可縮であるとは非形式的には要素をただ一つ持つということであり、この同値の定義は直観的にも自然であろう。技術的な利点として、可縮性は非常に扱いやすい性質であるという点、ホモトピー型理論における他の概念も可縮性を軸に定義することができるという点がある。[000S]で可縮性についての基本事項まとめる。

一価性公理は宇宙\(\mathcal {U}(i)\)の同一視型の特徴付けを与えているとも解釈できる。諸々の型の同一視型の特徴付けについての一般論として、同一視型の基本定理を[001R]で証明する。「基本定理」と名付けられる通り、この定理は本書の至る所で使われる。[000X]で一価性公理を導入する。また、関数型の同一視型の特徴付け(いわゆる関数外延性)にもなんらかの公理が必要であることが知られているので、[001Y]で関数外延性公理を導入する。

一価性公理は後に導入する高次帰納的型と合わせてその真価を発揮するのだが、一価性公理だけでもいくつか興味深い帰結を得られる。その一つは構造同一原理(structure identity principle)と呼ばれるもので、なんらかの数学的構造の同一視型はその構造を保つ同値の型と同値であるという原理である。構造同一原理を一般的に述べるには「構造」とは厳密にどう定義されるかという問題が大きいので立ち入らず、[0022]でいくつかの例を挙げるにとどめる。

[000U]はやや技術的な話で、同値の概念の基本性質を見る。