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