\(i\)を階数、\(G:\mathord {\textnormal {\textsf {LocalGen}}}(i)\)を局所生成系、\(A:\mathcal {U}(i)\)を型とする。型\(\mathord {\textnormal {\textsf {IsLocal}}}(G,A):\mathcal {U}(i)\)を

\(\forall _{k:G.\mathord {\textnormal {\textsf {Index}}}}\mathord {\textnormal {\textsf {IsEquiv}}}(\lambda (f:G.\mathord {\textnormal {\textsf {Cod}}}(k)\to A).f\circ G.\mathord {\textnormal {\textsf {fun}}}(k))\)と定義する。\(\mathord {\textnormal {\textsf {IsLocal}}}(G,A)\)の要素があるとき、\(A\)は\(G\)-局所的(\(G\)-local)であると言う。