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

• -\(\mathord {\textnormal {\textsf {Index}}}:\mathcal {U}(i)\)
• -\(\mathord {\textnormal {\textsf {Dom}}}:\mathord {\textnormal {\textsf {Index}}}\to \mathcal {U}(i)\)
• -\(\mathord {\textnormal {\textsf {Cod}}}:\mathord {\textnormal {\textsf {Index}}}\to \mathcal {U}(i)\)
• -\(\mathord {\textnormal {\textsf {fun}}}:\prod _{k:\mathord {\textnormal {\textsf {Index}}}}\mathord {\textnormal {\textsf {Dom}}}(k)\to \mathord {\textnormal {\textsf {Cod}}}(k)\)

\(\mathord {\textnormal {\textsf {LocalGen}}}(i)\)の要素を(階数\(i\)の)局所生成系(local generator)と呼ぶ。