\(\mathbf {1}\)は可縮である。実際、\(\mathord {\textnormal {\textsf {record}}}\mathopen {\{ \negmedspace |}\mathord {\textnormal {\textsf {center}}}\equiv \mathord {\star },\mathord {\textnormal {\textsf {contr}}}\equiv \lambda x.\mathord {\textnormal {\textsf {refl}}}\mathclose {|\negmedspace \} }:\mathord {\textnormal {\textsf {IsContr}}}(\mathbf {1})\)を確かめられる。