[000C] 同一視型

同一視型はホモトピー型理論において最も特徴的な型である。

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $a_{1}:A$ を要素とする。

-要素 $a_{2}:A$ に対し、同一視型(identity type) $a_{1}=a_{2}:\mathcal {U}(i)$ を構成できる。 $a_{1}=a_{2}$ の要素を $a_{1}$ と $a_{2}$ の同一視(identification)と呼ぶ。
-要素 $\mathord {\textnormal {\textsf {refl}}}\lbrace a_{1}\rbrace :a_{1}=a_{1}$ を構成できる。
- $a_{2}:A$ と $p:a_{1}=a_{2}$ を要素、 $$j$$ を階数、 $B:\prod _{\lbrace x:A\rbrace }a_{1}=x\to \mathcal {U}(j)$ を型の族、 $b:B(\mathord {\textnormal {\textsf {refl}}})$ を要素とすると、要素 $\mathord {\textnormal {\textsf {ind}}}_{=}(p,B,b):B(p)$ を構成できる。
- $$j$$ を階数、 $B:\prod _{\lbrace x:A\rbrace }a_{1}=x\to \mathcal {U}(j)$ を型の族、 $b:B(\mathord {\textnormal {\textsf {refl}}})$ を要素とすると、 $\mathord {\textnormal {\textsf {ind}}}_{=}(\mathord {\textnormal {\textsf {refl}}},B,b)\equiv b$ と定義される。

[HoTT-Book]にならって同一視型に等号の記号を使うが、その意味は従来の数学の等号とは大きく異なる。従来の数学では、 $a_{1}=a_{2}$ といえば $a_{1}$ と $a_{2}$ が等しいという命題であるが、型理論では $a_{1}=a_{2}$ はあくまで型である。従って、 $a_{1}=a_{2}$ の要素というものを考えることができ、それは非形式的には $a_{1}$ と $a_{2}$ の同一視のしかたと解釈される。

[000P]について説明する。 $\mathord {\textnormal {\textsf {refl}}}:a_{1}=a_{1}$ は $a_{1}$ とそれ自身の自明な同一視を表す。残りの規則はいわゆる帰納法原理の一例で、任意の $a_{2}:A$ と同一視型の要素 $p:a_{1}=a_{2}$ を使ってなんらかを構成するためには $$p$$ が $\mathord {\textnormal {\textsf {refl}}}$ の場合の構成( $b:B(\mathord {\textnormal {\textsf {refl}}})$ )を与えれば十分であると読める。注意するべきこととして、この帰納法原理から $a_{1}=a_{1}$ の要素は $\mathord {\textnormal {\textsf {refl}}}$ しか無いことは導出されない。同一視型の規則の正しい読み方は型の族 $\lambda x.(a_{1}=x):A\to \mathcal {U}(i)$ が $\mathord {\textnormal {\textsf {refl}}}:a_{1}=a_{1}$ で自由に生成されることであって、個々の型 $a_{1}=a_{2}$ については特に言えることはない。

同一視型からの関数を定義するにはパターンマッチが便利である。パターンマッチは一般に帰納的型からの関数を構成子による場合分けで定義する手法である。同一視型の構成子は $\mathord {\textnormal {\textsf {refl}}}$ だけなのでその場合の定義だけを与えれば関数を定義できることになる。

[008D] 記法

$\mathord {\textnormal {\textsf {ind}}}_{=}$ を使って関数を定義するには次のいずれかのような言い回しをする。

-関数 $f:\prod _{\lbrace x:A\rbrace }\prod _{p:a_{1}=x}B(p)$ を $\lambda (x,p).\mathord {\textnormal {\textsf {ind}}}_{=}(p,B,b)$ と定義する。
-関数 $f:\prod _{\lbrace x:A\rbrace }\prod _{p:a_{1}=x}B(p)$ を $f(\mathord {\textnormal {\textsf {refl}}})\equiv b$ で定義する。
- $$x:A$$ を要素、 $p:a_{1}=x$ を同一視とする。要素 $$f(p):B(p)$$ を $f(\mathord {\textnormal {\textsf {refl}}})\equiv b$ で定義する。

