Coqと少しの圏論が分かる人向けのhomotopy type theory(その1) -

The HoTT Book
http://homotopytypetheory.org/book/
が完成したらしいけど、どっちかというと、数学者向けに書かれてて500ページもある。homotopy type theoryで今できてることって、CoqやAgdaで書いたら、せいぜい数千行とか、そんなもんじゃないかと思うので、長すぎる気がする

一応、HoTTに関わる知識は、型理論の他に、ホモトピー論や圏論(モナドとかHaskell関連で出てくる類の知識はあまり知らなくてもいいけど、higher categoryとか教科書に書いてなさそうな話題や、モデル圏とかを知ってるといい)があって、全部真面目に勉強しようと思うと、それぞれのテーマで一冊以上の本が書ける。ただ、実際には、ホモトピー論や圏論はアイデアや視点を提供しているだけで、あくまでCoqやAgdaで書かれてる部分が重要なので、ホモトピー論や圏論の知識がなくても、無心にCoqやAgdaのコードを眺めてれば何とかなる(べきである)気がする(まぁでも、基本群って何?とかgroupoidっておいしいの?とかいうレベルだと辛いのかもしれない。というか、誰かが書いた解説を読んでも、用語レベルで詰まりそうではある)

前置き(1)homotopy type theoryで何が出来るのか

homotopy type theory(以下HoTT)は、2006年頃、VoevodskyとAwodeyが創始したということになってて、HoTTの研究は、type theoryという名前だけど、現在数学者主導で進められている。現在、HoTTには2つの側面があるように思う
(1)数学の新しい基礎(univalent foundation)としてのHoTT
(2)形式化されたホモトピー論としてのHoTT

(1)はVoevodskyが言い出したことになっていて、特にunivalent foundationという標語は、Voevodskyによるものだけど、CoqやAgda(のベースとなっているMartin Lof type theoryやCIC)に、"何らかのextensionality principle"を追加しようという試みは、HoTTより、ずっと以前からなされていて、計算機科学方面の人にとっては、HoTTは、そのような試みの一つとして捉えられているらしい(別の試みとしては、例えばAltenkirchという人のObservational Type theoryとかがある)。

これは(Martin-LofやThierry Coquandのような人が容易に解決できない程度には)難しい問題だと思うけど、それで何か大きなメリットがあるかというと、
Extensional versus intensional
http://en.wikipedia.org/wiki/Intuitionistic_type_theory#Extensional_versus_intensional
には、"In contrast in intensional Type Theory type checking is decidable, but the representation of standard mathematical concepts is somewhat complex, since extensional reasoning requires using setoids or similar constructions"と書いてあって、要するに、"商集合"を自由に作れないので、数学をやるのが大変になりますということ。普通のプログラムやアルゴリズムの性質を証明するに当たって、よいこと(より分かりやすい証明が書けるとか、コードが短くなるとか)があるかどうかは分からない。全く確約はできないけど、例えば、多項式のようなデータを作る時、今は、"syntacticな式の集合"を定義して、等しいかどうかの判定などには、適当な正規化関数を作って、正規化した結果が等しいかどうか見るという実装になるけど、このへんの実装や証明が自動化、半自動化されるというようなことは起こるかもしれない(妄想だけど)。

何にせよ、問題意識としては、Voevodsky以前から、計算機科学方面の人には知られていたことではある。今のところ、HoTTが以前の試みと比べて、何か大きく成功しているということはない

(2)は、ShulmanとかLumsdaineといった人たちが2010年頃からやっている話で、数学の一分野であるホモトピー論をCoqやAgda上で再構成してやろうという試みであるし、別の見方をすれば、型のホモトピー論をやっているともいえる。HoTT Bookも、こっち方面の人が書いているっぽい。VoevodskyやAwodeyのような人は、こっち方面の話題には殆ど関わってこないし、現在主にみんながやっているのは、"球面"のホモトピー群の計算をしようという問題で、数学的な動機が強いと思うのだけど、それが出来たところで、univalent foundationと関連してくるかというと、今のところ、わたしには直接的な関係は見えない

