ホモトピー型理論
[005U] 定義

\(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)であると言う。