[000S] 可縮性

可縮性はホモトピー型理論において中心的な役割を果たす概念である。

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型とする。型 $\mathord {\textnormal {\textsf {IsContr}}}(A):\mathcal {U}(i)$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {center}}}:A$
- $\mathord {\textnormal {\textsf {contr}}}:\prod _{x:A}\mathord {\textnormal {\textsf {center}}}=x$

\mathord {\textnormal {\textsf {IsContr}}}(A)

の要素がある時、

\(A\)

は可縮(contractible)であると言う。

つまり、型 $$A$$ が可縮であるとは、ある要素 $\mathord {\textnormal {\textsf {center}}}:A$ があり、すべての $$A$$ の要素は $\mathord {\textnormal {\textsf {center}}}$ と同一視されるということである。やや非形式的に言うと、 $$A$$ はただ一つの要素を持つということである。

後に示すことだが、 $\mathord {\textnormal {\textsf {IsContr}}}(A)$ の任意の二つの要素は(関数外延性の下で)同一視される([0042])。したがって、 $$A$$ が可縮であると言った場合、 $\mathord {\textnormal {\textsf {IsContr}}}(A)$ の要素があることは重要だが、その要素の具体的な定義は気にしなくてよい。あるいは、可縮性は型についての命題であり、それを証明できることは重要だがどのように証明されたかは重要ではないとも言える。

[001O] 例

$\mathbf {1}$ は可縮である。実際、 $\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {center}}}\equiv \mathord {\star },\mathord {\textnormal {\textsf {contr}}}\equiv \lambda x.\mathord {\textnormal {\textsf {refl}}}\mathclose {|\negmedspace \} }:\mathord {\textnormal {\textsf {IsContr}}}(\mathbf {1})$ を確かめられる。

型は∞グルーポイドの構造を持っているので、ただ一つの要素を持つとはいっても異なる同一視のしかたがある可能性が懸念される。次の[001L]は、可縮性は見た目よりもずっと強い条件で、任意の二つの要素の同一視もただ一つだけあることを示す。[001L]を繰り返し使えば、任意に高次の同一視もただ一つだけあることが分かる。

[001L] 命題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $a_{1},a_{2}:A$ を要素とする。 $$A$$ が可縮ならば $a_{1}=a_{2}$ も可縮である。

証明

$c:\mathord {\textnormal {\textsf {IsContr}}}(A)$ と仮定する。要素 $p:a_{1}=a_{2}$ と $q:\prod _{z:a_{1}=a_{2}}p=z$ を構成すればよい。仮定 $$c$$ より $a_{0}:A$ と $r:\prod _{x:A}a_{0}=x$ を得る。 $p\equiv \mathord {\textnormal {\textsf {ext}}}(r(a_{1}),r(a_{2}))$ と定義する。 $$q$$ については、一般化したもの $q':\prod _{x:A}\prod _{z:a_{1}=x}\mathord {\textnormal {\textsf {ext}}}(r(a_{1}),r(x))=z$ を構成し、 $q\equiv q'(a_{2})$ と定義する。同一視型の帰納法により、要素 $s:\mathord {\textnormal {\textsf {ext}}}(r(a_{1}),r(a_{1}))=\mathord {\textnormal {\textsf {refl}}}$ を構成すればよいが、これは[001M]で構成した。

型の可縮性は次の[001N]や[001K]を使って示される場合が多い。

[001N] 命題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $$a:A$$ を要素とする。型 $\sum _{x:A}a=x$ は可縮である。

証明

要素 $c:\sum _{x:A}a=x$ と $r:\prod _{z:\sum _{x:A}a=x}c=z$ を構成すればよい。 $c\equiv \mathord {\textnormal {\textsf {pair}}}(a,\mathord {\textnormal {\textsf {refl}}})$ と定義する。 $$r$$ については、カリー化([0014])により、 $\prod _{x:A}\prod _{w:a=x}c=\mathord {\textnormal {\textsf {pair}}}(x,w)$ の要素を構成すればよい。同一視型の帰納法により、 $c=\mathord {\textnormal {\textsf {pair}}}(a,\mathord {\textnormal {\textsf {refl}}})$ の要素を構成すればよいが、 $$c$$ の定義より $\mathord {\textnormal {\textsf {refl}}}$ とすればよい。