パターンマッチが有効なのはもちろん $\mathord {\textnormal {\textsf {ind}}}_{=}$ を使ったものに書き直せる時だけである。例えば、「関数 $f:a=a\to B$ を $f(\mathord {\textnormal {\textsf {refl}}})\equiv b$ と定義する」という使い方はできない。

$a_{1}=a_{2}$ が同一視型と呼ぶに価することを確認するために、いくつかの期待される関数を構成しよう。

[001C] 定義

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $$j$$ を階数、 $B:A\to \mathcal {U}(j)$ を型の族とする。 $a_{1},a_{2}:A$ と $p:a_{1}=a_{2}$ を要素とする。輸送関数(transport function)

\mathord {\textnormal {\textsf {transport}}}(B,p):B(a_{1})\to B(a_{2})

を

\mathord {\textnormal {\textsf {transport}}}(B,\mathord {\textnormal {\textsf {refl}}})\equiv \mathord {\textnormal {\textsf {id}}}

で定義する。

[001G] 比較

述語論理において、 $$B$$ を一変数の述語とすると、 $x_{1}=x_{2}\to B(x_{1})\to B(x_{2})$ が成り立つ。これは等しい対象は述語によって区別できないことを表す。[001C]はこの類似で、型理論においては同一視される要素を型の族では区別できないことを表す。

[001D] 定義

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $a_{0},a_{1},a_{2}:A$ を要素、 $p_{1}:a_{0}=a_{1}$ と $p_{2}:a_{0}=a_{2}$ を同一視とする。同一視 $\mathord {\textnormal {\textsf {ext}}}(p_{1},p_{2}):a_{1}=a_{2}$ を $\mathord {\textnormal {\textsf {transport}}}(\lambda x.(x=a_{2}),p_{1},p_{2})$ と定義する。

[001E] 定義

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型とする。

-関数 $\mathord {\textnormal {\textsf {sym}}}:\prod _{\lbrace x_{1},x_{2}:A\rbrace }x_{1}=x_{2}\to x_{2}=x_{1}$ を $\lambda (x_{1},x_{2},z).\mathord {\textnormal {\textsf {ext}}}(z,\mathord {\textnormal {\textsf {refl}}})$ と定義する。 $\mathord {\textnormal {\textsf {sym}}}(p)$ を ${p}^{-1}$ とも書く。
-関数 $\mathord {\textnormal {\textsf {trans}}}:\prod _{\lbrace x_{1},x_{2},x_{3}:A\rbrace }x_{1}=x_{2}\to x_{2}=x_{3}\to x_{1}=x_{3}$ を $\lambda (x_{1},x_{2},x_{3},z,w).\mathord {\textnormal {\textsf {ext}}}({z}^{-1},w)$ と定義する。 $\mathord {\textnormal {\textsf {trans}}}(p,q)$ を $q\circ p$ とも書く。

[001H] 比較

述語論理において、対称律 $x_{1}=x_{2}\to x_{2}=x_{1}$ と推移律 $x_{1}=x_{2}\to x_{2}=x_{3}\to x_{1}=x_{3}$ が成り立つ。[001E]はこの類似である。ちなみに、 $\mathord {\textnormal {\textsf {refl}}}:x=x$ は反射律とも思える。

[001F] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。関数

\mathord {\textnormal {\textsf {ap}}}(f):\prod _{\lbrace x_{1},x_{2}:A\rbrace }x_{1}=x_{2}\to f(x_{1})=f(x_{2})

を

\lambda (x_{1},x_{2},z).\mathord {\textnormal {\textsf {transport}}}(\lambda x.(f(x_{1})=f(x)),z,\mathord {\textnormal {\textsf {refl}}})

と定義する。文脈上わかる場合は、

\mathord {\textnormal {\textsf {ap}}}(f,p)

のことを

\(f(p)\)

と書いてしまうこともある。

[001I] 比較

述語論理において、 $$f$$ を一変数の関数とすると、 $x_{1}=x_{2}\to f(x_{1})=f(x_{2})$ が成り立つ。これは関数が等しさを保つことを表す。[001F]はこの類似で、型理論において関数は同一視を保つことを表す。