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

• -\(A\)の弱\(G\)-局所化\(\mathord {\textnormal {\textsf {WLoc}}}(G,A):\mathcal {U}(i)\)を構成できる。
• -要素\(a:A\)に対して、要素\(\mathord {\textnormal {\textsf {in}}}(a):\mathord {\textnormal {\textsf {WLoc}}}(G,A)\)を構成できる。
• -\(k:G.\mathord {\textnormal {\textsf {Index}}}\)を要素、\(f:G.\mathord {\textnormal {\textsf {Dom}}}(k)\to \mathord {\textnormal {\textsf {WLoc}}}(G,A)\)を関数、\(y:G.\mathord {\textnormal {\textsf {Cod}}}(k)\)を要素とすると、要素\(\mathord {\textnormal {\textsf {ext}}}(f,y):\mathord {\textnormal {\textsf {WLoc}}}(G,A)\)を構成できる。
• -\(k:G.\mathord {\textnormal {\textsf {Index}}}\)を要素、\(f:G.\mathord {\textnormal {\textsf {Dom}}}(k)\to \mathord {\textnormal {\textsf {WLoc}}}(G,A)\)を関数、\(x:G.\mathord {\textnormal {\textsf {Dom}}}(k)\)を要素とすると、同一視\(\mathord {\textnormal {\textsf {is-ext}}}(f,x):\mathord {\textnormal {\textsf {ext}}}(f,G.\mathord {\textnormal {\textsf {fun}}}(k,x))=f(x)\)を構成できる。
• -\(b:\mathord {\textnormal {\textsf {WLoc}}}(G,A)\)を要素、\(j\)を階数、\(C:\mathord {\textnormal {\textsf {WLoc}}}(G,A)\to \mathcal {U}(j)\)を型の族、\(s:\prod _{a:A}C(\mathord {\textnormal {\textsf {in}}}(a))\)と\(h:\prod _{\lbrace k:G.\mathord {\textnormal {\textsf {Index}}}\rbrace }\prod _{\lbrace f:G.\mathord {\textnormal {\textsf {Dom}}}(k)\to \mathord {\textnormal {\textsf {WLoc}}}(G,A)\rbrace }(\prod _{x:G.\mathord {\textnormal {\textsf {Dom}}}(k)}C(f(x)))\to (\prod _{y:G.\mathord {\textnormal {\textsf {Cod}}}(k)}C(\mathord {\textnormal {\textsf {ext}}}(f,y)))\)と\(p:\prod _{\lbrace k\rbrace }\prod _{\lbrace f\rbrace }\prod _{g:\prod _{x:G.\mathord {\textnormal {\textsf {Dom}}}(k)}C(f(x))}\prod _{x:G.\mathord {\textnormal {\textsf {Dom}}}(k)}h(g,G.\mathord {\textnormal {\textsf {fun}}}(k,x))=_{\mathord {\textnormal {\textsf {is-ext}}}(f,x)}^{C}g(x)\)を関数とすると、要素\(\mathord {\textnormal {\textsf {ind}}}_{\mathord {\textnormal {\textsf {WLoc}}}}(b,C,s,h,p):C(b)\)を構成できる。
• -\(a:A\)を要素、\(j\)を階数、\(C:\mathord {\textnormal {\textsf {WLoc}}}(G,A)\to \mathcal {U}(j)\)を型の族、\(s:\prod _{a:A}C(\mathord {\textnormal {\textsf {in}}}(a))\)と\(h:\prod _{\lbrace k:G.\mathord {\textnormal {\textsf {Index}}}\rbrace }\prod _{\lbrace f:G.\mathord {\textnormal {\textsf {Dom}}}(k)\to \mathord {\textnormal {\textsf {WLoc}}}(G,A)\rbrace }(\prod _{x:G.\mathord {\textnormal {\textsf {Dom}}}(k)}C(f(x)))\to (\prod _{y:G.\mathord {\textnormal {\textsf {Cod}}}(k)}C(\mathord {\textnormal {\textsf {ext}}}(f,y)))\)と\(p:\prod _{\lbrace k\rbrace }\prod _{\lbrace f\rbrace }\prod _{g:\prod _{x:G.\mathord {\textnormal {\textsf {Dom}}}(k)}C(f(x))}\prod _{x:G.\mathord {\textnormal {\textsf {Dom}}}(k)}h(g,G.\mathord {\textnormal {\textsf {fun}}}(k,x))=_{\mathord {\textnormal {\textsf {is-ext}}}(f,x)}^{C}g(x)\)を関数とすると、\(\mathord {\textnormal {\textsf {ind}}}_{\mathord {\textnormal {\textsf {WLoc}}}}(\mathord {\textnormal {\textsf {in}}}(a),C,s,h,p)\equiv s(a)\)と定義される。
• -\(k':G.\mathord {\textnormal {\textsf {Index}}}\)を要素、\(f':G.\mathord {\textnormal {\textsf {Dom}}}(k')\to \mathord {\textnormal {\textsf {WLoc}}}(G,A)\)を関数、\(y':G.\mathord {\textnormal {\textsf {Cod}}}(k')\)を要素、\(j\)を階数、\(C:\mathord {\textnormal {\textsf {WLoc}}}(G,A)\to \mathcal {U}(j)\)を型の族、\(s:\prod _{a:A}C(\mathord {\textnormal {\textsf {in}}}(a))\)と\(h:\prod _{\lbrace k:G.\mathord {\textnormal {\textsf {Index}}}\rbrace }\prod _{\lbrace f:G.\mathord {\textnormal {\textsf {Dom}}}(k)\to \mathord {\textnormal {\textsf {WLoc}}}(G,A)\rbrace }(\prod _{x:G.\mathord {\textnormal {\textsf {Dom}}}(k)}C(f(x)))\to (\prod _{y:G.\mathord {\textnormal {\textsf {Cod}}}(k)}C(\mathord {\textnormal {\textsf {ext}}}(f,y)))\)と\(p:\prod _{\lbrace k\rbrace }\prod _{\lbrace f\rbrace }\prod _{g:\prod _{x:G.\mathord {\textnormal {\textsf {Dom}}}(k)}C(f(x))}\prod _{x:G.\mathord {\textnormal {\textsf {Dom}}}(k)}h(g,G.\mathord {\textnormal {\textsf {fun}}}(k,x))=_{\mathord {\textnormal {\textsf {is-ext}}}(f,x)}^{C}g(x)\)を関数とすると、\(\mathord {\textnormal {\textsf {ind}}}_{\mathord {\textnormal {\textsf {WLoc}}}}(\mathord {\textnormal {\textsf {ext}}}(f',y'),C,s,h,p)\equiv h(\lambda x.\mathord {\textnormal {\textsf {ind}}}_{\mathord {\textnormal {\textsf {WLoc}}}}(f'(x),C,s,h,p),y')\)と定義される。
• -\(k':G.\mathord {\textnormal {\textsf {Index}}}\)を要素、\(f':G.\mathord {\textnormal {\textsf {Dom}}}(k')\to \mathord {\textnormal {\textsf {WLoc}}}(G,A)\)を関数、\(x':G.\mathord {\textnormal {\textsf {Dom}}}(k')\)を要素、\(j\)を階数、\(C:\mathord {\textnormal {\textsf {WLoc}}}(G,A)\to \mathcal {U}(j)\)を型の族、\(s:\prod _{a:A}C(\mathord {\textnormal {\textsf {in}}}(a))\)と\(h:\prod _{\lbrace k:G.\mathord {\textnormal {\textsf {Index}}}\rbrace }\prod _{\lbrace f:G.\mathord {\textnormal {\textsf {Dom}}}(k)\to \mathord {\textnormal {\textsf {WLoc}}}(G,A)\rbrace }(\prod _{x:G.\mathord {\textnormal {\textsf {Dom}}}(k)}C(f(x)))\to (\prod _{y:G.\mathord {\textnormal {\textsf {Cod}}}(k)}C(\mathord {\textnormal {\textsf {ext}}}(f,y)))\)と\(p:\prod _{\lbrace k\rbrace }\prod _{\lbrace f\rbrace }\prod _{g:\prod _{x:G.\mathord {\textnormal {\textsf {Dom}}}(k)}C(f(x))}\prod _{x:G.\mathord {\textnormal {\textsf {Dom}}}(k)}h(g,G.\mathord {\textnormal {\textsf {fun}}}(k,x))=_{\mathord {\textnormal {\textsf {is-ext}}}(f,x)}^{C}g(x)\)を関数とすると、同一視\(\mathord {\mathord {\textnormal {\textsf {ind}}}_{\mathord {\textnormal {\textsf {WLoc}}}}\mathord {\textnormal {\textsf {-}}}\mathord {\textnormal {\textsf {is-ext}}}}(f',x',C,s,h,p):\mathord {\textnormal {\textsf {apd}}}(\lambda b.\mathord {\textnormal {\textsf {ind}}}_{\mathord {\textnormal {\textsf {WLoc}}}}(b,C,s,h,p),\mathord {\textnormal {\textsf {is-ext}}}(f',x'))=p(\lambda x.\mathord {\textnormal {\textsf {ind}}}_{\mathord {\textnormal {\textsf {WLoc}}}}(f'(x),C,s,h,p),x')\)を構成できる。