\(i\)を階数、\(A:\mathcal {U}(i)\)を型とすると、関数\(\mathord {\textnormal {\textsf {id}}}:A\to A\)は同値である。
[000X] 一価性
同値\(A\simeq B\)は型\(A,B:\mathcal {U}(i)\)の「正しい」同一視のしかたと考えられる。つまり、同値\((A=B)\simeq (A\simeq B)\)が期待される。しかし、関数\(A\simeq B\to A=B\)は宇宙、関数型、対型、同一視型の規則からは導出できない。実際、型を従来の意味での集合と解釈するモデルを考えると、\(A\simeq B\)は\(A\)から\(B\)への全単射のなす集合と解釈される一方、\(A=B\)は\(A\)と\(B\)が等しい時に限り(一つだけ)要素を持つような集合と解釈される。異なる集合の間にも全単射は存在する場合があり、その時には関数\(A\simeq B\to A=B\)は存在しない。
一価性公理は同値\((A=B)\simeq (A\simeq B)\)を導出する公理である。先に説明したように、この同値は型理論の集合論的解釈とは相反するものである。一価性公理の下では、型は空間のホモトピー型のように振る舞う。その意味で、一価性公理は型理論をホモトピー論的なものに強制する公理と言える。
\(i\)を階層とする。宇宙\(\mathcal {U}(i)\)が一価性(univalence)を満たすとは、\(\prod _{X:\mathcal {U}(i)}\mathord {\textnormal {\textsf {IsContr}}}(\sum _{Y:\mathcal {U}(i)}X\simeq Y)\)の要素があることである。
[0026]から[001S]を適用できて、\(\mathcal {U}(i)\)が一価性を満たす時、任意の型\(A,B:\mathcal {U}(i)\)に対して同値\((A=B)\simeq (A\simeq B)\)を構成できる。
一価性公理(univalence axiom)は任意の階数の宇宙が一価性を満たすことを要請する。
ここで公理という言葉を使ったが、規則と公理に本質的な違いは無い。つまり、[000Z]は任意の階数\(i\)に対して要素\(\mathord {\textnormal {\textsf {ua}}}(i):\prod _{X:\mathcal {U}(i)}\mathord {\textnormal {\textsf {IsContr}}}(\sum _{Y:\mathcal {U}(i)}X\simeq Y)\)を構成できるという規則だとも言える。本書では、次のように感覚的に使い分ける。
- -規則は新しい型の種類を導入する際に使われ、その型が何なのかを説明するものである。例えば[000H]は関数型を説明するための規則だが、\(\mathord {\textnormal {\textsf {ua}}}(i)\)は複合的な型の要素でしかなく、新しい型を説明するものではない。
- -規則は導入した後はいつでも暗黙的に使うが、公理を使用する際は明示する。これは公理がどのように使われるかを強調するためというのもあるが、相反する公理を導入する可能性も考えると公理を大域的に仮定するのは良くないというのがある。あるいは、規則は型理論の基盤にあたるものだが公理は選択的な機能だと言ってもよい。