型理論と圏論の言葉は次のように対応します。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mfk}[1]{ \mathfrak{#1} }
\newcommand{\In}{ \text{ in } }`$
| 型理論 | 圏論 |
|---|---|
| 型 | 対象 |
| 型宇宙 | 圏の対象達のクラス |
| インスタンス | 射 |
Sets As Types（集合が型だ）の立場をとるならば、次の対応です。
- 型 $`A`$ ←→ 対象〈集合〉 $`A`$
- 型宇宙 $`{\bf Type}`$ ←→ 対象〈集合〉達のクラス $`|{\bf Set}|`$
- 型 $`A`$ のインスタンス $`a`$ ←→ 余域が $`A`$ である射 $`a:{\bf 1} \to A \In {\bf Set}`$
コンテキストの概念を入れるなら、コンテキスト $`X`$ における 型 $`A`$ のインスタンスは：
- 余域が $`A`$ である射 $`a:X \to A \In {\bf Set}`$
型宇宙 $`{\bf Type} = |{\bf Set}|`$ とは別に、論理的計算のための宇宙 $`{\bf Prop} = |{\bf Bool}|`$ を考えます。$`{\bf Bool}`$ は次のような圏です。
- $`|{\bf Bool}| := \{{\bf 0}, {\bf 1}\}`$ （$`{\bf 0}`$ は空集合、$`{\bf 1}`$ は特定された単元集合）
- $`{\bf Bool}(x, y) := {\bf Set}(x, y)`$ （ホムセットは、集合圏のホムセットをそのまま）
定義から、$`{\bf Bool}`$ は集合圏の充満部分圏になります。ホムセットを列挙してみます。
- $`{\bf Bool}({\bf 0}, {\bf 0}) \cong {\bf 1}`$
- $`{\bf Bool}({\bf 0}, {\bf 1}) \cong {\bf 1}`$
- $`{\bf Bool}({\bf 1}, {\bf 0}) = {\bf 0}`$
- $`{\bf Bool}({\bf 1}, {\bf 1}) \cong {\bf 1}`$
圏 $`{\bf Bool}`$ をデカルト閉圏にするために、内部ホムを次のように定義します。
- $`[{\bf 0}, {\bf 0}] := {\bf 1}`$
- $`[{\bf 0}, {\bf 1}] := {\bf 1}`$
- $`[{\bf 1}, {\bf 0}] := {\bf 0}`$
- $`[{\bf 1}, {\bf 1}] := {\bf 1}`$
$`{\bf Bool}`$ におけるデカルト積 $`\land`$ は、ほぼ直積ですが、$`{\bf 1}\land {\bf 1} := {\bf 1}`$ と定義します。厳密に $`x\land y = x \times y`$ ではありませんが、事実上、$`\land`$ と $`\times`$ は同じです。
二元集合 $`{\bf B}\in |{\bf Set}|`$ は（型理論の言葉では）型ですが、$`{\bf Prop} = |{\bf Bool}|`$ は型宇宙です。型 $`{\bf B}`$ と型宇宙 $`{\bf Prop}`$ は別物です。
型理論ベースの論理では、型〈集合〉$`A`$ から型宇宙への写像、つまり、型ファミリー $`P`$ を“述語” と考えます。
$`\quad P : A \to {\bf Prop} \In {\bf SET}`$
一方 集合論ベースの論理では、集合$`A`$ から二元集合（代数構造の台）$`{\bf B}`$ への写像 $`p`$ が“述語”です。
$`\quad p : A \to {\bf B} \In {\bf Set}`$
このギャップをどう埋めるのでしょう？
$`{\bf Set}`$ はトポスなので、部分対象分類子〈subobject classifier〉$`\Omega_{\bf Set}`$ を持ちます。$`\Omega_{\bf Set}`$ は $`{\bf B}`$ だと思ってかまいません。
$`\quad {\bf B} = \Omega_{\bf Set} \In {\bf Set}`$
型ファミリー $`P`$ を、離散圏から“集合圏の部分圏”への反変関手だとみまします（この場合、反変・共変に意味はないですが）。
$`\quad P : A^\mrm{op} \to {\bf Bool} \In {\bf Cat}`$
$`P`$ は前層です。前層に対してグロタンディーク構成、つまり要素の圏〈category of elements〉を作ります。グロタンディーク構成の標準射影と共に次のファイブレーションができます。
$`\quad \pi^P : \int_A P \to A \In {\bf Cat}`$
$`P`$ の値は $`{\bf 0}`$ か $`{\bf 1}`$ だったので、$`\pi^P`$ は単射になります。
この状況を、$`{\bf Cat}`$ から $`{\bf Set}`$ に移します。すると次の図式ができます。
$`\quad \xymatrix{
{\int_A P} \ar@{>->}[d]_{\pi^P} \ar[r]^{!}
\ar@{}[dr]|{\text{p.b. ?}}
& {\bf 1} \ar@{>->}[d]^{t}
\\
A \ar@{.>}[r]
& \Omega_{\bf Set}
}\\
\quad \In {\bf Set}
`$
下のTシャツに記述があるように、トポスでは、モノ射（集合圏では単射）に対して、上の図式の四角形がプルバックになるような射（集合圏では写像） $`p:A \to \Omega_{\bf Set}`$ が存在します。この射〈写像〉$`p`$ が型ファミリー $`P`$ に対応する集合論的述語です。
