この記事は昨日の記事「カリー／ハワード／ランベック対応のための共通表現」の続きです。
昨日の記事では、ニュートラルな（クセのない）表現「(f with A) support B」を論理ではどう言うのか？ を話題にしました。型理論には触れなかったので、この記事では型理論の言い回し・呼び名を話題にします。
言い回し・呼び名の話だけではなくて、単純型理論の圏論的な定式化と、単純型理論から依存型理論を構成する手法についても述べます。
記事内で使う文字の色については「文字の色の約束（再確認）」を参照してください。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\mcal}[1]{\mathcal{#1}}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\u}[1]{\underline{#1} }
\newcommand{\In}{\text{ in } }
\newcommand{\hyp}{\text{－} }
\newcommand{\Imp}{\Rightarrow }
%\newcommand{\Equiv}{ \Leftrightarrow }
\newcommand{\T}[1]{ \text{#1} }
\newcommand{\op}{\mathrm{op} }
\newcommand{\id}{\mathrm{id} }
%\newcommand{\dto}{\looparrowright} % dependent to
%\newcommand{\hto}{\rightsquigarrow} % hetero to
%\newcommand{\parto}{\supset\!\to}
`$
内容：
単純型理論の言い回し
型理論は、単純型理論と依存型理論に大別されます。単純型理論と依存型理論では、呼び名・言い回しは違います。まず、単純型理論の話をします。
圏論的な主張 $`f:A \to B \In \cat{C}`$ は、(f with A) support B とその変種（主語の変更、受動態など）で表現されるのでした（「カリー／ハワード／ランベック対応のための共通表現」参照）。型理論にふさわしい動詞（support の置き換え）は inhabit〈居住する | 生息する〉でしょう。inhabit は型理論の専門用語としても使われる動詞です。
- (f with A) inhabit B
B を主語として受動態の文で書くなら：
- B is inhabited by f with A
- B is inhabited with A by f
型理論の習慣としては：
- A を明示することが少ない。
- 任意の A を考えるのではなくて、特定の A が暗黙に与えられていると考えることが多い。
上記の事情で、A を主語とすることはほぼありません。A を主語とする文は使われないのです。
- 【不使用】A inhabits B by f
f を主語とするなら：
- f inhabits B with A
構成素の省略でも、A を表に出す表現は使用されません。
f を省略して A, B だけ：
- 【不使用】A inhabits B
- 【不使用】B is inhabited with A
A を省略して f, B だけ：
- f inhabits B
- B is inhabited by f
f, A を省略して B だけ：
- B is inhabited
単純型理論のインスタンス
前節の例で、なぜ【不使用】な文が出てくるか、事情を説明しましょう。
$`\cat{C}`$ を単純型理論のための圏だとします。$`\cat{C}`$ の対象を型〈type〉と呼びます。したがって、$`|\cat{C}|`$ はすべての型からなる集合です。$`|\cat{C}|`$ を型宇宙〈type universe〉と呼びます。圏 $`\cat{C}`$ として集合圏 $`\mbf{Set}`$ を採用すると、集合論的単純型理論〈set-theoretic simple type theory〉になります。
型宇宙 $`|\cat{C}|`$ の要素（つまり型）は単純型理論の主題です。しかし型理論では、$`\cat{C}`$ の射の一部にしか興味を持ちません。型理論が興味を持つ射をインスタンスと呼ぶことにします。
型理論の悪習により、「インスタンス」を「項〈term〉」と呼びます。困ったことに、構文論側と意味論側を区別せずに「項」と呼びます。このことについては、以下の過去記事で批判的に説明しています。
ここでは「インスタンス」を使うと承知してください。
インスタンスを圏論的に説明すると、圏 $`\cat{C}`$ の終対象 $`\mbf{1}`$ からの射 $`f`$ です。
$`\quad f : \mbf{1} \to B \In \cat{C}`$
$`\cat{C} = \mbf{Set}`$ の場合は、インスタンスは集合 $`B`$ の要素と一対一対応します。
前節での【不使用】な言い回しを再掲すると：
- 【不使用】A inhabits B by f
- 【不使用】A inhabits B
- 【不使用】B is inhabited with A
$`A = \mbf{1}`$ と固定して考えているので、これらの意味はいずれも：
- $`f: \mbf{1} \to B \In \cat{C}`$
型理論にとってはこれは当たり前で、言わずもがな／蛇足なので、文として使用する機会がないのです。
$`A = \mbf{1}`$ には言及しない言い回しに丁寧な日本語を付けて列挙すると：
f, B だけ：
- f inhabits B
- インスタンス f は、型 B に居住する
f, B だけ、受動態：
- B is inhabited by f
- 型 B は、インスタンス f により居住される
B だけ：
- B is inhabited
- 型 B は居住されている
B だけのときの解釈は論理のときとは違います。B が、なんらかのインスタンスにより居住されていれば、「型 B は居住されている」と言います。特に $`\cat{C} = \mbf{Set}`$ のときは、「集合 B は空ではない」ということです。
論理の場合（「カリー／ハワード／ランベック対応のための共通表現」参照）と比較してみましょう。
- $`A = \mbf{1}`$ と固定して考えている。論理の場合は、仮定を固定はしない。
- 「B は居住されている」とは、なんらかの（なんでもいい）インスタンス（射）で居住されていることを意味する。論理の場合は違って、特定の述語（または論理式）からの射で保証されている、という意味になる。
- 型理論と論理の双方を、うまく調整すれば、きれいな対応を作ることもできる。例えば、論理の側で「仮定なしの証明しか考えない」と制限すると、型理論のインスタンスとうまく対応する。
ニュートラルな動詞 support を論理なら guarantee 、型理論なら inhabit に変えて調整しました。それだけでなく、上記注意事項のような方法論や習慣の違いも考慮する必要があります。「Proofs-as-Terms が説明困難な事情： n回目の整理」で述べたこと（以下）の一端がうかがえると思います。
語句レベルではなくて文レベルの対応が必要です。逐語訳ではホントにまったく全然ダメで、分野ごとの文化的違いまで考慮して意訳する必要があります。
型理論における“一般の射”の扱い方
前節で述べたように、単純型理論は、終対象 $`\mbf{1}`$ を持つ圏 $`\cat{C}`$ で展開されます。型理論が興味を持つ射は $`f:\mbf{1} \to B \In \cat{C}`$ という形の射、つまりインスタンスだけです。
となると、$`\cat{C}`$ の一般の射 $`f: A \to B \In \cat{C}`$（$`A`$ は $`\mbf{1}`$ とは限らない）は扱えないのか？ と心配になります。
実は、型理論でも一般の射を扱います。ただし、直接扱うのではなくて間接的に扱います。間接的に扱う方法が幾つかあります。
圏 $`\cat{C}`$ がデカルト閉圏だとします。すると、$`A, B\in |\cat{C}|`$ に対して指数対象〈内部ホム〉$`[A, B]`$ が存在します。この状況では：
- $`f: A \to B \In \cat{C}`$ の代わりに、インスタンス $`\varphi :\mbf{1}\to [A, B] \In \cat{C}`$ が使える。
$`f \longleftrightarrow \varphi`$ の相互変換は、カリー化／反カリー化により与えられます。
$`\quad \cat{C}(A, B) \cong \cat{C}(A\times \mbf{1}, B) \cong \cat{C}(\mbf{1}, [A, B])`$
この方法により、$`\cat{C}`$ のすべての射を間接的に扱えます。
この方法は論理にも適用できます。「カリー／ハワード／ランベック対応のための共通表現」の事例と記法をそのまま使うとして、証明 $`i: P \to Q \In \mbf{X''}`$ の代わりに、仮定なしの証明 $`\iota : \top \to (P \Imp Q)`$ が使えます。
$`i \longleftrightarrow \iota`$ の相互変換は、演繹定理により与えられます。演繹定理は、論理版のカリー化／反カリー化です。
$`\quad \mbf{X''}(P, Q) \cong \mbf{X''}(P\land \top, Q) \cong \mbf{X''}(\top, P \Imp Q)`$
この節の内容だけでも次の対応表を作れます。
| 型理論（圏論的） | 論理（構文論） |
|---|---|
| 型 | 論理式 |
| 終対象 | 真を表す論理定数 |
| インスタンス | 仮定のない証明 |
| 一般の射 | 証明 |
| カリー化／反カリー化 | 演繹定理 |
大きな対応表を作ろうと思うと、方法論・習慣の違いや同義語・多義語により対応が破綻するので、小さなスコープで小さな対応表をたくさん作るのが良いやり方です。
ちなみに、上の「型理論（圏論的）」は、圏論の用語と型理論・ラムダ計算の用語が混ざっているので、分離すると次のようです。
| 型理論・ラムダ計算の用語 | 圏論の用語 |
|---|---|
| 型 | 対象 |
| ユニット型 | 終対象 |
| インスタンス | 終対象からの射 |
| ？？ | 一般の射 |
| カリー化／反カリー化 | 随伴の転置／反転置 |
「随伴の転置／反転置」はあまり馴染みがない言葉かも知れません。以下の過去記事を参照してください。
依存型理論への入口
型理論において、インスタンスとは限らない一般の射 $`f: A \to B \In \cat{C}`$ を扱う方法をもうひとつ紹介します。この方法は、単純型理論から依存型理論への橋渡しにもなります。
$`f: A \to B \In \cat{C}`$ をインスタンスとして扱うために、新しい圏 $`\cat{C}/B`$ を考えます。$`\cat{C}/B`$ はスライス圏〈slice category〉（オーバー圏〈over category〉とも呼ぶ）です。
$`\cat{C}/B`$ の対象は、$`s: S \to B \In \cat{C}`$ のような $`\cat{C}`$ の射です。$`\cat{C}/B`$ の射は、以下のような $`\cat{C}`$ 内の可換三角形です。
$`\quad \xymatrix{
S \ar[dr]_{s} \ar[rr]^h
&{}
&T \ar[dl]^{t}
\\
{}
&B
&{}
}\\
\quad \T{commutative }\In \cat{C}
`$
$`s = h;t`$ （セミコロンは図式順結合記号）なので、可換三角形は $`h`$ と $`t`$ で決まります。なので、可換三角形を $`h^t`$ と書くと便利です。圏 $`\cat{C}/B`$ の結合〈composition〉は次の簡単な公式で与えられます。
$`\quad h^t ; k^u = (h;k)^u`$
$`\quad \xymatrix{
S \ar[dr]_{s} \ar[r]^h
&T \ar[d]|{t} \ar[r]^k
&U \ar[dl]^{u}
\\
{}
&B
&{}
}\\
\quad \T{commutative }\In \cat{C}
`$
$`\cat{C}/B`$ の対象 $`s`$（$`s:S \to B \In \cat{C}`$）の恒等射は次の可換三角形です。
$`\quad \xymatrix{
S \ar[dr]_{s} \ar[rr]^{\id_S}
&{}
&S \ar[dl]^{s}
\\
{}
&B
&{}
}\\
\quad \T{commutative }\In \cat{C}
`$
つまり、$`\id_s = {\id_S}^s`$（大文字小文字の違いに注意！）です。次が成立します。
$`\quad \id_s; h^t = {\id_S}^s ; h^t = (\id_S; h)^t = h^t`$
$`\quad h^t; \id_t = h^t ; {\id_T}^t = (h; \id_T)^t = h^t`$
圏 $`\cat{C}/B`$ は、特定された終対象 $`\mbf{1}_B`$ を持ちます。それは、$`\cat{C}`$ の射 $`\id_B`$ です。
$`\quad \mbf{1}_B := \id_B \; \in |\cat{C}/B|`$
$`\mbf{1}_B \in |\cat{C}/B|`$ が終対象であるなら、任意の対象 $`s \in |\cat{C}/B|`$ から唯一の射 $`!_s : s \to \mbf{1}_B \In \cat{C}/B`$ があるはずです。$`\cat{C}/B`$ の射（$`\cat{C}`$ の可換三角形） $`!_s`$ は次のように与えられます。
$`\quad !_s := s^{\id_B}`$
$`\quad \xymatrix{
S \ar[dr]_{s} \ar[rr]^{s}
&{}
&B \ar[dl]^{\id_B}
\\
{}
&B
&{}
}\\
\quad \T{commutative }\In \cat{C}
`$
さて、$`\cat{C}`$ の一般の射 $`f:A \to B \In \cat{C}`$ があるとします。これは、$`\cat{C}/B`$ の対象（射ではない）とみなせます。$`f \in |\cat{C}/B|`$ ですね。終対象 $`\mbf{1}_B\in |\cat{C}/B|`$ から、対象 $`f \in |\cat{C}/B|`$ への射はどうなるかを見てみましょう。
$`h^f:\mbf{1}_B \to f \In \cat{C}/B`$ は次の可換三角形です。
$`\quad \xymatrix{
B \ar[dr]_{\id_B} \ar[rr]^h
&{}
&A \ar[dl]^f
\\
{}
&B
&{}
}\\
\quad \T{commutative }\In \cat{C}
`$
可換三角形を等式で表すなら：
$`\quad h;f = \id_B`$
上記の等式を、「セクション〈section〉」という言葉を使って次のように言います。
- $`h`$ は $`f`$ のセクションである。
ここまでにやったことをまとめると：
- $`\cat{C}`$ の一般の射 $`f:A \to B \In \cat{C}`$ を、$`\cat{C}/B`$ の対象 $`f\in |\cat{C}/B|`$ とみなした。
- $`\cat{C}/B`$ の終対象 $`\mbf{1}_B`$ から、対象 $`f`$ への射 $`h^f`$ を考えた。
- このとき、$`h^f`$ の $`h`$ は、$`\cat{C}`$ において $`f`$ のセクションである。
型理論の呼び名・言い回しで言い直すと：
- 型理論の圏 $`\cat{C}`$ の一般の射 $`f:A \to B \In \cat{C}`$ は、別な型理論の圏 $`\cat{C}/B`$ の型とみなせる。
- 新しい型理論の圏 $`\cat{C}/B`$ の、型 $`f`$ のインスタンス $`h^f`$ を考えることができる。
- このとき、インスタンス $`h^f`$ の $`h`$ は、$`\cat{C}`$ において $`f`$ のセクションである。
もとの圏 $`\cat{C}`$ が都合が良い性質を持つなら、新しい圏 $`\cat{C}/B`$ でも型理論を展開できます。次の対応があります。
| 新しい圏 | もとの圏 |
|---|---|
| 型 | 一般の射 |
| 終対象 | 恒等射 |
| インスタンス | セクション |
前節では、$`\cat{C}`$ の一般の射は $`\cat{C}`$ 内の指数対象〈内部ホム〉のインスタンスとして扱いました。この節では、$`\cat{C}`$ の一般の射は別な圏 $`\cat{C}/B`$ の対象（型）とみなしたのです。別な圏 $`\cat{C}/B`$ のインスタンスは、$`\cat{C}`$ で見ればセクションです。
ここまで、$`\cat{C}`$ の対象 $`B`$ を固定して $`\cat{C}/B`$ を作りましたが、任意の対象 $`X\in |\cat{C}|`$ に対するスライス圏構成 $`X \mapsto \cat{C}/X`$ を考えることができます。$`\cat{D}[X] := \cat{C}/X`$ と置くと、（都合の良い仮定のもとで）次のインデックス付き圏〈indexed category〉が得られます。
$`\quad \cat{D}[\hyp] : \cat{C}^\op \to \mbf{CAT}_1 \In \mbb{CAT}`$
ここで、$`\mbf{CAT}_1`$ は、“圏達の2-圏”の2-射〈自然変換〉を捨てた1-圏です。$`\mbb{CAT}`$ はサイズが大きい圏をも含む十分に大きな“圏達の2-圏”です。
今詳しい話はしませんが、圏 $`\cat{C}`$ とそれから作ったインデックス付き圏 $`\cat{D}[\hyp]`$ は、依存型理論のひとつの定式化（局所デカルト閉圏〈locally Cartesian closed category〉と呼ぶ）となります。これは、単純型理論の圏 $`\cat{C}`$ が良い性質を持つなら、それから依存型理論のためのインデックス付き圏 $`\cat{D}[\hyp]`$ を構成可能であることを意味しています。
まとめ
ニュートラルな（クセのない）表現「(f with A) support B」から、型理論向きの動詞 inhabit に変更し、A は終対象に固定して暗黙化すると、型理論における文 f inhabits B が出てきます。型理論特有の言い回しや省略が生まれる背景は、型理論がインスタンスにしか興味を持たないことでした。
インスタンス（終対象からの射）とは限らない一般の射も型理論の枠組み・手法でちゃんと扱えます。ひとつの方法は、（デカルト閉圏の）指数対象〈内部ホム〉へのインスタンスを使う方法です。
もうひとつ、まったく違った方法は、一般の射をスライス圏〈オーバー圏〉の対象とみなす方法です。もとの圏の射を対象として持つスライス圏でも、単純型理論が展開できます。新しい単純型理論におけるインスタンスは、もとの圏のセクションです。
スライス圏構成を、すべての対象に渡って系統的に遂行するとインデックス付き圏が得られます。これにより、各対象ごとの単純型理論を寄せ集めた型理論ができます。個々の単純型理論を束ねた全体は、依存型理論のひとつの定式化となります。
以上の内容に関して、この記事の説明は丁寧なものではありませんでした。が、分野固有の手法・習慣から圏論的概念への翻訳ができるなら、そんなに難しいことではありません。鬼門は、圏論的概念に到着する前に、分野固有の手法・習慣の食い違いに惑わされ疲弊してしまうことです。
前回の記事「カリー／ハワード／ランベック対応のための共通表現」とこの記事の前半を読んで、分野ごとの呼び名・言い回しを無視する能力（分野をまたいだ共通概念にアクセスする能力）をトレーニングしてください。
