関数外延性を仮定する。\(i\)を階数、\(G:\mathord {\textnormal {\textsf {LocalGen}}}(i)\)を局所生成系、\(A:\mathcal {U}(i)\)を型とする。

1. 1\(\mathord {\textnormal {\textsf {Loc}}}(G,A)\)は\(G\)-局所的である。
2. 2\(X:\mathcal {U}(i)\)を型とし、\(X\)は\(G\)-局所的であると仮定する。関数\(\lambda f.f\circ \mathord {\textnormal {\textsf {in}}}:(\mathord {\textnormal {\textsf {Loc}}}(G,A)\to X)\to (A\to X)\)は同値である。