集合論・圏論 vs. 型理論

集合論の所属関係（関係記号は '$`\in`$'）と型理論の居住関係（関係記号は '$`:`$'）は似ているけど違う、という話を「型・インスタンス・宇宙とタルスキ宇宙系列 // 居住関係」でしました。

所属関係と居住関係を区別しなくてもよい場合もあります。しかし、区別しないと“まったくワケワカメ”となる状況もあります。集合と型、要素とインスタンスをどう区別するかを説明します。$`\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\mbf}[1]{\mathbf{#1} }
%\newcommand{\mbb}[1]{\mathbb{#1} }
%\newcommand{\u}[1]{\underline{#1} }
%\newcommand{\Imp}{\mathrel{\Rightarrow} }
\newcommand{\In}{\text{ in } }
\newcommand{\Emp}{\langle\rangle }
\newcommand{\op}{\mathrm{op} }
%\newcommand{\hyp}{\text{－} }
\newcommand{\Iff}{\mathrel{\Leftrightarrow} }
`$

内容：

• 型と型宇宙
• 型の要素とインスタンス
• 前層と余前層
• 要素とインスタンスが一致するケース
• おわりに

型と型宇宙

「型とはなんぞや？」は意味のない問〈とい〉です。「型とは ～～ だとしよう」と約束をして話を始める、というだけのことです。約束をして合意する前には、“型の概念”はありません。型をどう約束するかには幾つもの流儀があります。

• Sets-as-Types
• Algebras-as-Types
• Coalgebras-as-Types
• Propositions-as-Types
• Categories-as-Types
• Logical Relations-as-Types*1
• ‥‥

多くのケースで、型はとある圏（場合により高次圏）の対象だとみなせるので、「型とは対象である」は比較的妥当な主張です。ここから先では、圏 $`\cat{C}`$ の対象が型だとして話を進めます。この状況では、圏 $`\cat{C}`$ の対象の集合 $`|\cat{C}|`$ を型宇宙〈type universe〉と呼びます。

圏論の概念と、対応する型理論の概念は次のようになります。

圏
圏の対象達の集合	型宇宙
圏の対象	型
圏の射	インスタンス
圏の射の余域	インスタンスの型
圏の射の域	インスタンスのコンテキスト

圏そのものに対応する型理論の用語がないのですが、僕は「型銀河」と呼んでいます。

型の要素とインスタンス

集合の「要素」という言葉は、モノの種別や特徴を表す言葉ではありません（「モノの種別とモノの相対役割り」参照）。所属記号 '$`\in`$' の左側に置かれたモノを「要素」と呼ぶだけで、そのモノが何であるかとは関係ありません。

一般的には、型は居住者〈inhabitant〉としてのインスタンスを持つかも知れません。しかし、型が集合とは限らないので、「型が要素を持つ」は本来無意味な言明です。それにも関わらず、ときに「型の要素」という言葉を（勘違いや誤用ではなくて）使うことがあります。これは、型が（集合論の意味の）要素を持つことがある、ということです。

型 $`A`$ が要素 $`\xi`$ を持つことを $`\xi : A`$ と書いてしまうことが多いのですが、この横着が誤解・曲解・混乱のもとです。次のように書きましょう。

$`\quad \xi \in: A`$

これならば、「要素は '$`\in`$' の左」「型は '$`:`$' の右」というルールと整合します。

さて、本来集合ではない型が要素を持つとはどういうことでしょうか？ ひとつの可能性は、「型と呼んではいたが、その正体は集合だった」です -- Sets-as-Types の立場のときですね。もう少し一般的に考えると、「型に集合が対応していた」です。

型に集合を対応させる写像を $`\mrm{E}`$ として、$`\mrm{E}`$ も明示的に書くと：

$`\quad \xi \in: A \text{ via }\mrm{E}`$

次が成立します。

$`\quad (\xi \in: A \text{ via }\mrm{E}) \iff ( \xi \in \mrm{E}(A) )`$

