ホモトピー型理論
[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\)連結であると言う。