■

[HoTT]HoTTをこっそり学ぶ　その１

HoTT始めました。HoTTとはHomotopy Type Theoryの略語であり、またその最初のテキスト（？）である『Homotopy Type Theory　Univalent Foundations of Mathematics』というタイトルの本（電子本もネットに落ちている）も指している。著者は『The Univalent Foundations Program』というグループで、前書きによるとたくさんの人々が参加しているようである。さて、その内容となると実はまだ私は理解できていない、というかアウトラインを聞いても方向性がなんのこっちゃなのである。これもネットに落ちている上村太一氏の『Homotopy Type Theory入門』から引用させていただくと

『Homotopy Type Theory (HoTT) は 依存型理論の拡張で、ホモトピー論に特化した型理論である。代数トポロジーと計算機科学の橋渡しとなる分野であり、ホモトピー論、高次圏論、数理論理学、定理証明器、依存型プログラミングなどと関わりが深い。特に定理証明器を用いた代数トポロジーおよび数学全般の形式化に使われており、HoTT による数学の基礎付けとその定理証明器上での実装は Univalent Foundations program と呼ばれる。』

とのこと。ホモトピーの計算を計算機でやるといっている一方で、集合論に代わる数学全般の形式化という大それたことも目指しているようなのである。どっちやねん。

型理論を数学の基礎に据えようというアイデアは1970～80年代からあるようで、Curry－Howard対応により、論理とプログラミングはほぼ同じものとの理解からプログラミングの方から数学を基礎づけるというアイデアである。ただまあ、ちゃんと調べたわけではないが、それだけだと70年代の構成主義的な立場から数学を基礎づけたBishopらの結果を超えるようなものではないんじゃなかろうかという気がする。コンピュータでの自動証明というようなことも一時流行ったような流行ってないような？
しかし、どうやらHoTTは”型理論＝プログラミング”に”ホモトピー論”を加えることによりその上を行こうという発想らしい。数学の基礎付けうんぬんはともかくとしても、依存型理論という型理論のひとつにunivalence axiomという公理とHigher inductive typeという型を加えることで、ホモトピー理論をプログラミングとして理解できるというのが驚きではある。本当にの基本群やら、とかが計算できるというのだ（すいません。ホモトピー論はまともに勉強していないので、はともかく後者がどれくらいすごいのかすごくないのかは判断つきません。精進します）。

ともかくHoTT本をネット上の勉強会に参加して読み始めてみたわけであるが、うーむ、これは私には合ってない。本書の前書きにも述べられているが、全編インフォーマルと称していて、通常の数学書の体裁とはかなりちがっており、だらだらとHoTTについてのあることないことが述べられている。すくなくともIntroductionはそうである。章が進むにつれて、ましになってくるらしいが、勉強会でも『ここはこういう意味かなぁ』で保留した箇所がたくさんある。我慢である。一方、依存型理論とホモトピー理論は　∞-groupoid を通じて関連しているとの情報を得て、こっち方面からも攻めてみようということで、 Cisinski "Higher Categories and Homotopical Algebra"

Higher Categories and Homotopical Algebra (Cambridge Studies in Advanced Mathematics)

も読み始めた。 なんとこんなところに以前のカテゴリー論の勉強が役に立つとは。こちらはまっとうな数学本で気分がいい。タイトルが仰々しいが、いまのところちょっと背伸びしているぐらいの難易度である。ちなみにこの本も著者が電子版を公開しているのでタダで読めるのもありがたい。例によって、HoTT本やCisinski本をネタにして気になったところを紹介していきたい。