型 $`A`$ が インスタンス（要素ではない！） $`f`$ を居住者として持つ（ホストする）ことは、次のように書きます。

$`\quad f : A`$

これまた誤解・曲解・混乱のもとになる略記です。横着しないで書けば：

$`\quad \Emp \vdash f : A`$

ここで、$`\Emp`$ は空コンテキストです。「空」が付いたからといって空集合を連想したりしないでね、空集合じゃねーから！ 一般的には、コンテキスト $`X`$ のもとで、インスタンス $`f`$ の型〈居住地〉が $`A`$ であることを、型理論では次のように書くのです。

$`\quad X \vdash f : A`$

圏論的に解釈すると次のようなことです。

$`\quad (\Emp \vdash f : A) \iff (f: I \to A \In \cat{C})`$

$`\quad (X \vdash f : A) \iff (f: X \to A \In \cat{C})`$

ここで、$`I`$ は圏 $`\cat{C}`$ の終対象とします。

前層と余前層

任意の圏から集合圏 $`\mbf{Set}`$ への反変関手を前層〈presheaf〉と呼びます。共変でなく反変であることや、「前」と「層」を並べた奇妙な呼び名が気になるかも知れませんが、そういうことは歴史的・偶発的に決まってしまったことなので、気にしてもしょうがありません。

圏 $`\cat{C}`$ 上の前層 $`F`$ は次のように書けます。

$`\quad F: \cat{C}^\op \to \mbf{Set} \In \mbf{CAT}`$

反変関手なので $`{^\op}`$ が付いています。$`{^\op}`$ を取り去って共変関手としたものは余前層〈copresheaf〉と呼びます。共変に「余」が付いているのは、反変関手を使うことが多いからです。

前節では、$`\mrm{E}`$ を写像といいましたが、ここからは 圏 $`\cat{C}`$ 上の余前層だとします。つまり：

$`\quad \mrm{E}: \cat{C} \to \mbf{Set} \In \mbf{CAT}`$

圏 $`\cat{C}`$ と余前層 $`\mrm{E}`$ の組 $`(\cat{C}, \mrm{E})`$ を余前層付き圏〈category with copresheaf〉と呼ぶことにします。実際のところ、これは単なる余前層に過ぎません。余前層の域圏を強調して $`\mrm{E} = (\cat{C}, \mrm{E})`$ という冗長な書き方を採用しているだけです。が、「圏 $`\cat{C}`$ にも注目している」という気持ちの表明にはなります。

$`(\cat{C}, \mrm{E})`$ が余前層付き圏のとき、その対象 $`A \in |\cat{C}|`$ に対して、次の2つの概念が定義できます。

• $`A`$ の要素： $`\mrm{E}(A)`$ の要素を、$`A`$ の要素という。
• $`A`$ のインスタンス： $`\mrm{cod}(f) = A`$ である $`\cat{C}`$ の射 $`f`$ を $`A`$ のインスタンスという。

言い回しは不正確でロクデモナイですが、「そう言うんだからしょうがない」と割り切ります。

それぞれをちゃんと区別して、次の記法を使います。

• $`\xi`$ は $`A`$ の要素： $`\xi \in: A \text{ via }\mrm{E}`$
• $`f`$ は $`A`$ のインスタンス： $`X \vdash f : A`$

集合論・圏論の通常の記法では：

• $`\xi`$ は $`A`$ の要素： $`\xi \in \mrm{E}(A) \In \mbf{Set}`$
• $`f`$ は $`A`$ のインスタンス： $`f: X \to A \In \cat{C}`$

余前層付き圏という構造のなかでは、「要素」と「インスタンス」はまったく別です。

要素とインスタンスが一致するケース

型理論の圏論的モデルとして、デカルト閉圏がよく使われます。圏 $`\cat{C}`$ が単なる（プレーンな）圏ではなくて、終対象、（モノイド積としての）直積、指数対象〈内部ホム対象〉を持つことになります。

