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

\(i\)を階数、\(A:\mathord {\textnormal {\textsf {Span}}}(i)\)をスパン、\(C:\mathord {\textnormal {\textsf {Cocone}}}(A)\)を余錐とする。型\(\mathord {\textnormal {\textsf {IsUniversal}}}(C):\mathcal {U}(i)\)\(\mathord {\textnormal {\textsf {IsEquiv}}}(\mathord {\textnormal {\textsf {cmp}}}(C))\)と定義する。\(\mathord {\textnormal {\textsf {IsUniversal}}}(C)\)の要素があるとき、\(C\)普遍余錐(universal cocone)であると言う。