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

iiを階数、A:Span(i)A:\mathord {\textnormal {\textsf {Span}}}(i)をスパン、B:SpanOver(A)B:\mathord {\textnormal {\textsf {SpanOver}}}(A)をAA上のスパン、C:Cocone(A)C:\mathord {\textnormal {\textsf {Cocone}}}(A)を余錐とする。型CoconeOver(B,C):U(succ(i))\mathord {\textnormal {\textsf {CoconeOver}}}(B,C):\mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))と次のレコード型と定義する。

  • -Vertex:C.Vertex→U(i)\mathord {\textnormal {\textsf {Vertex}}}:C.\mathord {\textnormal {\textsf {Vertex}}}\to \mathcal {U}(i)
  • -inLeft:∏{x:A.Left}B.Left(x)→Vertex(C.inLeft(x))\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Left}}}\rbrace }B.\mathord {\textnormal {\textsf {Left}}}(x)\to \mathord {\textnormal {\textsf {Vertex}}}(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}(x))
  • -inRight:∏{x:A.Right}B.Right(x)→Vertex(C.inRight(x))\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Right}}}\rbrace }B.\mathord {\textnormal {\textsf {Right}}}(x)\to \mathord {\textnormal {\textsf {Vertex}}}(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}(x))
  • -inCenter:∏{x:A.Center}B.Center(x)→Vertex(C.inCenter(x))\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Center}}}\rbrace }B.\mathord {\textnormal {\textsf {Center}}}(x)\to \mathord {\textnormal {\textsf {Vertex}}}(C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(x))
  • -inleg-l:∏{x:A.Center}∏y:B.Center(x)inCenter(y)=C.inleg-l(x)VertexinLeft(B.leg-l(y))\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-l}}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Center}}}\rbrace }\prod _{y:B.\mathord {\textnormal {\textsf {Center}}}(x)}\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(y)=_{C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-l}}}}(x)}^{\mathord {\textnormal {\textsf {Vertex}}}}\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Left}}}}(B.\mathord {\textnormal {\textsf {leg-l}}}(y))
  • -inleg-r:∏{x:A.Center}∏y:B.Center(x)inCenter(y)=C.inleg-r(x)VertexinRight(B.leg-r(y))\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-r}}}}:\prod _{\lbrace x:A.\mathord {\textnormal {\textsf {Center}}}\rbrace }\prod _{y:B.\mathord {\textnormal {\textsf {Center}}}(x)}\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Center}}}}(y)=_{C.\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {leg-r}}}}(x)}^{\mathord {\textnormal {\textsf {Vertex}}}}\mathord {\textnormal {\textsf {in}}}_{\mathord {\textnormal {\textsf {Right}}}}(B.\mathord {\textnormal {\textsf {leg-r}}}(y))
CoconeOver(B,C)\mathord {\textnormal {\textsf {CoconeOver}}}(B,C)の要素をCC上BB下の余錐と呼ぶ。