・数学の新しい基礎とか必要なん?集合論じゃダメなの?
Voevodskyは特にhigher category theoryをやる時に困ると言ってる。HoTTは、商集合を自然に作ることができるだけでなく、higher category theoryをやるのにも自然な枠組みを与えると期待されていると言える。ただ、今"普通の"数学やる人は、higher categoryを使わないし、そもそも、数学の基礎なんて、別に必要ともしていないと思う

・MizarやHOLじゃダメなの?
数学をコンピュータ上に形式化しようという試みは、CoqやAgda以外にもいくつかあって、それなりに成功しているように見える。けど、そのへんの話は、よく知らない

・何故ホモトピー論をCoqやAgdaで形式化するのか?
何か綺麗に出来そうだからというのが一つの答え。もうちょっと意識の高そうな答えは、それ自体がホモトピー論の新しい定式化になっているから。今のところ、HoTTがホモトピー論に対して、新しい発見をもたらすというようなことは起きてない

univalent foundationは、現時点ではあまり目に見える成果が出てないし、ホモトピー論を形式化するといっても、出来てることは少ない。それでも少しは成果があるのは(2)の話なので、以下は主にCoqでホモトピー論をやる話。univalent foundationという壮大な目標と比べると、球面のホモトピー群を計算するとかいうのは、大分重箱の隅をつつく感はあるけど、意外と、そういうところから新しい発見がないとも限らない

前置き(2)CoqやAgdaでホモトピー論が出来る大雑把な理由

ホモトピー論は幾何学の一分野で、教科書を開くと、多分位相空間を使って説明してあるはず(単体的集合やsimplicial setや一般のモデル圏でやってる場合もあるかも)。こういう標準的なやり方を、そのままCoqでやろうと思って、位相を定義して、例えば球面を定義するために、実数を定義してetc.とやってると、物凄く大変そうな気がする。HoTTでは、位相とか連続性のような幾何学にありがちな概念は一切使わず、全然違う方法で、ホモトピー論をやる

基本的な発見は、空間も型もweak ∞-groupoidと呼ばれる構造が入ることにある(数学的に厳密なことをやりたいわけでないので、以下位相空間とか言わず、単に空間と呼ぶ。普通に平面とか球面とか直線とか円周とかをイメージすればいい。また、ここでの型というのも、CoqやAgdaの型で、HaskellとかOCamlの型は指してない)。weak ∞-groupoidはgroupoidを物凄く拡張した概念だけど、ちゃんと定義するのは大変なので、何か同じ構造が入るのだということだけ分かれば十分

幸運なことに(?)、幾何学の方では、空間に対応するweak ∞-groupoidを調べれば、ホモトピー論をやるのに必要な幾何学的情報は、そこに全部含まれていることが分かっている。こうして、weak ∞-groupoidの言葉でホモトピー論を書き直すという仕事が発生するけど、位相空間の言葉で定義されたホモトピー論の概念を、weak ∞-groupoidに移植する仕方は、そんなに明らかでもないので、ホモトピー論の教科書を読んで、HoTTのコードを見ても、あんまり同じことをやっているようには見えないかもしれない

weak ∞-groupoidみたいな難しそうなもん使わなくても、位相空間のような数学科の学部で習う概念で、ホモトピー論が出来るならそれでよくね?というのは、多分正しいし、殆どのホモトピー論の人たちはweak ∞-groupoidとか使わないと思う。ただ、幾何学をformalにやろうとした時、人間の直感をそのまま定式化したような位相とか連続性の概念から始めると、めんどくさいことになる一方、weak ∞-groupoidはformalに扱うのには都合がよさそうではある(ユークリッド幾何に対する座標幾何のようなものと思えばいいのかもしれない)。まぁ、それでも、幾何学を形式化して嬉しいのは暇人だけなので、そういう意味では、やっぱり凄いメリットがあるとは言えないのが現状かもしれない

とにかく、そういうわけで、型もweak ∞-groupoidなので、型に対してホモトピー論をやることができるし(できるかどうかと意味があるかどうかは別であるけど)、空間のweak ∞-groupoidと型のweak ∞-groupoidが同じになるようなことがあれば、型のホモトピー論をやることと幾何学的なホモトピー論をやることは同じになるはずである

空間がgroupoidになることの適当な説明

