関数外延性と一価性を仮定する。\(i\)を階数、\(A:\mathord {\textnormal {\textsf {Span}}}(i)\)をスパン、\(B:\mathord {\textnormal {\textsf {SpanOver}}}(A)\)を\(A\)上のスパン、\(C:\mathord {\textnormal {\textsf {Cocone}}}(A)\)を余錐とする。\(B\)がカルテシアンで、\(C\)が普遍余錐であると仮定すると、型

\(\lbrace D:\mathord {\textnormal {\textsf {CoconeOver}}}(B,C)\mid \mathord {\textnormal {\textsf {IsCart}}}(D)\rbrace \)は可縮である。さらに、一意に存在するカルテシアンな\(D:\mathord {\textnormal {\textsf {CoconeOver}}}(B,C)\)に対して、\(\mathord {\textnormal {\textsf {Total}}}(D):\mathord {\textnormal {\textsf {Cocone}}}(\mathord {\textnormal {\textsf {Total}}}(B))\)は普遍余錐である。