一連のシリーズ記事として、「階層化された宇宙達を備えた型理論」について述べてきました。最初の記事がハブ記事（他の記事へのリンク集）にもなっています。
「階層化された宇宙達を備えた型理論」は依存型理論でもあり、パイ型とシグマ型を持っています。パイ型とシグマ型は型ファミリーに対して定義されます。型ファミリーは依存型理論の中心的な概念です。シリーズ過去記事では、型ファミリーを定義するために、型（圏の対象／宇宙の要素）を“棲家である圏／宇宙”から外部に取り出す方法を使っています。
対象を圏の外部に取り出す方法を外部化手法〈externalization〉と呼ぶとして、外部化手法は圧倒的に便利なところがあります。しかし一方、型理論を強引に集合論と圏論に帰着させている感じもします。いわば外科手術的手法であって、「こんな乱暴なことしていいのかな？ する必要があったのだろうか？」という疑問もわきます。
この辺のことを考えるヒントとして、パイ型により指数型を表現してみます。パイ型により指数型が表現できるデカルト閉圏は、“ほとんど集合圏”のように思えます。とは言え、もっと弱い条件や全然別な方法で同じ結果（パイ型により指数型が表現できること）が得られるかも知れないので断言は出来ませんが、「集合圏と似てないデカルト閉圏に対しては、外部化手法は有効じゃない」気がします。
「外部化しないでどうやるんだ？」と聞かれると、よく分かりません。ひょっとすると、外部化が有効な範囲で十分なのかも知れません。分からないことばかりですが、まーともかく、パイ型により指数型を表現するシナリオを書いておきます。最後に外部化手法について思うことを記します。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\ol}[1]{\overline{#1}}
\newcommand{\J}{\mathrm{J}}
\newcommand{\K}{\mathrm{K}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\In}{\text{ in }}
\newcommand{\Imp}{\Rightarrow}
\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\hyp}{ \text{－} }
\newcommand{\dim}[2]{{#1}\!\updownarrow^{#2}}
\newcommand{\twoto}{\Rightarrow }
`$
内容：
シリーズ・ハブ記事：
用語・記法の約束
$`U \in U' \in U''`$ を三階層分のグロタンディーク宇宙とします。三階層分あればたいてい間に合います。集合圏や圏の圏は $`U, U', U''`$ に相対的に考えます。
- $`{\bf Set} := {\bf Set}_U`$
- $`{\bf Cat} := \mrm{Cat}({\bf Set})`$ （$`\mrm{Cat}(\hyp)`$ は内部圏の2-圏を作り出す構成）
- $`{\bf SET} := {\bf Set}_{U'}`$
- $`{\bf CAT} := \mrm{Cat}({\bf SET})`$
- $`\mathbb{SET} := {\bf Set}_{U''}`$
- $`\mathbb{CAT} := \mrm{Cat}(\mathbb{SET})`$
$`{\bf Cat}`$ の対象は小さい圏〈小圏 | small category〉と呼びます。単に圏〈category〉と言ったら、小さいとは限らないが $`U`$ に関して局所小〈locally small〉であることは仮定します。
$`\cat{C}`$ は（この記事を通して）、$`U`$-局所小なデカルト閉圏とします。記号 $`{\bf 1}, \times, [\hyp, \hyp]`$ はデカルト閉圏の終対象（かつモノイド単位）、デカルト積、指数の意味で使います。
次のような型理論の言葉を使います。
- $`\cat{C}`$ の対象を型〈type〉と呼ぶ。
- $`a: {\bf 1} → A \In \cat{C}`$ のとき、$`a`$ を型 $`A`$ のインスタンス〈instance〉と呼ぶ。
型の外延化と圏化
型の外延化〈extensionalize〉という概念は、「デカルト閉・型システム」で定義しました。型 $`A \in |\cat{C}|`$ に対して、その外延化は
$`\quad \ol{A} := \cat{C}({\bf 1}, A)`$
と定義します。これは、型 $`A`$ のインスタンス全体の集合です。「最近の型理論： 宇宙と世界、そして銀河」では、同じことを次のように定義しています。
$`\quad \mrm{Inst}(A) := \cat{C}({\bf 1}, A)`$
型の外延化とインスタンス集合は同じなので：
$`\quad \ol{A} = \mrm{Inst}(A) \In {\bf Set}`$
射 $`f:A \to B \In \cat{C}`$ に対して、外延化〈インスタンス集合〉のあいだの写像を定義できるので、外延化〈インスタンス集合〉は関手になります。
$`\quad \ol{(\hyp)} \; = \mrm{Inst} : \cat{C} \to {\bf Set} \In {\bf CAT}`$
集合に離散圏を対応させ、写像に離散圏のあいだの関手を対応させる $`\mrm{Disc}`$ は、集合圏から圏の圏への関手になります。
$`\quad \mrm{Disc} : {\bf Set} \to \dim{\bf Cat}{1} \In {\bf CAT}`$
ここで、 $`\dim{\bf Cat}{1}`$ は、2-圏の2-射を捨てて1-圏とみなしたものです。
$`\dim{\bf Cat}{1}\, \subset \dim{\bf CAT}{1}`$ （部分圏）なので、$`\mrm{Disc}`$ は次のようにもみなせます。
$`\quad \mrm{Disc} : {\bf Set} \to \dim{\bf CAT}{1} \In \mathbb{CAT}`$
型の外延化の後に離散圏化することを、型圏化〈type categorification〉と呼びます*1。型圏化は「最近の型理論： 依存型理論で述語論理が出来てしまう理由」で導入した概念で、$`\J`$ で表します。
$`\xymatrix{
\cat{C} \ar[r]^{\mrm{Inst}} \ar[dr]_{\J}
& {\bf Set} \ar[d]^{\mrm{Disc}}
\\
{}
& \dim{\bf CAT}{1}
}\\
\In \mathbb{CAT}
`$
外部化手法では、型外延化 $`\mrm{Inst}`$ や型圏化 $`\J`$ を用いて、圏 $`\cat{C}`$ の内部に居た対象〈型〉を $`{\bf Set}`$ や $`{\bf CAT}`$ へと引きずり出します*2。圏 $`\cat{C}`$ の構造と性質によっては、対象を引きずり出すときにもともとの情報を失うかも知れません（例えば、$`\ol{A}`$ が空集合になる）。
デカルト閉圏の外延性
外延化は、型〈対象〉だけではなくて射にも定義できて、$`\mrm{Inst}: \cat{C} \to {\bf Set}`$ は関手になるのでした。この外延化関手が忠実関手〈faithful functor〉のとき、圏 $`\cat{C}`$ は外延的〈extensional〉ということにします*3。
圏の外延性は、デカルト閉圏でなくても終対象を持つ圏に対して定義できます。外延的な圏は、終対象が分離子〈separator〉になっている圏です。このとき、外延化関手は、集合圏への忘却関手とみなしてかまいません。
さらに、外延化関手が充満忠実関手〈fully faithful functor〉のとき、圏 $`\cat{C}`$ はフル外延的〈fully extensional〉ということにします。フル外延的な圏では、ホムセットが写像の集合（集合圏のホムセット）と同型になります。
$`\text{For } A, B\in |\cat{C}|\\
\quad \cat{C}(A, B) \cong \mrm{Map}(\ol{A}, \ol{B}) \In {\bf Set}`$
フル外延的な圏は、集合圏の充満部分圏に非常に近い圏になります*4。
デカルト閉圏 $`\cat{C}`$ がフル外延的なら、次の同型が成立します。
$`\text{For } T, A, B\in |\cat{C}|\\
\quad \cat{C}(T\times A, B) \cong \mrm{Map}(\ol{T}, \cat{C}(A, B))`$
それは、次のような同型の連鎖から分かります。
$`\quad \cat{C}(T\times A, B)\\
\cong \cat{C}(T, [A, B])\\
\cong \mrm{Map}(\ol{T}, \ol{[A, B]} )\\
= \mrm{Map}(\ol{T}, \cat{C}({\bf 1}, [A, B]) )\\
\cong \mrm{Map}(\ol{T}, \cat{C}(A, B) )
`$
幾つかの準備
「$`\cat{C}`$ がフル外延的なデカルト閉圏ならば、指数型をパイ型で表現可能」なことを示すための準備をします。この節は飛ばして、後で必要になったら見直すでもいいです。
次のような同型／等式を示します。使っている記号の意味はすぐ後で説明します。
- $`\cat{C}(T\times A, B) \cong \mrm{Map}(\ol{T}, \cat{C}(A, B))`$
- $`\cat{C}^{\J(T)}(\K^A_{\J(T)}, \K^B_{\J(T)}) \cong \mrm{Map}(\ol{T}, \cat{C}(A, B))`$
- $`\K^A_{\J(T)} = \mrm{Can}_{\J(!_T)} \K^A_{\J({\bf 1})}`$
- $`\cat{C}^{\J(T)}(\mrm{Can}_{\J(!_T)} \K^A_{\J({\bf 1})}, \K^B_{\J(T)}) \cong \mrm{Map}(\ol{T}, \cat{C}(A, B))`$
一番目は前節で示したことを再掲したものです。二番目の同型の左辺の一部に、三番目の等式による“代入”をすれば四番目が得られます。
二番目、三番目で出てくる $`\cat{C}^{\J(T)}`$ は圏の指数です。一般に、$`\cat{A}, \cat{B}`$ が圏のとき、$`\cat{B}^\cat{A} = [\cat{A}, \cat{B}]`$ は、圏の指数 -- つまり関手圏を表します。関手圏の対象は関手で、射は自然変換です。$`T \in |\cat{C}|`$ に対して $`\J(T)`$ は圏（離散圏）だったので、$`\cat{C}^{\J(T)}`$ は関手圏として意味を持ちます。
$`\K^A_{\J(T)}`$ は、省略せずに書けば $`\K^A_{\J(T), \cat{C}}`$ です。これは、$`\J(T) \to \cat{C}`$ の定数関手を意味します。一般に、$`\K^C_{\cat{A}, \cat{B}}`$ は次のような関手です。
$`\text{For }X \in |\cat{A}|\\
\quad \K^C_{\cat{A}, \cat{B}}(X) = C \;\in |\cat{B}|\\
\text{For }f:X\to Y \In \cat{A}\\
\quad \K^C_{\cat{A}, \cat{B}}(f) = (\id_C : C\to C \In \cat{B})
`$
文脈から明らかなら、次のような省略をします。
$`\K^C := \K^C_{\cat{A}} := \K^C_{\cat{A}, \cat{B}}`$
$`\mrm{Can}_K`$ は左右のカン拡張 $`\mrm{Lan}_K, \mrm{Ran}_K`$ と語呂をあわせた記法です（「最近の型理論： 型判断／シーケントの意味論に向けて // 記法について少し」参照）。これは、関手 $`K`$ のプレ結合による引き戻しを表します。関手の図式順結合記号を $`*`$ 、反図式順結合記号を $`\cdot`$ とすると（「関手と自然変換の計算に出てくる演算子記号とか // 今後使う予定の演算子記号〉参照）：
$`\quad \mrm{Can}_K F := K*F = F\cdot K`$
$`\mrm{Lan}_K \dashv \mrm{Can}_K \dashv \mrm{Ran}_K`$ が随伴トリプルになります。
二番目の同型
次を示します。
$`\quad \cat{C}^{\J(T)}(\K^A_{\J(T)}, \K^B_{\J(T)}) \cong \mrm{Map}(\ol{T}, \cat{C}(A, B))`$
$`\alpha \in \cat{C}^{\J(T)}(\K^A_{\J(T)}, \K^B_{\J(T)})`$ のとき、$`\alpha`$ は次の形の自然変換〈2-射〉です。
$`\quad \alpha :: \K^A \twoto \K^B : \J(T) \to \cat{C} \In {\bf CAT}`$
$`\alpha`$ の成分は、対象 $`t\in |\J(T)|`$ ごとに、
$`\quad \alpha_t : \K^A(t) \to \K^B(t) \In \cat{C}`$
$`K^\hyp`$ は定数関手だったので、
$`\quad \alpha_t : A \to B \In \cat{C}`$
つまり、$`t \mapsto \alpha_t`$ は次のような写像になります。
$`\quad \alpha_\hyp : |\J(T)| \to \cat{C}(A, B)`$
$`\J(T)`$ は離散圏だったので、自然性の条件は自明に満たされてしまいます。
$`|\J(T)| = \ol{T}`$ なので、上記の手順は次の写像を定義します。
$`\quad \alpha \mapsto (\alpha_\hyp : \ol{T} \to \cat{C}(A, B))`$
これが1:1なのは明らかなので、目的の同型が得られます。
三番目の等式
次を示します。
$`\quad \K^A_{\J(T)} = \mrm{Can}_{\J(!_T)} \K^A_{\J({\bf 1})}`$
この等式は次の可換図式と同じです。
$`\require{AMScd}
\begin{CD}
\J(T) @>{\J(!_T)}>> \J({\bf 1})\\
@V{\K^A}VV @VV{\K^A}V \\
\cat{C} @= \cat{C}
\end{CD}\\
\text{commutative in }{\bf CAT}`$
関手の行き先は、どっちみち一点 $`A \in |\cat{C}|`$ に潰れてしまうので、可換性は（したがって等式も）自明でしょう。
パイ型による指数型の表現
フル外延的なデカルト閉圏 $`\cat{C}`$ においては、2つの対象の指数型 $`[A, B]`$ がパイ型構成を使って表現できることを示します。ただし、細部を省略したアウトラインです。
前節の補題から次が言えます。
$`\quad \cat{C}(T\times A, B) \cong \cat{C}^{\J(T)}(\mrm{Can}_{\J(!_T)} \K^A_{\J({\bf 1})}, \K^B_{\J(T)})`$
一方、$`\cat{C}`$ をターゲットとする関手に対して、$`\J(!_T) : \J(T) \to \J({\bf 1})`$ に沿った右カン拡張を考えると、次のホムセット同型が成立します。
$`\quad \cat{C}^{\J(T)}(\mrm{Can}_{\J(!_T)} \K^A_{\J({\bf 1})}, \K^B_{\J(T)}) \cong
\cat{C}^{\J({\bf 1})}( \K^A_{\J({\bf 1})}, \mrm{Ran}_{\J(!_T)} \K^B_{\J(T)})
`$
$`\J({\bf 1})`$ は単対象で恒等射だけの圏なので $`\cat{C}^{\J({\bf 1})} \cong \cat{C}`$ となります。この圏同型を考慮すると：
$`\quad \cat{C}^{\J(T)}(\mrm{Can}_{\J(!_T)} \K^A_{\J({\bf 1})}, \K^B_{\J(T)}) \cong
\cat{C}( A, \lim \K^B_{\J(T)})
`$
本節最初の同型と組み合わせると、次の同型が得られます。
$`\quad \cat{C}(T\times A, B) \cong \cat{C}( A, \lim \K^B_{\J(T)})`$
このホムセット同型に伴う諸々の自然性を示せば、関手 $`T\times \hyp`$ と $`\lim \K^\hyp_{\J(T)}`$ が随伴関手だと分かります。関手 $`T\times \hyp`$ の右随伴関手が指数 $`[T, \hyp]`$ なので、
$`\quad [T, \hyp] = \lim \K^\hyp_{\J(T)}`$
だと言えます。
外部化手法による $`F:\J(T) \to \cat{C}`$ のパイ型の定義は、
$`\quad \Pi_T F := \lim F`$
なので、次のようにも書けます。
$`\quad [T, \hyp] = \Pi_T (\K^\hyp_{\J(T)})`$
これはまさに、パイ型による指数型の表現です。
外部化手法について
外部化手法を前提として、フル外延的なデカルト閉圏においては、指数型がパイ型で表現できることは分かりました。これは、外部化手法の妥当性を示すものでしょうか？ なんか違う気がする。フル外延的という仮定が強すぎます。フル外延的の仮定なしでも同じ結果を示せる可能性はあります。が、やってみた印象としては、外部化手法が集合論と集合論ベースの圏論に依拠し過ぎていて柔軟性に欠ける気がします。
適用範囲が狭い代わりに、外部化手法にはメリットがあります。通常の集合と圏をベースにしているので、直感的な把握が容易です。具体的な表示が得られ、具体的な計算ができます。注目しているデカルト閉圏 $`\cat{C}`$ の外部である集合圏／圏の圏には、使えるツールが揃っています。特に、関手圏とカン拡張が便利です。
明らかなメリットがあるので、外部化手法は使い続けるかも知れませんが、完全に満足すべき状況でないのは確かです。外部化手法を改善するか、別の手法に乗り換えることを考える必要があります。
注目しているデカルト閉圏 $`\cat{C}`$ の外の世界を、$`{\bf Set}`$ から別な圏にすることが考えられます。例えば、順序集合の圏 $`{\bf Ord}`$ です。$`\cat{C}`$ がωCPOの圏のように、順序豊穣圏〈order enriched category〉のとき、対象の外部化として順序集合が使えます。単なる集合を使うより、圏 $`\cat{C}`$ の特性を外部化に反映させることが出来るでしょう。
デカルト閉圏 $`\cat{C}`$ の対象を外部化する代わりに、$`\cat{C}`$ を $`\cat{C}`$ 自身のなかに内部化して型ファミリーを定義する方法もあるでしょう。外部に存在するツールが $`\cat{C}`$ 内部にあるとも限らないので、ツールの内部版を作る手間がかかるかも知れません。これ、しんどいかも。
ファミリーと依存型理論の圏論的意味論の道具として、ファミリー付き圏〈category with families〉や局所デカルト閉圏〈locally cartesian closed category〉なんてのもあるそうです。こういう、外部化しない方法も試してみる価値があります。
僕としては、階層化された宇宙／銀河のなかでハイパードクトリンが構成できればいいので、外部化手法以外に乗り換えてもかまいません。
