[007Y] 局所化

ファイバー余積以外の重要な高次帰納的型として局所化(localization)がある。

$$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)と呼ぶ。

[0080] 定義

$$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)であると言う。

型 $$A$$ の $$G$$ -局所化([0084])は $$A$$ に最も近い $$G$$ -局所的な型のことである。 $$G$$ -局所化の構成への最初の段階として、次の高次帰納的型を導入する。

[0081] 規則

$$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')$ を構成できる。

$\mathord {\textnormal {\textsf {WLoc}}}(G,A)$ は再帰的な高次帰納的型の例である。ここでいう再帰的とは、 $\mathord {\textnormal {\textsf {ext}}}$ と $\mathord {\textnormal {\textsf {is-ext}}}$ の引数 $$f$$ の型 $G.\mathord {\textnormal {\textsf {Dom}}}(k)\to \mathord {\textnormal {\textsf {WLoc}}}(G,A)$ に $\mathord {\textnormal {\textsf {WLoc}}}(G,A)$ 自身が現れるということである。ファイバー余積([003R])は再帰的な高次帰納的型ではない。

定義から、関数

\lambda f.f\circ G.\mathord {\textnormal {\textsf {fun}}}(k):(G.\mathord {\textnormal {\textsf {Cod}}}(k)\to \mathord {\textnormal {\textsf {WLoc}}}(G,A))\to (G.\mathord {\textnormal {\textsf {Dom}}}(k)\to \mathord {\textnormal {\textsf {WLoc}}}(G,A))

のファイバーは(関数外延性の下で)要素を持つが可縮であるとまでは言えない。可縮性を保証するためにはより高次の同一視の構成子を追加するのも一つの手だが、実は

\(G\)

に関数を追加することでも実現できる。

[0082] 定義

$$i$$ を階数、 $A,B:\mathcal {U}(i)$ を型、 $f:A\to B$ を関数とする。関数 $\mathord {\textnormal {\textsf {codiag}}}(f):B\mathbin {{}_{f}\smash {+}_{f}}B\to B$ を

- $\mathord {\textnormal {\textsf {codiag}}}(f,\mathord {\textnormal {\textsf {in}}}_{1}(y))\equiv y$
- $\mathord {\textnormal {\textsf {codiag}}}(f,\mathord {\textnormal {\textsf {in}}}_{2}(y))\equiv y$
- $\mathord {\textnormal {\textsf {codiag}}}(f,\mathord {\textnormal {\textsf {glue}}}(x))=\mathord {\textnormal {\textsf {refl}}}$

で定義する。

[0083] 定義

$$i$$ を階数、 $G:\mathord {\textnormal {\textsf {LocalGen}}}(i)$ を局所生成系とする。局所生成系 $\mathord {\textnormal {\textsf {D}}}(G):\mathord {\textnormal {\textsf {LocalGen}}}(i)$ を次のように定義する。

- $\mathord {\textnormal {\textsf {Index}}}\equiv G.\mathord {\textnormal {\textsf {Index}}}+G.\mathord {\textnormal {\textsf {Index}}}$
- $\mathord {\textnormal {\textsf {fun}}}(\mathord {\textnormal {\textsf {in}}}_{1}(k))\equiv G.\mathord {\textnormal {\textsf {fun}}}(k)$
- $\mathord {\textnormal {\textsf {fun}}}(\mathord {\textnormal {\textsf {in}}}_{2}(k))\equiv \mathord {\textnormal {\textsf {codiag}}}(G.\mathord {\textnormal {\textsf {fun}}}(k))$
- $\mathord {\textnormal {\textsf {Dom}}}$ と $\mathord {\textnormal {\textsf {Cod}}}$ は $\mathord {\textnormal {\textsf {fun}}}$ から決まる。

[0084] 定義

$$i$$ を階数、 $G:\mathord {\textnormal {\textsf {LocalGen}}}(i)$ を局所生成系、 $A:\mathcal {U}(i)$ を型とする。 $$A$$ の $$G$$ -局所化( $$G$$ -localization) $\mathord {\textnormal {\textsf {Loc}}}(G,A):\mathcal {U}(i)$ を $\mathord {\textnormal {\textsf {WLoc}}}(\mathord {\textnormal {\textsf {D}}}(G),A)$ と定義する。

$\mathord {\textnormal {\textsf {Loc}}}(G,A)$ は次の普遍性を満たす。

[0085] 演習

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

1 $\mathord {\textnormal {\textsf {Loc}}}(G,A)$ は $$G$$ -局所的である。
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)$ は同値である。