デカルト閉圏 $`\cat{C}`$ に対して、その上の余前層 $`\mrm{E}`$ を次のように定義します。

• 対象 $`A\in |\cat{C}|`$ に対して、$`\mrm{E}(A) := \cat{C}(I, A)`$ 、ここで $`I`$ は終対象（かつモノイド単位対象）。
• 射 $`f : A \to B \In \cat{C}`$ に対して、$`\mrm{E}(f) : \mrm{E}(A)\to \mrm{E}(B)\In \mbf{Set}`$ は、ポスト結合前送りで定義する。

このセットアップだと、次が言えます。

$`\quad \xi \in: A \text{ via } \mrm{E}\\
\Iff \xi \in \mrm{E}(A) \In \mbf{Set}\\
\Iff \xi \in \cat{C}(I, A) \In \mbf{Set}\\
\Iff \xi : I \to A \In \cat{C}\\
\Iff I \vdash \xi : A \\
\Iff \Emp \vdash \xi : A
`$

型理論では、圏の終対象を空コンテキストと呼び、$`\Emp`$ などで記すのが習慣です。つまり、型理論の記法で次が言えます。

$`\quad (\xi \in: A \text{ via } \mrm{E}) \iff (\Emp \vdash \xi : A )`$

ここで、次のようなモノグサな略記規則を導入します。

• 余前層 $`\mrm{E}`$ は暗黙の前提として、$`\text{ via } \mrm{E}`$ は書かない。さらに、$`\in:`$ は単に $`:`$ と書いてよい。
• インスタンスのコンテキストが空コンテキストのときは $`\vdash \xi : A`$ と書いてよい。さらに、単に $`\xi : A`$ だけでもよい。

このモノグサな略記規則を使うと、先の同値は、見た目では自明になります。

$`\quad (\xi : A) \iff (\xi : A )`$

ここまでの話では、要素 $`\xi`$ は“終対象からの射”で、一般の射ではありませんでした。しかし、デカルト閉圏では、終対象からの射だけで、事実上すべての射を表現できます。その理由は次の同型です。

$`\quad \cat{C}(A, B) \cong \cat{C}(I, [A, B]) \In \mbf{Set}`$

ここで、$`[A, B]`$ は指数対象〈内部ホム対象〉です。上記の同型を与える写像を $`\mrm{FullCurry}`$ （フルカリー化）とすると、次が言えます。

$`\quad f: A \to B \In \cat{C}\\
\Iff f \in \cat{C}(A, B) \In \mbf{Set}\\
\Iff \mrm{FullCurry}(f) \in \cat{C}(I, [A, B]) \In \mbf{Set}\\
\Iff \mrm{FullCurry}(f) : I \to [A, B] \In \cat{C}\\
\Iff I \vdash \mrm{FullCurry}(f) : [A, B] \\
\Iff \Emp \vdash \mrm{FullCurry}(f) : [A, B]
`$

最後の行にモノグサな略記規則を使うと、単に $`\mrm{FullCurry}(f) : [A, B]`$ と書けます。もとの射 $`f`$ と $`\mrm{FullCurry}(f)`$ を同一視してしまえば、次のように書けます。

$`\quad f : [A, B]`$

指数対象 $`[A, B]`$ を $`(A \to B)`$ とか書くと、圏論的な $`f: A \to B \In \cat{C}`$ と区別が付かなくなります。単なるモノグサ・横着だけではなくて、背後にあるメカニズムを意図的に隠したいという目的で、わざと区別が付かない記法（嘘も方便*2）を採用することもあります。

おわりに

単なるモノグサ・横着であれ、意図的な隠蔽・暗黙化であれ、区別が付かない記法を使って区別しないですごしていれば、概念の峻別には鈍感になります。それでも特に問題も起きずに幸せでいられるかも知れません。しかし、デカルト閉圏ベースの単純型理論の先にある依存型理論などで複雑な構成をしようとすると、幸せではいられなくなります。