[001N]は同一視型の帰納法の別表現と考えられる。同一視型の帰納法は型の族 $\lambda x.(a=x):A\to \mathcal {U}(i)$ が $\mathord {\textnormal {\textsf {refl}}}:a=a$ で自由に生成されることを表す。これは、対型 $\sum _{x:A}a=x$ が $\mathord {\textnormal {\textsf {pair}}}(a,\mathord {\textnormal {\textsf {refl}}})$ で自由に生成されると言い換えられる。一つの要素で生成される型はその要素しか持たないと期待され、[001N]は実際にそうだと言っている。

[001K]は可縮性がレトラクトで閉じることを主張する。

[001J] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型とする。型 $\mathord {\textnormal {\textsf {Retract}}}(A,B):\mathcal {U}(i)$ を次のレコード型と定義する。

- $\mathord {\textnormal {\textsf {retraction}}}:B\to A$
- $\mathord {\textnormal {\textsf {section}}}:A\to B$
- $\mathord {\textnormal {\textsf {r-s}}}:\prod _{x:A}\mathord {\textnormal {\textsf {retraction}}}(\mathord {\textnormal {\textsf {section}}}(x))=x$

\mathord {\textnormal {\textsf {Retract}}}(A,B)

は

A\triangleleft B

と書くこともある。

A\triangleleft B

の要素がある時、

\(A\)

は

\(B\)

のレトラクト(retract)であると言う。また、

A\mathrel {\triangleleft \triangleright }B

を

(A\triangleleft B)\times (B\triangleleft A)

と定義する。

$\mathord {\textnormal {\textsf {Retract}}}(A,B)$ は $\mathord {\textnormal {\textsf {IsContr}}}(A)$ と違って命題ではないが、実用上は $\mathord {\textnormal {\textsf {Retract}}}(A,B)$ の要素の具体的な定義は重要ではない場合が多い。これは[001K]のように、ある性質がレトラクトで閉じるという使われ方をする場合が多いからである。

[001K] 命題

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $r:\mathord {\textnormal {\textsf {Retract}}}(A,B)$ を要素とする。 $$B$$ が可縮ならば $$A$$ も可縮である。

証明

$d:\mathord {\textnormal {\textsf {IsContr}}}(B)$ と仮定する。要素 $$a:A$$ と $p:\prod _{x:A}a=x$ を構成すればよい。仮定 $$d$$ から $$b:B$$ と $q:\prod _{y:B}b=y$ を得る。仮定 $$r$$ から $f:B\to A$ と $g:A\to B$ と $t:\prod _{x:A}f(g(x))=x$ を得る。 $a\equiv f(b)$ と定義する。 $$p$$ を定義するために、 $$x:A$$ を仮定する。 $$q(g(x)):b=g(x)$$ と $$t(x):f(g(x))=x$$ に注意して、 $p(x)\equiv t(x)\circ \mathord {\textnormal {\textsf {ap}}}(f,q(g(x)))$ と定義すればよい。

可縮性を使って型の同値が定義される。

[001P] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数、 $$b:B$$ を要素とする。型 $\mathord {\textnormal {\textsf {Fiber}}}(f,b):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {elem}}}:A,\mathord {\textnormal {\textsf {id}}}:f(\mathord {\textnormal {\textsf {elem}}})=b\mathclose {|\negmedspace \} }$ と定義する。

[001Q] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。型 $\mathord {\textnormal {\textsf {IsEquiv}}}(f):\mathcal {U}(i)$ を $\prod _{y:B}\mathord {\textnormal {\textsf {IsContr}}}(\mathord {\textnormal {\textsf {Fiber}}}(f,y))$ と定義する。 $\mathord {\textnormal {\textsf {IsEquiv}}}(f)$ の要素がある時、 $$f$$ は同値(equivalence)であると言う。

[000V] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型とする。型 $A\simeq B:\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {Record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {fun}}}:A\to B,\mathord {\textnormal {\textsf {is-equiv}}}:\mathord {\textnormal {\textsf {IsEquiv}}}(\mathord {\textnormal {\textsf {fun}}})\mathclose {|\negmedspace \} }$ と定義する。

この定義による同値の概念が妥当なものであるかは自明ではない。直観的には、 $\mathord {\textnormal {\textsf {Fiber}}}(f,b)$ は $$b$$ の $$f$$ による逆像であり、 $\mathord {\textnormal {\textsf {IsContr}}}(\mathord {\textnormal {\textsf {Fiber}}}(f,b))$ は逆像がただ一つの要素を持つことを表す。これはもっともらしい定義だが、 $\simeq$ が反射的、対称、推移的であることすら[000V]から直ちに分かることではない。[000U]でこの同値の概念が妥当であることを説明するが、その前にいくつか重要な定理と概念を導入する。