HoTTに興味があるCS系の学生が、HoTT本の冒頭を読んだ体験を元に、知っておくと学び易くなりそうな話をまとめてみた。
対象は自分と同じ、型理論は少し知ってる[1]けどホモトピーとかわからんという人。「型理論は知らんけどホモトピー論と圏論の用語はわかる」という人はそのまま本読めばいいと思うし、両方ともわからない人は学ぶモチベーションがよくわからない(し、とりあえずどちらかを学んだ方がいいと思う)のでとりあえず無視する。
HoTTについてはさわり程度の知識しかないまま書かれているため、話半分に読んでもらった方がいいと思う。
最初は自主ゼミでHoTT本を一人輪読した時の資料を公開しようかとも思ったのだけれど、「英語を読むとアナフィラキシーショックで死ぬ」という人でもなければ原文を読んだ方が良いと思う。
書いてみたかっただけなので、多分読んでも得るものは無い。
「The Univalent Foundations Programという集団が提唱している、ホモトピー理論で型理論を意味付ける理論」というのがHoTTの最も端的な説明だと思う。
現在、型理論というものは集合論を使って説明されることが多い。素朴には「型は値の集合」というやつで、とてもイメージし易い。かの有名な型システム入門(TaPL)を見ると、「型とは〜である」という話はしていないものの、型付け関係を二項関係として定義しており、集合論を使っている。
で、型理論で使われている集合論の部分をホモトピー論に置き換えてしまおうというのがホモトピー型理論。
型理論に限らず、ホモトピー論を含めた世の数学は集合論の上に立ってることになっているけれど、ここでは位相幾何学の概念(点とか空間とか)をプリミティブなものとして扱う。つまり「集合と要素」ではなく「空間と点と道」が。さらにその概念を使って集合論を再定義することで、数学全体の基盤まで置き換えてしまおうという考えもあるらしい。
モチベーションとかはよく理解していないけれど、依存型使わない範囲なら別に嬉しさも面白さも無いような気がしている。
ちなみに、HTTと略すとHigher Topos Theoryを指すことが多いようなので注意。
HoTTを学びたいという時に、The HoTT Bookを読む以外の選択肢は現状では無いと思う。
これはどちらかというと数学の人に向けて書かれているので、素直に頭から読んでいっても躓き易い。なので、とりあえず知っておくべき知識と、読むにあたって意識すべきことを並べておく。
どれも、これが無いと読めないというよりは、あれば理解が早いというようなものなので、「わからなければ無視する」というだけでも代用可能かもしれない。
第1章ではホモトピーの話は一切せず、集合にもホモトピーにも依らない型理論の話をしている。
ここで扱われるのはADT的な型なので、ADTを持つ言語の経験があれば楽だろう。
特に依存型を持つ言語[2]に親しんでいる人であれば、第1節と第5節と第10節以降を読めば大体わかってしまうかもしれない。
逆に、依存型理論なんてわかってるという人でも、第12節だけは読んでおくべきだと思う。
HoTTは型理論の概念とホモトピー論の概念を結びつけるものだが、その際に圏論の概念を経由している。そのせいか、説明も無く圏論の用語が出てくるので、面食らってしまうかもしれない。
定義を理解している必要は無いけれど、例えば随伴(adjoint)と言われた時に「2つの構造間の何かしらの対応関係」くらいの認識を持てていると、躓かずに読み進められるはず。
一応2章冒頭で道やホモトピーとは何かについて軽く説明してくれるけれど、視覚的イメージが持てた方が良いと思う。
とりあえず英語版Wikipediaのhomotopyのページにあるgifアニメでも見ておけばいいんじゃなかろうか。