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

\(i\)を階数、\(A:\mathord {\textnormal {\textsf {Span}}}(i)\)をスパン、\(B:\mathord {\textnormal {\textsf {SpanOver}}}(A)\)\(A\)上のスパン、\(C:\mathord {\textnormal {\textsf {Cocone}}}(A)\)を余錐、\(D:\mathord {\textnormal {\textsf {CoconeOver}}}(B,C)\)\(C\)上の余錐とする。型\(\mathord {\textnormal {\textsf {IsCart}}}(D):\mathcal {U}(i)\)\((\forall _{x:A.\mathord {\textnormal {\textsf {Left}}}}\mathord {\textnormal {\textsf {IsEquiv}}}(D.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}\lbrace x\rbrace ))\land (\forall _{x:A.\mathord {\textnormal {\textsf {Right}}}}\mathord {\textnormal {\textsf {IsEquiv}}}(D.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}\lbrace x\rbrace ))\land (\forall _{x:A.\mathord {\textnormal {\textsf {Center}}}}\mathord {\textnormal {\textsf {IsEquiv}}}(D.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}\lbrace x\rbrace ))\)と定義する。\(\mathord {\textnormal {\textsf {IsCart}}}(D)\)の要素があるとき、\(D\)カルテシアン(cartesian)であると言う。