[005T] 連結性

$$n$$ 型は $$n$$ 次元より上の構造が自明な型であったが、逆に $$n$$ 次元以下の構造が自明な型を導入する。

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。型 $\mathord {\textnormal {\textsf {IsConnected}}}(n,A):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {IsContr}}}({\| A\| }_{n})$ と定義する。 $\mathord {\textnormal {\textsf {IsConnected}}}(n,A)$ の要素がある時、 $$A$$ は $$n$$ 連結( $$n$$ -connected)であると言う。

[005V] 定義

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

[005W] 注意

[005V]の意味での $$n$$ 連結関数は古典的なホモトピー論における $$n+1$$ 連結写像に対応するものである。

[005X] 命題

$$i$$ を階数、 $A:\mathcal {U}(i)$ を型、 $n:\mathord {\textnormal {\textsf {TruncLevel}}}$ を要素とする。 $$A$$ が $$n$$ 型かつ $$n$$ 連結ならば、 $$A$$ は可縮である。

証明

[0051]から従う。

定義から、任意の関数は $$-2$$ 連結である。 $$-1$$ 連結な関数は全射であると考える。

[005Z] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。型 $\mathord {\textnormal {\textsf {IsSurj}}}(f):\mathcal {U}(i)$ を $\forall _{y:B}\exists _{x:A}f(x)=y$ と定義する。 $\mathord {\textnormal {\textsf {IsSurj}}}(f)$ の要素がある時、 $$f$$ は全射(surjection)であると言う。

[0074] 命題

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。次は論理的に同値である。

1 $$f$$ は全射である。
2 $$f$$ は $$-1$$ 連結である。

証明

$$y:B$$ を要素とする。[0041]より、 ${\| \mathord {\textnormal {\textsf {Fiber}}}(f,y)\| }_{-1}$ と $\mathord {\textnormal {\textsf {IsContr}}}({\| \mathord {\textnormal {\textsf {Fiber}}}(f,y)\| }_{-1})$ は論理的に同値であるから主張が従う。