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

関数外延性と一価性を仮定する。\(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)\)が普遍余錐であることは論理的に同値である。