「贅沢主義者のグロタンディーク宇宙」でグロタンディーク宇宙の話をしました。贅沢主義か節約主義かは、公理系を設定するときの態度であって、どちらの態度で公理系を設定しても、得られる概念は同じです。
ところで、単一のグロタンディーク宇宙ではなくて、宇宙の無限系列を考えることがあります。
$`\quad U_0 \in U_1 \in U_2 \in \cdots`$
番号を 0 から始めましたが、1 から始めることもあります。番号付け方式の違いはどうでもいい違いです。
宇宙の無限系列を、集合論的に解釈したものをラッセル方式〈Russell-style〉の宇宙系列と呼びます。ラッセル方式の宇宙系列は、型理論との相性が悪いことが指摘されています。型理論と相性が良い宇宙系列としてタルスキ方式〈Tarski-style〉の宇宙系列があります。
この記事では、型、インスタンス、宇宙という型理論の基本概念を復習して、タルスキ方式の宇宙系列〈タルスキ宇宙系列〉を紹介します。$`\newcommand{\mrm}[1]{\mathrm{#1} }
\newcommand{\cat}[1]{\mathcal{#1} }
\newcommand{\In}{\text{ in }}
\newcommand{\mbf}[1]{\mathbf{#1} }
%\newcommand{\Imp}{\Rightarrow}
%\newcommand{\hyp}{\text{－} }
%\newcommand{\dtimes}{\mathop{!\!{\times}} }
%\newcommand{\dto}{\mathrel{!\!{\to}} }
`$
内容：
居住関係
この機会に居住関係についてまとめておきます。
記号 '$`\in`$' で表される集合論の所属関係〈set membership relation〉と、記号 '$`:`$' で表される型理論の関係は、似てはいますが違います。型理論の関係は居住関係〈type inhabitation relation〉と呼びます。
型の居住〈type inhabitation〉に関する用語はフランス語と英語が混じっていてややこしいです（もともとフランス語だったのかも？ 歴史的事実は知らんけど）。
| 語 | 言語・品詞 | 意味 | カタカナ書き |
|---|---|---|---|
| inhabit | 英語 動詞 | 生息する | インハビット |
| inhabited | 英語 形容詞的 | 住人がいる（生息されている） | インハビテッド |
| inhabitant | 英語 名詞 | 住人 | インハビタント |
| habitant | 仏語 名詞 | 住人 | アビト |
| habitat | 英語 名詞 | 生息地 | ハビタ |
| habitat | 仏語 名詞 | 生息地 | アビタ |
| inhabitation | 英語 名詞 | 居住 | インハビテーション |
日本語は、次を使うことにします。
| 居住する、住む | 日本語 動詞 |
| 居住 | 日本語 名詞 |
| 居住者、住人 | 日本語 名詞 |
| 居住地、生息地 | 日本語 名詞 |
| 居住されて、居住された | 日本語 形容詞的 |
「$`A`$ は $`x`$ に居住されている」は $`x:A`$ のことです。ぎごちない言い方になりますね。$`A`$ を主語として受動態でない言い方が欲しいところですが、「$`A`$ は $`x`$ を住まわせる」あたりか？ ウーム、言いにくい。カタカナ語を使いますが「$`A`$ は $`x`$ をホストする」にします。
型理論では、型に居住するモノ（型がホストするモノ）をしばしば項〈term〉と呼びます。しかし、項は構文論的概念なので、この用法は奇妙だし誤解をまねきます。集合の要素〈element〉と一緒にされたくない、ということかも知れませんが不適切です。
ここでは、「項」ではなくて「インスタンス〈instance〉」を使います。「インスタンス」は集合の要素だと思われてしまうリスクが高いのですが、「インスタンスと要素は違うぞ！」と大声で前置きして使う方針にします。
「型」と「インスタンス」を使うことにすると、$`x:A`$ は次の言い回しになります。
- インスタンス $`x`$ は、型 $`A`$ に居住している。
- インスタンス $`x`$ の居住地は、型 $`A`$ である。
- インスタンス $`x`$ は、型 $`A`$ の居住者である。
- 型 $`A`$ は、インスタンス $`x`$ に居住されている。
- 型 $`A`$ は、インスタンス $`x`$ をホストしている。
- 型 $`A`$ は、インスタンス $`x`$ の居住地である。
インスタンス $`x`$ に対して、その居住地〈生息地〉を $`\mrm{habitat}(x)`$ と書くことにすると、次が成立します。
$`\quad x:A \iff \mrm{habitat}(x) = A`$
集合の所属関係では、関数（値が一意的に決まる対応）としての $`\mrm{habitat}`$ を定義することはできません。これは、集合論と型理論の大きな違いです。
型とインスタンスの圏論的な解釈
「集合と要素の所属関係」と「型とインスタンスの居住関係」の違い（と類似性）を理解するには、型理論を圏論的に解釈するのが良い方法です。
現在の型理論の主流は依存型理論ですが、依存性を考えない型理論を特に単純型理論〈simple type theory〉と呼びます。まずは単純型理論から始めましょう。
単純型理論の圏論的解釈は：
- 型とは、とある（都合がいい）圏 $`\cat{C}`$ の対象である。
- インスタンスとは、圏 $`\cat{C}`$ の射である。
- インスタンス＝射 $`x`$ に対して、$`\mrm{habitat(x)} := \mrm{cod}(x)`$
“都合がいい圏”とは、例えばデカルト閉圏です。デカルト閉圏ならば、終対象、直積、内部ホム〈指数対象〉が使えます。
インスタンス〈射〉の居住地である型〈対象〉は $`\mrm{cod}`$ で与えられるのですが、$`\mrm{dom}(x)`$ のほうは $`x`$ のコンテキスト〈context〉といいます。次のように書くと約束しましょう。
$`\quad \mrm{context}(x) := \mrm{dom}(x)`$
こう約束すると、次が成立します。
$`\quad \mrm{context}(x) = X \iff \mrm{dom}(x) = X\\
\quad \mrm{habitat}(x) = A \iff \mrm{cod}(x) = A
`$
「居住地〈habitat〉／コンテキスト〈context〉」などの独自の用語を使うのは致し方ないことです。型理論は圏論とは独立に発展したものですから。後知恵で対応を取っているのです。
圏論における $`x: X \to A \In \cat{C}`$ の、型理論における書き方は次です。この書き方は、型理論の判断形式〈judgement form〉と呼ばれたりします。
$`\quad X \vdash x:A \In \cat{C}`$
型理論では $`\In \cat{C}`$ は実は書きません（圏論じゃないからな）。圏に相当する環境は暗黙に仮定されます。型理論の判断形式に現れるターンスタイル記号 '$`\vdash`$' は特に判断ストローク〈judgement stroke〉と呼ばれます。
都合のいい圏 $`\cat{C}`$ として集合圏 $`\mathbf{Set}`$ を選ぶと、"Sets as Types"〈集合が型だ〉の立場になります。この場合は：
- 型とは、集合圏の対象、つまり集合である。
- インスタンスとは、集合圏の射、つまり写像〈関数〉である。
- インスタンス＝写像 $`x`$ に対して、$`\mrm{habitat(x)} := \mrm{cod}(x)`$
「インスタンスは要素だ」と思いこんでいると、「インスタンスとは写像だ」という解釈に違和感を感じるでしょう。違和感の正体は事前の思い込みなので、その違和感に合理的根拠はありません。思い込みを払拭すればいいだけのことです。
とはいえ、「インスタンス〈写像〉のなかに、要素だと思ってもいいモノもある」のは事実です。次の形のインスタンス〈写像〉をポインティング・インスタンス〈pointing instance〉、あるいは単にポイント〈point〉と呼ぶことにします*1。
$`\quad x: \mbf{1} \to A \In {\bf Set}`$
集合圏以外でも、終対象があればポインティング・インスタンスを定義できます。
集合圏においては、“集合の要素”と“型（これも集合のこと）のポインティング・インスタンス”が一対一に対応します。次の同型が成立する、ということです。
$`\quad A \cong \mrm{Map}(\mbf{1}, A) \In \mbf{Set}`$
集合圏以外の圏や、型理論においては、要素という概念が使える保証はありません。よって、要素は忘れてインスタンスを使うのです。終対象（場合によってはモノイド圏の単位対象）があればポインティング・インスタンス〈ポイント〉が定義できるので、要素の代わりにポインティング・インスタンスを使えます。が、終対象がないなら、ポインティング・インスタンスの定義もできません。
型理論の習慣として、インスタンスを項と呼ぶのは、「項」なら「要素」と勘違いされるリスクが少ないからでしょう。次の表の横の並びはすべて事実上同義です。
| 型理論 その1 | 型理論 その2 | 圏論 |
|---|---|---|
| 項 | インスタンス | 射 |
| 閉じた項 | ポインティング・インスタンス | 終対象からの射 |
| 項の型 | インスタンスの型〈居住地〉 | 射の余域 |
| 項のコンテキスト | インスタンスのコンテキスト | 射の域 |
| 空コンテキスト | 空コンテキスト | 終対象 |
圏の終対象に相当する空コンテキスト*2は、型理論では $`(), \langle\rangle, \diamondsuit`$ のような空リストとして表します。したがって、$`x`$ がポインティング・インスタンスであることは次のように書きます。
$`\quad \langle\rangle \vdash x:A \In \cat{C}`$
空コンテキストの場合、そこに何も書かないことが多いです。
$`\quad \vdash x:A \In \cat{C}`$
さらには、判断ストローク〈ターンスタイル記号〉ごと省略してしまうことがあります。
$`\quad x:A \In \cat{C}`$
圏論ではないので、実際には $`\In \cat{C}`$ は書きません。
$`\quad x:A`$
もし、$`\cat{C} = \mbf{Set}`$ ならば、これは、$`x:{\bf 1}\to A \In {\bf Set}`$ のことなので、次のように書いてもかまわないでしょう。
$`\quad x\in A`$
このように、省略に省略を重ねた特殊ケースにおいては、次が成立すると言えます（言えなくもないです）。
$`\quad x:A \iff x\in A`$
しかし、省略に省略を重ねた特殊ケースを一般的なケースだと誤解するのはとてもまずいですね。型理論の諸概念が、ストレートに集合論的概念に対応するわけではないです。
依存型理論
この記事は、依存型理論の説明をすることは目的にしてないので、手短に大雑把な話だけにします。
依存型理論も圏論的に、特に集合圏において解釈できます。が、解釈は単純型理論のときとは異なります。だいぶ面倒になります。
依存型理論の圏論的解釈は：
- 型とは、とある（都合がいい）圏 $`\cat{C}`$ のバンドルである。
- インスタンスとは、圏 $`\cat{C}`$ のバンドルのセクションである。
- インスタンス＝バンドルのセクション $`x`$ に対して、$`\mrm{habitat(x)} := \mrm{cod}(x)`$
- バンドル-ファミリー対応が使える場合は、$`\mrm{habitat(x)}`$ をバンドルに対応するファミリーだと解釈することが多い。
バンドルやバンドル-ファミリー対応については、以下の記事とそこからリンクされている過去記事達を参照してください。
$`\cat{C}`$ のバンドルの実体は、$`\cat{C}`$ の射です。しかし、バンドルとみなした射は、バンドルの圏（アロー圏、スライス圏、「アロー圏 ＝ バンドルの圏」参照）の対象となるので、役割はまったく違います。
依存型理論のインスタンスに対応するのはセクションですが、バンドル $`f:A \to B`$ のセクションとは次のような射です。
$`\quad s : B \to A \In \cat{C}\\
\quad \text{where } s;f = \mrm{id}_B
`$
依存型理論では、$`A`$ が $`B`$ 上のファミリー $`F`$ のシグマ型となっている場合を考えます。このときの $`f`$ はシグマ型の標準射影〈canonical projection〉です。
$`\quad s : B \to \Sigma(B \mid F) \In \cat{C}\\
\quad \text{where } s;f = \mrm{id}_B
`$
型、インスタンス、インスタンスの居住地の概念は単純型理論より面倒になりますが、インスタンスのコンテキストが域〈domain〉であることは単純型理論と変わりません。ただし、インスタンスの域〈コンテキスト〉が複雑な構造を持つことはあります。
型宇宙
型はインスタンスをホストします。言い方を変えると、インスタンスは型に居住します。では、型をホストするモノは何でしょう？ 言い方を変えると、型は何に〈どこに〉居住するのでしょうか？
型の居住地〈アビタ〉を型宇宙〈type universe〉と呼びます。Agda, Coq*3, Leanなどの型システムは型宇宙を備えています（「最近の型理論： 宇宙と世界、そして銀河」参照）。ただし、「宇宙」でなく「ソート」という呼び名を採用していることがあります。
型宇宙はグロタンディーク宇宙で説明できることが多いのですが、型宇宙の系列をグロタンディーク宇宙の系列だとすると、何かと不都合なようです。このことはルオの論文に書いてあります。
- [Luo12]
- Title: Notes on Universes in Type Theory
- Author: Zhaohui Luo
- Data: October 2012 (Revised on Nov 2, 2012)
- Pages: 8p
- URL: https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf
これは、集合論の所属関係の系列は、型理論とは相性が悪い事の現れです。集合論では、任意の長さの所属関係の系列を作れます。
$`\quad x_0 \in x_1 \in \cdots \in x_n`$
なんなら、可算無限の長さの系列も作れます。
しかし、所属関係を居住関係に置き換えた次のような系列は、型理論では認めたくないのです。
$`\quad x_0 : x_1 : \cdots : x_n`$
認めてよいのは次のいずれかの形だけです。
$`\quad \text{インスタンス} : \text{型}\\
\quad \text{型} : \text{型宇宙}\\
\quad \text{インスタンス} : \text{型} : \text{型宇宙}
`$
これは、次の素朴な発想を否定することになります。
- （否定される発想）型宇宙は、より大きな型宇宙のインスタンスである。
否定されるべき発想に基づいてやっていても、何だかうまくいってしまうのですが、上記ルオの論文にその事情も書いてあります。強制部分型付け〈coercive subtyping〉を使うと、型宇宙系列を否定されるべき発想〈ラッセル方式の型宇宙系列〉で扱っても（見かけ上は）大丈夫とのことです。
タルスキ方式の宇宙系列
型宇宙の系列を考える際の、タルスキ方式〈Tarski-style〉を説明します。
$`U`$ を型宇宙（以下、単に宇宙）として、$`U'`$ を $`U`$ より上位の宇宙とします。ラッセル方式〈集合論方式〉のように、$`U \in U'`$ とは考えません。$`U`$ と $`U'`$ のあいだには、集合論的所属関係も、型理論的居住関係もないとします。
$`U`$ は直接的に $`U'`$ に居住することは出来ません。が、$`U`$ の代理（あるいはレイフィケーション、「ゲーデルの発想の応用としてのメタプログラミング、そして妖精さん達」参照）である型 $`u`$ が $`U'`$ 内に居住しているとします。型 $`u`$ は宇宙 $`U`$ のコード〈code〉と呼びます。$`U`$ のコード $`u`$ は $`U`$ そのものではないことが重要です。
コード化された宇宙 $`u`$ （$`U`$ ではない）をデコードして宇宙に戻す操作を $`T`$ とします。$`T`$ をデコーディング演算〈decoding operator〉と呼びます。デコーディング演算で、コードは宇宙に戻るので：
$`\quad T(u) = U`$
$`T`$ は、$`u`$ 以外の型 $`b:U'`$ にも $`T(b)`$ が定義されている関数だと思ってかまいません。
これだけだと、$`U`$ に住む型達と $`U'`$ に住む型達は何の関係もありません。下位の宇宙 $`U`$ に居る型は、上位の宇宙 $`U'`$ にも居ると考えたいですよね。直接的にそうは出来ないので、型を上位の宇宙に持ち上げて〈lift して〉埋め込む関数 $`t`$ を想定します。
$`\quad t: U \to U'\\
\quad t(a) : U' \text{ for }a:U
`$
$`t`$ をリフティング演算〈lifting operator〉と呼びます。集合論的に $`U \subset U'`$ とは考えないが、リフティング演算 $`t`$ を介して、あたかも $`U \subset U'`$ のように思っても差し支えない状況になっています。
なんで直接的に $`U\in U'`$ や $`U\subset U'`$ を許さないのかと言うと、“型の型”、“型の型の型”、‥‥ のような概念を野放図に使われると、ろくでもないことになる場合もあるからです。
タルスキ方式で宇宙の無限系列を作るには、番号 $`i = 0, 1, 2, \cdots`$ に対して次のモノを準備します。
- 宇宙 $`U_i`$
- 宇宙のコード $`u_i : U_{i + 1}`$
- デコーディング演算 $`T_i : U_i \to \mathbb{TYPE}`$
- リフティング演算 $`t_i : U_i \to U_{i + 1}`$
ここで、$`\mathbb{TYPE}`$ は“広義の型の集まり”です。広義の型とは、なにかをホストする能力があるモノです。型はインスタンスをホストする能力を持ち、宇宙は型をホストする能力を持つので、型も宇宙も広義の型です。
その他の宇宙
グロタンディーク宇宙は、ZFC集合論内で作れる集合論的宇宙です。ラッセル方式の宇宙系列は、宇宙達が所属関係で繋がっている素朴なアイディアに基づく宇宙系列です。タルスキ方式の宇宙系列は、ラッセル方式に比べて複雑ですが、型理論との相性は良くなっています。
ほかに、ホフマン／ストレイカーによる宇宙があります。
- [HS97-]
- Title: Lifting Grothendieck Universes
- Authors: Martin HOFMANN, Thomas STREICHER
- Date: Spring 1997
- Pages: 4p
- URL: https://www2.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf
ヴォエヴォドスキーの宇宙も、ホフマン／ストレイカー宇宙をヒントにしているのかも知れません。ヴォエヴォドスキー宇宙に関しては、以下の記事で書いています。