空間にgroupoid構造を入れる簡単な方法は、「空間の点を対象として、点xから点yへの(連続な)曲線を射とするような圏」を考えればいい("曲線"というけど、別に曲がってなくて、直線でもいいし、定点でもいいので、経路とかいう方が適切な日本語の気もする。英語ではpath)。以下のことはすぐ分かるので、これはgroupoidになる
・点xから点xへの自明な"曲線"があり、これは恒等射に対応する
・点xから点yへの曲線を逆にたどれば、点yから点xへの曲線がある。これは射のinverseに相当する
・射の合成を、曲線を繋ぐことで定義すれば、これは結合的になる

このgroupoidは単純であるけれども、射の集まりがでかすぎるので、これを(射の合成や逆とcompatibleな)同値関係で割ったgroupoidを考える。この同値関係は、直感的には、曲線が互いに空間内の連続的な変形で移りあうという形で定義される。そうやって定義されるものをfundamental groupoidと呼ぶ(厳密な定義を書くのは簡単だけども、これがメインの話でないので省略する)

2つの曲線が互いに空間内の連続的な変形で移りあわない例を直感的に説明する。空間としては、原点に穴があいた平面を考える。説明のために、直交座標が入っていて、P=(-1,0),Q=(1,0)として、PとQを繋ぐ曲線を考える。P,Qは円周x^2+y^2=1の上に乗っていて、PからQへの曲線として、この円周の上側(上半平面側)と下側を通って行く2つの曲線L,Mがある。LとMの逆の合成は、Pから円周を通って一周してPに戻ってくる曲線なので、LとMが同値とすると、これは点Pから点Pへの自明な曲線と同値でないといけない。なので、円x^2+y^2=1が、点Pから動かない曲線へ連続変形できないといけない。後者の曲線は小さいので、前者の曲線を縮小していこうとすると、原点に穴があいてるので、これが邪魔になって、連続的に曲線を一点に潰すことはできない。なので、円周を一周してPに戻ってくる曲線は、恒等射ではないし、元々考えたLとMは同値ではない

型がgroupoidになることの説明

型Aに、groupoid構造を入れるには「型Aの値全体を対象として、x,y:Aに対して、x=yの証明全体をxからyへの射とするような圏」を考えればいい。恒等射、射の合成、射のinverseを以下で定義する
・x:Aに対して、x=xは反射律で証明でき、これを恒等射とする
・x,y:Aに対して、x=yの証明から対称律によって、y=xの証明を得ることができる。これを射のinverseとする
・x,y,z:Aに対して、x=yの証明とy=zの証明から、推移律によって、x=zの証明を得る。これを射の合成とする

この定義からは、射の合成が結合的であることとか、そういう圏の公理を満たすかどうか、すぐには分からない。そもそも、普通の数学では、証明が等しいかどうか考えることは意味がないので、例えば、2つの反射律を推移律で合成したものが反射律かどうかというのは、数学では出てこない問題意識。CoqやAgdaでは、証明が等しいかどうかを考えることは意味を持つ。意味を持つだけでなく、上の定義で、ちゃんと型がgroupoidになることを証明することができる。初見だと、これは結構衝撃的なことだと思う

というわけで、その証明をCoqで書いてみる。Coqにはデフォルトで、eqが定義されている(Print eq.とかで見れる)けど、少し使いづらいので、自分で新しく定義しなおすことにする

(*
Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
*)
Inductive Id {A:Type} : A->A->Type := id_refl : forall (t:A),Id t t.
Notation "x == y" := (Id x y) (at level 70).

という感じ。eqの定義と殆ど同じだけど、eqでPropになってるところをTypeにしている

この定義には、反射律は含まれている(id_refl)けど、対称律と推移律は含まれてないので、それらを定義する必要がある

Definition concat {A} {x y z:A} : (x==y) -> (y==z) -> (x==z).
  intros p q.
  induction p.
  exact q.
Defined.

Definition inverse {A} {x y:A} : (x==y) -> (y==x).
  intros p.
  induction p.
  apply id_refl.
Defined.

Notation "p @ q" := (concat p q) (at level 60).
Notation "! p" := (inverse p) (at level 50).

