\(i\)を階数、\(A:\mathord {\textnormal {\textsf {Span}}}(i)\)をスパン、\(B:\mathord {\textnormal {\textsf {SpanOver}}}(A)\)を\(A\)上のスパンとする。型\(\mathord {\textnormal {\textsf {IsCart}}}(B):\mathcal {U}(i)\)を\((\forall _{x:A.\mathord {\textnormal {\textsf {Center}}}}\mathord {\textnormal {\textsf {IsEquiv}}}(B.\mathord {\textnormal {\textsf {leg-l}}}\lbrace x\rbrace ))\land (\forall _{x:A.\mathord {\textnormal {\textsf {Center}}}}\mathord {\textnormal {\textsf {IsEquiv}}}(B.\mathord {\textnormal {\textsf {leg-r}}}\lbrace x\rbrace ))\)と定義する。\(\mathord {\textnormal {\textsf {IsCart}}}(B)\)の要素があるとき、\(B\)はカルテシアン(cartesian)であると言う。