\(i\)を階数、\(A:\mathcal {U}(i)\)を型とする。型\(\mathord {\textnormal {\textsf {IsContr}}}(A):\mathcal {U}(i)\)を次のレコード型と定義する。

• -\(\mathord {\textnormal {\textsf {center}}}:A\)
• -\(\mathord {\textnormal {\textsf {contr}}}:\prod _{x:A}\mathord {\textnormal {\textsf {center}}}=x\)

\(\mathord {\textnormal {\textsf {IsContr}}}(A)\)の要素がある時、\(A\)は可縮(contractible)であると言う。