HoTT(ホモトピー型理論) はホモトピー論や∞圏論を型システムの上で展開しようという考え方である。この体系は既にCoqで形式化が進んでいる。これはその使い方の覚書である。
まず、HoTT/Coqではなく、HoTT全般に関係する資料について述べる。
- HoTTの本家サイト http://homotopytypetheory.org/ に情報がたくさんある。この分野は数学の他分野に比べて、インターネット上に情報がより集約されているという特徴がある。
- HoTTについて紙面で勉強するならば、上のサイトにあるHoTT Bookを読むのが最も適切である。
- HoTTに関連するコードは主に https://github.com/HoTT/ に集約されている。
- HoTTに限らず、圏論や∞圏論に関係する事柄は nLab http://ncatlab.org/ に充実している。辞典として用いるのに便利である。ただし、積極的にカテゴリカルな記述をするなど先鋭的であり慣れていないとわかりづらい場合があるので、書籍やWikipediaなどの他の資料と併用するとよいかもしれない。
- HoTTについて書かれているブログの例 http://d.hatena.ne.jp/m-a-o/ http://d.hatena.ne.jp/m-hiyama/
HoTT/Coqは次の二つからなる。
- HoTT用にカスタマイズされたCoq
- 上のCoqで動作する証明ライブラリ
1のみのパッケージは https://github.com/HoTT/coq/ から入手できる。使い方は通常のCoqとほぼ同じである。特徴として、HIT(高階帰納型)を擬似的に実現するためのPrivate Inductive命令が使えることと、宇宙多相性に対応していることが挙げられる。
宇宙多相性は適当なオプションをつければ有効化できるので、「8.5が待てない、今すぐ宇宙多相性が使いたい」という人も使ってみる価値があるかもしれない。
2のパッケージ https://github.com/HoTT/HoTT/ には git submoduleの形で1のパッケージが同梱されている。したがってHoTTをCoqで始めたい人はこれを使えばよい。
インストール方法はREADMEを読め (Ubuntu等のLinuxに入れるのがオススメ)
HoTT/Coqのcoqdocは http://hott.github.io/HoTT/coqdoc-html/toc.html にある。
coqdocではなくproviolaを用いたものは http://hott.github.io/HoTT/proviola-html/toc.html にある。
これらのファイルの実体は https://github.com/HoTT/HoTT/tree/gh-pages にあり、これはHoTTが更新されるたびにTravis-CIで自動でビルド＆デプロイされている。
Require Import HoTT.HoTT/Coqライブラリは非常に軽量であり、全てのライブラリをロードしても一瞬で終わる。
Require Import Overture PathGroupoids Equivalences Trunc HProp HSet.
Require Import types.Unit types.Paths types.Sigma types.Forall types.Arrow.
Require Import types.Bool types.Universe Misc.
Require Import hit.Circle.
Local Open Scope path_scope.
Local Open Scope equiv_scope.特に、HoTT/Coqのライブラリ内では Require Import HoTT. を実行してはいけないので注意すること。
Require Import categories.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.HoTT/Coq本体とは異なり、圏論ライブラリの全てのライブラリをロードするのはそれなりの時間がかかる。
Require Import categories.
Require Import categories.Utf8.
Set Universe Polymorphism.
Set Implicit Arguments.
Generalizable All Variables.
Set Asymmetric Patterns.伝統的なCoqと異なり、命題と集合は区別せず、Propは使わない。
Unit… 0項直積 (tt唯一の元)Empty… 0項直和A * B… 2項直積 (pair唯一のコンストラクタ)A + B… 2項直和 (inl,inr左右のコンストラクタ)forall x, P x… 依存直積 / 依存関数空間 (funλ式)A -> B… 非依存直積 / 関数空間 (funλ式)sig Pまたは{ x : _ & P x }… 依存直和 / ファイブレーション (exist唯一のコンストラクタ /sig_rect除去関数)Bool… 2点集合 (true,false左右のコンストラクタ /ifが使える)
x = y…xからyへの道空間x = y :> A…xやyが空間Aの点であることを明示f == g… 関数fとgの間の各点道からなる空間 (Funextはこれがf = gと見なせるということを主張する)A <~> B… 空間AとBの間のホモトピー同値からなる空間 (UnivalenceはこれがA = Bと見なせるということを主張する)Contr A…Aは可縮空間である (Unitとホモトピー同値)IsHProp A…Aは命題である (EmptyまたはUnitとホモトピー同値)IsHSet A…Aは集合である (離散空間とホモトピー同値)IsTrunc n A…Aはn-Truncatedである (nがminus_twoのときContr, nがminus_oneのときIsHProp, nが0のときIsHSet)IsEquiv f…fはホモトピー同値写像
<~>, Contr, IsHProp, IsHSet, IsTrunc, IsEquiv は型クラスである。つまりインスタンスを用意しておけば勝手に補充してくれる。
また、HIT(高階帰納型)として定義される次の型についても把握しておこう。
minus1Trunc A…Aは非空である(という命題) / (-1)-truncationあるいはinhabitedとも呼ぶ。quotient R… 関係Rによる商空間Susp A…Aの懸垂 (ただし、Aが空のときはSusp Aは2点集合となるので注意)S1… 円周S1
1あるいはidpath x…xの恒等道 (=のコンストラクタ)p @ qあるいはconcat p q… 道pとqの合成p ^… 道pの逆道ap f p… 道pを関数fで写す。f : A -> B,p : x = yのとき、ap f p : f x = f y。fのpへの適用(application)または道への作用(action on path)transport P p zあるいはp # z… 値zを道pに沿って輸送する。複素積分と同様に、輸送する道が異なると輸送した結果は異なる可能性がある。p:x=yのときにtransport P p : P x -> P yapD01とか色々 …apの亜種(一般化)transportD…transportの亜種(一般化)s @@ t… 2次元道の水平合成whiskerL p t… 2次元道を左からずらすwhiskerR s q… 2次元道を右からずらすcancelL,cancelR…whiskerLとwhiskerRの逆f ^-1…fがホモトピー同値写像であることがわかっているとき、その逆写像
定理だと思って書いていたらゴールにこれらの名前が出てくるなんてこともよくあるから実際には一概に「定理」とは言えない。
concat_p_ppとかconcat_pp_p… 結合法則 (名前から性質を読み取れるようにせよ)concat_1pとかconcat_p1… 左および右から恒等道を合成しても変わらないconcat_pVとかconcat_Vp… 左および右から逆道を合成すると消えるinv_pp… 合成の逆は逆の合成ap_1…ap _ 1は1ap_pp… 合成への作用は作用したものの合成ap_const… 恒等関数を作用させると1になるtransport_const…transport (fun _ => Const)を見つけたら大体これによる書き換えが正解transport_arrow…transport (fun x => A x -> B x)を見つけたら大体これtransport_forall…transport (fun x => forall y:A x, B x y)を見つけたら大体これtransport_hoge…transport (fun x => hoge)を見つけたら大体これ (適当)
たぶんOvertureとPathGroupoidsとtypes.Pathsの定義や定理は最終的には全部覚えないといけないんじゃないかという気がする。(もちろん最初から暗記する必要はない)
まずHoTTでは、Coqの通常の証明モードの使い方
Lemma FooBar : forall X, BarBaz.
Proof.
yokini.
hakaratte.
Qed.
の他に、定義をするための証明モードの使い方
Definition FooBar : forall X, BarBaz.
Proof.
nanka.
tsukuru.
Defined.
をよく使う。(QedではなくDefinedを使っていることがポイント。)また、ここでDefinitionをInstanceに変えたものもよく使う。
よく使うタクティック
refine… 値を直接与える。ただし、空欄補充に失敗したらそれを次のゴールにする。refine (foobar @ _)… 等式の証明で左側を書き換えていくときに結構使う。rewrite H… 通常のCoqのrewriteと全く同じ。HoTTの=でも使えるということ。simpl… HoTTでも重要。simplを実行しても見た目が変わっていない場合でも、表示されていない項がこっそり変化して使いやすくなっていることがある。hott_simpl… HoTT特有のめんどくさい書き換えのうち、自明なものをやってくれる。change… 項の形のせいで進まないタクティックを力技で何とかする。unfold… HoTTでも重要
よく使う戦略
transpose (fun _ => _)を見つけて、funの中身が特定の形をしていたら、それを分解するための定理を使って書き換えるとうまくいくことがある。x = yの形をしているある道pについて、destruct pは成功したり失敗したりする(たいてい失敗する)。複雑な式が、このタクティック一本で単純化されることもある。しかし、適切な場所で適切なものをdestructするには慣れが必要。Definition thm ... Definedで作ったものの中身がゴールに出てくると、thmが巨大だと悲惨。定義したものは細かく分ける必要が出てくることがある。- 透明な定義にするか、不透明な証明にするかの判断は重要。その型が
IsHPropだったら不透明な証明にしてもだいたい問題ない。そうでなかったら、透明である必要があることが多い。
HoTTは将来的に全てのコードが実行可能となることが期待されているが、現在は実行できないものがいくつかある。それは
- 関数外延性 (
Funext) - 単葉性 (
Univalence) - 高階帰納型 (HIT)
また、HoTT/Coqのライブラリには無いようだが、例えば次のような公理を導入することができる。
- 命題に対する排中律、命題に対する二重否定除去則
- 集合でインデックスされた集合族に対する選択公理
- 集合でインデックスされた型の族に対する選択公理
Higher Inductive Typeは例えば次のように定義できることが期待されている。
Inductive S1 : Type :=
| base : S1
| loop : base = base.
Definition S1_rect(P : S1 -> Type) (b : P base) (l : loop # b = b) (x : S1) : P x :=
match x return P x with
| base => b
| loop => l
end.そして、S1_rect P b l baseはbaseに、apD (S1_rect P b l) loopはlに簡約されることが期待されている。
現在はこれをPrivate Inductiveという仕組みとAxiomを使って擬似的に実現している。 (Circle.v参照)
このとき、S1_rect P b l baseはbaseに簡約されるが、apD (S1_rect P b l) loopはlに簡約されない。代わりにこの2つが等しいことを示す公理がある。
UnivalenceとFunextは、どこで仮定しているかがわかるように型クラスの形で持ち回している。
これらの公理を使うには、例えば
Definition foo `{Univalence} (P:Type) ... := ... .とか、
Section AssumeUnivalence.
Context `{Univalence}.
...
End AssumeUnivalence.とか書く。