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

\(i\)を階数、\(A:\mathord {\textnormal {\textsf {Span}}}(i)\)をスパンとする。型\(\mathord {\textnormal {\textsf {Cocone}}}(A):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\)を次のレコード型と定義する。

  • -\(\mathord {\textnormal {\textsf {Vertex}}}:\mathcal {U}(i)\)
  • -\(\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}:A.\mathord {\textnormal {\textsf {Left}}}\to \mathord {\textnormal {\textsf {Vertex}}}\)
  • -\(\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}:A.\mathord {\textnormal {\textsf {Right}}}\to \mathord {\textnormal {\textsf {Vertex}}}\)
  • -\(\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}:A.\mathord {\textnormal {\textsf {Center}}}\to \mathord {\textnormal {\textsf {Vertex}}}\)
  • -\(\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-l}}}}:\prod _{x:A.\mathord {\textnormal {\textsf {Center}}}}\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(x)=\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}(A.\mathord {\textnormal {\textsf {leg-l}}}(x))\)
  • -\(\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-r}}}}:\prod _{x:A.\mathord {\textnormal {\textsf {Center}}}}\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(x)=\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}(A.\mathord {\textnormal {\textsf {leg-r}}}(x))\)
\(\mathord {\textnormal {\textsf {Cocone}}}(A)\)の要素を\(A\)下の余錐(cocone)と呼ぶ。