妄想かも知れない、トンチンカンかも知れない、雑感。
内容：
チャーチ／チューリングの提唱
チャーチ／チューリングの提唱〈Church-Turing thesis〉とは、およそ次のような主張です。
- 計算可能性の概念は、どのような方法で定義しても同値になる。
これは、チャーチ／チューリングの定理でもチャーチ／チューリングの公理でもなく、提唱〈テーゼ〉です。主張を正確に述べることもできないし、もちろん証明もできません。経験則を指導原理として位置付けたものでしょう。
計算可能関数の定義は色々とあります。
これらの方法で定義される関数のクラスが同じであることは証明できる（証明された）定理です。まったく異なる定義が同じ関数のクラスを定義するのです。この事実から、直感的な「計算可能」という概念は、定義によらない普遍的な概念であるように思えます。
その「思い」を言葉にしたのがチャーチ／チューリングの提唱なんでしょうが、それを言ったからってなんなんだ？ というスッキリしない感じが残ります。
高次圏論
高次圏論でも同じような事情があります。誰かが提唱したわけではないので、名前は付いてませんが、多くの人が次のような「思い」を抱いているでしょう。
- 高次圏の概念は、どのような方法で定義しても同値になる。
高次圏の定義も色々とあります。2004年に書かれたチェン／ラウダの高次圏の教科書がありますが：
- Title: Higher-Dimensional Categories: an illustrated guide book
- Authors: Eugenia Cheng and Aaron Lauda
- Pages: 182p
- URL: http://cheng.staff.shef.ac.uk/guidebook/guidebook-new.pdf
その目次を見てみましょう。
- 2. Penon
- 3. Batanin and Leinster
- 3.3 Leinster
- 3.4 Batanin
- 4. Opetopic
- 5. Tamsamani and Simpson
- 5.3 Simpson's definition .
- 5.4 Tamsamani's definition
- 6. Street
- 7. Joyal
- 8. Trimble and May
- 8.1 Trimble
- 8.2 May
4章のOpetopic以外はすべて人名です。OpetopicもBaez-Dolanとすれば、11人の人名が並びます。それぞれの人がそれぞれの定義を提案しています。
計算可能性の場合とは違って、異なる定義が同値であることの証明は難しく、同値性が証明された例は少数です。「どのような方法で定義しても同値になる」は、経験則と呼ぶには弱く、希望的観測や努力目標といったところでしょう。
n-圏は、次元n以外のもうひとつの整数mを使ってより細かい分類がされます。(n, m)-圏とは、m次を超える射がすべて可逆であるn-圏です。チェン／ラウダの教科書で扱っているのは(n, n)-圏（nが無限でもよい）で、その後で多用されるようになった高次圏に(∞, n)-圏があります。
バーウィック／ショマー=プリの唯一性定理
高次圏の場合は、定義がたくさんあり、それらの定義を書き出すのも難しく、定義の同値性を示すのも難しく、「いったいどうすりゃいいんだ？」な状況です。一見、混沌とした状況に対して、別なアプローチをする人もいます。「高次圏とは何か？」に答えるのではなくて、「高次圏“論”とは何か？」に焦点を移すのです。
「高次圏とは何か？」にはたくさんの人がそれぞれの定義を持ち、それぞれに高次圏論を展開しています。それらの高次圏論（高次圏ではない）に共通する特徴を探して、高次圏論を公理化しよう、というわけです。
卑近な例で言えば； 「ベクトルとは何か？」は今は問題にされないでしょう。単に「ベクトル空間の要素」です。公理化されて興味の対象となっているのは「ベクトル空間」のほうです。同様に、高次圏とは単に「高次圏論で扱う対象」で済ませるのです。
バーウィックとショマー=プリは、(∞, n)-圏論を公理化して、その公理を満たす(∞, n)-圏論は、本質的には（ある種のupto-isoで）1つしかないことを示しています。
- Title: On the Unicity of the Homotopy Theory of Higher Categories
- Autohrs: Clark Barwick, Christopher Schommer-Pries
- Pages: 45p
- URL: https://arxiv.org/abs/1112.0040
上記論文の最初の投稿は2011年末（30 Nov 2011）ですが、今年（7 Aug 2018）になって大幅にリライトされてます（Completely rewritten）。改善が続けられて、読みやすくなったのでしょうが、僕にはハードル高すぎ。
テクニカルな内容は追えないまでも、バーウィック／ショマー=プリの戦略は見当が付きます。
- 対象物そのものではなくて、対象物を扱っている理論に注目する。
- その理論を公理化する。
- 公理化された理論は、本質的には唯一であることを示す。
- 現在知られている理論が公理を満たすことを確認する。
- 複数の理論が同値であることが分かる。
- どの理論を使っても、（ある抽象レベルでは）同じ結果が出ることが保証される。
もう一度チャーチ／チューリングの提唱
さて、冒頭のチャーチ／チューリングの提唱ですが、バーウィック／ショマー=プリと同様な戦略で、定理にできないものでしょうか？ 「計算可能性とは何か？」ではなくて「計算可能性の理論とは何か？」に注目して、計算可能性理論を公理化するというアプローチです。計算可能性の場合は、直接的・個別的に同値性が証明できたので、理論の公理化の必要性はなかったのでしょうが、計算可能性が「定義によらない普遍的な概念」だとすれば、定義・定式化をどうしようが本質的に唯一の概念的実体を記述する、という形の定理があってもよさそう、と思うんですが。
