Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory

ビッグピクチャー： 「回転する」集合の宇宙を築く

想像してみてください。あなたはオブジェクト（集合）の宇宙を構築しています（伝統的な数学（「整礎的」な集合論）では、すべてのオブジェクトはより小さなオブジェクトによって作られ、その小さなオブジェクトはさらに小さなものによって作られ、最終的に「無」へと辿り着きます。それはピラミッドのようなものです。ブロックが宙に浮いていることは許されず、必ずその下に何か基盤がなければなりません。

しかし、もし、オブジェクトが自分自身の上に成り立つような宇宙を築きたいとしたらどうでしょう？ 例えば、自分自身を含んでいる箱があったら？ あるいは、箱Aが箱Bの中にあり、箱Bが箱Cの中にあり、そして箱Cが箱Aの中にある、というような箱の連鎖があったら？ 伝統的な数学では、これは無限ループを生み出すため禁止されています。この論文では、著者たちが**ホモトピー型論（HoTT）**と呼ばれる現代的なフレームワークを用いて、このようなループを「許容する」数学的宇宙をどのように構築できるかを探求しています。

この論文は主に2つのことを行っています：

1. **スコット（Scott）**という数学者が定めたルールに従い、ループを許容する集合のモデルを構築すること。
2. **アツェル（Aczel）**という数学者が定めたルールに従い、ループを許容する別の集合のモデルを構築すること。

ツール：木、余代数、そして「展開」

これらのモデルを理解するために、**「木（ツリー）」**を想像してください。

• **整基礎的な木（古い方法）**は、家系図のようなものです。根があり、枝があり、最終的には葉（末端）に到達します。これらは成長を止めます。
  এটি。
• 非整基礎的な木（新しい方法）は、フラクタルや合わせ鏡のようなものになり得ます。枝がループして再び根に戻ったり、あるいは一つの枝が分割されて、全体と全く同じ見た目の枝が二つ現れたりします。

著者たちは、これらの木を記述するために**余代数（Coalgebra）**という概念を使用しています。余代数を「マシン（機械）」と考えてください。そのマシンは、あるノード（節点）を見て、次に何が来るかを教えてくれます。

• マシンが「停止」と言えば、それは葉です。
• マシンが「これらの子要素へ行け」と言えば、それは枝です。
• マシンが「あなた自身である子要素へ行け」と言えば、それはループです。

論文は問いかけます：あらゆる可能なループを記述できる「究極の」マシンとは何か？

2つのモデル：スコット vs アツェル

著者たちは、これらのループを扱うための2つの異なる「究極のマシン（数学的モデル）」を構築しています。これらは、ループする世界における「等しさ（等価性）」の扱いに関する、2つの異なる哲学に対応しています。

1. 「鏡」モデル（スコットの非整基礎公理）

• 比喩： 合わせ鏡を想像してください。鏡の前に立つと、反射が見えます。その反射がまた別の鏡の中にあるなら、反射の反射が見えます。
• ルール： このモデルでは、2つのオブジェクトは、その**展開パターン（unfolding patterns）**が同じであれば「等しい」とみなされます。もし、集合の層を（玉ねぎの皮を剥くように、あるいは木を展開するように）解き続けていき、その枝のパターンが別の集合と同一であれば、それらは同じものです。
• 結果： 著者たちは、このモデルとして機能する特定のタイプの木構造（$V^0_\infty$ と呼ばれるもの）を構築しました。これは「不動点」であり、宇宙のルールを適用すると、再び同じ宇宙が得られます。
• 主要な発見： このモデルは、厳密な意味での「最終的（terminal）」なマシンではありません。それは「第3の選択肢」です。出発点（initial）でもなければ、絶対的な終着点（terminal）でもありません。その中間地点に位置しています。これは、ループの識別に対してより厳しい制限を持つ、スコットのルールを満たしています。

2. 「普遍的」モデル（アツェルの非整基礎公理）

• 比喩： 自分自身について語る物語を含む、あらゆる可能な物語を収めた「マスター・カタログ」を想像してください。
• ルール： このモデルでは、あらゆるグラフ（点と線の図）を集合に変換できます。もしループを描いた図があれば、その図と完全に一致する一意の集合が存在します。
• 結果： 著者たちは、この目的のための「終結余代数（Terminal Coalgebra）」（究極のマシン）を構築しました。しかし、この特定のマシンを構築するためには、**命題のリサイズ（Propositional Resizing）**と呼ばれる、特殊でやや議論の余地のある数学的ツールを使用する必要がありました。
  • 命題のリサイズとは？ あなたが膨大な本のライブラリ（命題）を持っていると想像してください。このツールを使うと、物語の内容を失うことなく、ライブラリ全体を凝縮して、たった一つの棚に収まるようにできるのです。これは、構築を可能にする強力なショートカットです。
• 主要な発見： このモデルはアツェルのルールを満たしています。これは「終結的（terminal）」なオブジェクト、つまり、これらのルールの下で可能な、最も完全なループする集合の宇宙です。

「同一性」のパズル：何が二つのものを同じにするのか？

この論文の主要な部分は、トリッキーなパズルを解くことです：2つのループする木が実際に同じであると、どうすればわかるのか？

標準的な数学では、二つのものが同じように見えれば、それらは等しいとされます。しかし、ループのある世界では、物事は奇妙になります。

• 著者たちは、これら2つのループする木の間にある「等しさ」が、別の種類の木（「インデックス付きM型」）として記述できることを発見しました。
• 比喩： 二つの無限のフラクタルを比較しているところを想像してください。それらが同じであることを証明するには、単に全体の絵を見るだけでは不十分です。あらゆる枝、あらゆる小枝、そしてあらゆる小々枝を一つずつ比較しなければなりません。論文は、この比較を行うための正確なレシピ（「特徴付け」）を提供しています。彼らは、これら複雑なループの「等しさ」自体が、構造化された無限のオブジェクトであることを証明しました。

成果の要約

1. スコットのモデル： ループを許容し、等しさが「展開」される木の形状によって決定される集合の宇宙を構築しました。これは不動点ですが、絶対的な「終結的（terminal）」なものではありません。
2. アツェルのモデル： あらゆるグラフを集合に変換できる、ループを許容する「究極の」集合の宇宙を構築しました。これには、命題のリサイズという特別な数学的仮定が必要でした。
3. 「等しさ」のレシピ： これらの無限のループ構造における「同一性」を定義する方法を正確に解明し、等しさがまさに別の種類の木構造であることを示しました。
4. 形式化： 彼らはこれを単に紙に書いたのではありません。論理的なステップに間違いがないことを確認するために、Agdaというコンピュータプログラムの中で構築しました。

なぜこれが重要なのか？

この論文は、現実世界のエンジニアリング問題や医療問題を解決しようとしているわけではありません。むしろ、数学の基礎的なパズルを解決しようとしています。これは、現代の計算機科学の論理（ストリームや遷移システムのような複雑な循環データ構造を扱う必要があるもの）と、古典的な集合論（ループを禁止するもの）との間の溝を埋めるものです。

要するに、彼らは物事が自分自身を含むことができる2つの異なる「宇宙」を構築し、それらが特定のルールに従って機能することを証明し、そしてそのような自己包含的なものが実際に同じものであるかどうかを判断する方法を正確に示したのです。