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

• -\(\mathord {\textnormal {\textsf {Carrier}}}:\mathcal {U}(i)\)
• -\(\mathord {\textnormal {\textsf {point}}}:\mathord {\textnormal {\textsf {Carrier}}}\)

\(\mathcal {U}_{\bullet }(i)\)の要素を(階数\(i\)の)点付き型(pointed type)と呼ぶ。