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

• -\(\mathord {\textnormal {\textsf {Vertex}}}:C.\mathord {\textnormal {\textsf {Vertex}}}\to \mathcal {U}(i)\)
• -\(\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))\)
• -\(\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))\)
• -\(\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))\)
• -\(\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))\)
• -\(\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))\)

\(\mathord {\textnormal {\textsf {CoconeOver}}}(B,C)\)の要素を\(C\)上\(B\)下の余錐と呼ぶ。