ホモトピー型理論
[007T] 演習

\(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\)上の余錐とする。\(B\)がカルテシアンで、\(C\)が普遍余錐で、\(D\)がカルテシアンならば、\(\mathord {\textnormal {\textsf {Total}}}(D):\mathord {\textnormal {\textsf {Cocone}}}(\mathord {\textnormal {\textsf {Total}}}(B))\)は普遍余錐である。