ホモトピー型理論
[007R] 定義

\(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)であると言う。