\(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))\)