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

• -\(\mathord {\textnormal {\textsf {Left}}}:\mathcal {U}(i)\)
• -\(\mathord {\textnormal {\textsf {Right}}}:\mathcal {U}(i)\)
• -\(\mathord {\textnormal {\textsf {Center}}}:\mathcal {U}(i)\)
• -\(\mathord {\textnormal {\textsf {leg-l}}}:\mathord {\textnormal {\textsf {Center}}}\to \mathord {\textnormal {\textsf {Left}}}\)
• -\(\mathord {\textnormal {\textsf {leg-r}}}:\mathord {\textnormal {\textsf {Center}}}\to \mathord {\textnormal {\textsf {Right}}}\)

\(\mathord {\textnormal {\textsf {Span}}}(i)\)の要素を(階数\(i\)の)スパン(span)と呼ぶ。