名前は、射の合成と逆であることを踏まえて、concatとinverseにしてある(eq型では、eq_transとeq_sym)。concatは標準的な射の合成の記法 $q \circ p$ とp,qの順番が反転しているので注意

以上で定義ができたので、必要な性質を満たすことを示していけばいい。例えば、射の合成則は

Definition assoc {A} {x y z w:A} (p:x==y) (q:y==z) (r:z==w) : (p @ q) @ r == p @ (q @ r).
  induction p;induction q;induction r.
  apply id_refl.
Defined.

という形で簡単に証明できる。他の公理は以下の通り(証明はinductionするだけなので省略する)

Definition id_left_unit {A} {x y:A} (p:x==y) : (id_refl x) @ p == p.

Definition id_right_unit {A} {x y:A} (p:x==y) : p @ (id_refl y) == p.

Definition id_right_inverse {A} {x y:A} (p:x==y) : (p @ !p) == (id_refl x).

Definition id_left_inverse {A} {x y:A} (p:x==y) : (!p @ p) == (id_refl y).

以上で、型がgroupoidになることが分かった

型がweak ∞-groupoidになるということの適当な説明

圏論では、対象が等しいかどうかではなく、同型かどうかを議論するのがオーソドックスなやり方。そういうことをするのは、例えば、n次元ベクトル空間を作るやり方は、無数にあるけど、それらは、一般に集合として等しくなくて、同型にしかならないというシチュエーションが数学では空気のように存在するから。例えば、公理的集合論では、集合の等しさは、外延性の公理で決まって、多項式環K[x,y]の{x,y}で生成される2次元ベクトル空間と{x^2,y^2}で生成される2次元ベクトル空間は等しくない。基本的に、普通の数学では、集合が等しいかどうかという議論は意味がないことが多くて、同型かどうかを問題にする

まぁ、そういうわけなのだけど、射が等しいかどうかは、普通に議論される。例えば、射の結合律は
$f \circ (g \circ h) = (f \circ g) \circ h$
とか書いてある。それで、射が等しいかどうかの議論をやめて、同型かどうかだけを議論しようというのが、2-圏の発想。つまり、射の間の射(2-射と呼ぶ)
$\alpha_{f,g,h} : f \circ (g \circ h) \to (f \circ g) \circ h$
があって、こういうものがデタラメにあっても、何もできないので、よさげな公理を満たすことを要請する。どんな公理を要請すればいいかは自明でないけども、ちょっと、それは置いておいて、同型なのだから、最低限可逆であることを要請したい。可逆であるという条件を素直に書くと
$\alpha_{f,g,h}^{-1} \circ \alpha_{f,g,h} = id_{f \circ (g \circ h)}$
$\alpha_{f,g,h} \circ \alpha_{f,g,h}^{-1} = id_{(f \circ g) \circ h}$
となる(2-射の合成と1-射の合成で同じ記号を使ってるけど、気にしない)。ここでは、射が等しいかどうかの議論をやめたのに、2-射が等しいかどうかの議論をしてしまっている。従って、2-射が等しいかどうかの議論もやめようというという発想は自然に出てくる。それで、3-圏に行きつくと、やっぱり、3-射が等しいかどうかを議論する羽目になって、こうして、n-圏が現れて、全てのn-射が等しいかどうか議論する必要がなくなる極限として、∞-圏が出てくる(n-圏には、weak n-圏とstrict n-圏があるけど、ここではweak n-圏しか扱わない)

射が等しいかどうかの議論をやめたら何か嬉しいのかというと、今のところ、特に嬉しいことはない。なので、日常的に圏を使っている数学者でも、2-圏や3-圏を使う人は少ない。あと、2-圏や3-圏の定義は分かってるけど、一般のn-圏の定義を書くことは現在誰も出来てない

type theoryに話を戻すと、「普通の数学では、等しいかどうかは議論するけども、等しいことの証明の等しさは議論しない」というのは、言葉遊びとしては、「普通の圏論では、対象が同型かどうか議論するけども、射が同型かどうかは議論しない」というのと似てる。CoqやAgdaでは、証明が等しいかどうか議論できるだけでなく、"証明が等しいことの証明の等しさ"も議論できる。そうすると、上の2-圏の $\alpha_{f,g,h}$ に対応するのは、assocそのものと思うことができる。assocが可逆であるかどうか考えてみると、これは、素朴に以下のように書ける

