\(i\)を階数、\(A,B:\mathcal {U}(i)\)を型、\(f:A\to B\)を関数、\(n:\mathord {\textnormal {\textsf {TruncLevel}}}\)を要素とする。型\(\mathord {\textnormal {\textsf {IsTruncMap}}}(n,f):\mathcal {U}(i)\)を\(\prod _{y:B}\mathord {\textnormal {\textsf {IsTrunc}}}(n,\mathord {\textnormal {\textsf {Fiber}}}(f,y))\)と定義する。