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

\(i\)を階数、\(A:\mathord {\textnormal {\textsf {Span}}}(i)\)をスパン、\(C:\mathord {\textnormal {\textsf {Cocone}}}(A)\)を余錐とする。関数

\(\mathord {\textnormal {\textsf {cmp}}}(C):A.\mathord {\textnormal {\textsf {Left}}}\mathbin {{}_{A.\mathord {\textnormal {\textsf {leg-l}}}}\smash {+}_{A.\mathord {\textnormal {\textsf {leg-r}}}}}A.\mathord {\textnormal {\textsf {Right}}}\to C.\mathord {\textnormal {\textsf {Vertex}}}\)
を次のように定義する。
  • -\(x:A.\mathord {\textnormal {\textsf {Left}}}\)に対して\(\mathord {\textnormal {\textsf {cmp}}}(C,\mathord {\textnormal {\textsf {in}}}_{1}(x))\equiv C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}(x)\)
  • -\(y:A.\mathord {\textnormal {\textsf {Right}}}\)に対して\(\mathord {\textnormal {\textsf {cmp}}}(C,\mathord {\textnormal {\textsf {in}}}_{2}(y))\equiv C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}(y)\)
  • -\(z:A.\mathord {\textnormal {\textsf {Center}}}\)に対して\(\mathord {\textnormal {\textsf {cmp}}}(C,\mathord {\textnormal {\textsf {glue}}}(z))=C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-r}}}}(z)\circ {(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-l}}}}(z))}^{-1}\)