Definition assoc_is_right_reversible  {A} {x y z w:A} (p:x==y) (q:y==z) (r:z==w) :
   (assoc p q r) @ !(assoc p q r) == id_refl ((p @ q) @ r).
Proof.
   exact (id_right_inverse _).
Defined.

Definition assoc_is_left_reversibel {A} {x y z w:A} (p:x==y) (q:y==z) (r:z==w) :
   !(assoc p q r) @ (assoc p q r) == id_refl (p @ (q @ r)).
Proof.
   exact (id_left_inverse _).
Defined.

証明は、型がgroupoidになることを証明した時出てきたid_right_inverseとid_left_inverseそのものに過ぎない

2-圏の公理で満たすべきものは他にも色々あるけど、全部列挙しても、だるいだけなので、唐突に、一番重要なK_4 cohenrence条件を書く。これは、大体、2-射に於ける、assocのような役割を果たすものと言える

Definition concat2 {A} {x y z:A} {p q:x==y} {r s:y==z} : p==q -> r==s -> p @ r == q @ s.
  intros f g.
  induction f ;induction g.
  apply id_refl.
Defined.

Notation "p [@] q" := (concat2 p q) (at level 61).

Definition K4 {A} {x y z w u:A} (a:x==y) (b:y==z) (c:z==w) (d:w==u) :
   ((assoc a b c) [@] (id_refl d)) @ (assoc a (b @ c) d) @ ((id_refl a) [@] (assoc b c d)) ==
      (assoc (a @ b) c d) @ (assoc a b (c @ d)).
Proof.
  induction a;induction b;induction c;induction d.
  apply id_refl.
Defined.

この条件は、モノイダル圏の(associatorが満たす)pentagon axiomと同じ形なのが、Wikipediaの図式を眺めてると分かる(モノイダル圏は、2-圏の特殊な場合なので、同じものが出てくる)
http://en.wikipedia.org/wiki/Monoidal_category#Formal_definition

K4条件には、次のような類似物もある。mを代数の非結合的な掛け算で線形であるとすると、
A(x,y,z) = m(x,m(y,z)) - m(m(x,y),z)
のように置くと、
A(x,y,m(z,w)) + A(m(x,y),z,w) =
m(x,m(y,m(z,w)) - m(m(x,y) , m(z,w)) + m(m(x,y) , m(z,w)) - m(m(m(x,y),z),w) =
m(x,m(y,m(z,w)) - m(m(m(x,y),z),w)

m(x,A(y,z,w)) + A(x, m(y,z), w) + m(A(x,y,z),w) =
m(x,m(y,m(z,w)) - m(x,m(m(y,z),w)) + m(x,m(m(y,z),w)) - m(m(x,m(y,z)),w) + m(m(x,m(y,z)),w) - m(m(m(x,y),z),w) =
m(x,m(y,m(z,w)) - m(m(m(x,y),z),w)
なので、
m(x,A(y,z,w)) + A(x, m(y,z), w) + m(A(x,y,z),w) = A(x,y,m(z,w)) + A(m(x,y),z,w)
となる。じっと眺めると、この式は、K4 coherence条件と同じ形をしていることが分かる。

まぁ、とにかく、2-groupoidになるというのは、こういう条件を沢山満たすということ。同様にして、型が3-groupoid,4-groupoid, ... ,weak ∞-groupoidになることも証明していけるはずだけど、weak ∞-groupoidに対しては、無限個の条件が存在するはずで、全てのcoherence条件を、きちんと書き下して、証明するようなことは誰もできてない。そういう証明を作ることは理想であるけども、Voevodskyは、それを回避して全然違う方法で、型がweak ∞-groupoidになることを証明してしまった。ただ、多分それは、CoqやAgdaに載せるには結構つらいのじゃないかと思う

別に、これらの話は、HoTTとか言わなくても、CoqやAgdaで成立している話だし、ホモトピーって何?とか、どのへんがホモトピー論?って思わなければ、数学を知らないCoq/Agda使いでも理解できるはず。空間が、weak ∞-groupoidになることは簡単に説明できる気がしないので略。