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

その2。

ホモトピー群とEckmann-Hilton argument

型がweak ∞-groupoidだということが分かったので、weak ∞-groupoidに対して、ホモトピー群というものを定義する。type theory的には、ホモトピー群を定義する動機はあまりないけど、数学にinspireされて、(意味があるかどうかは分からないけど)こういうものを定義してみて、後で、natのような具体的な型に対して、ホモトピー群を計算しようという試み

普通のgroupoid Xに対して、Hom(x,x)は群になる(xはXの適当なobject)。fundamental groupoidを思い出すと、これは、空間上の点xから点xへの適当な曲線の適当な同値類の集合と見なせる。例えば、円周の場合、適当な点Oを固定すると、fundamental groupoidは、点Oから点Oへ右回り(左回り)にn周する(nは自然数)ような曲線の全体と同一視できる。右回りにn周するような曲線と、右回りにm周するような曲線をつなぐと、右回りに(n+m)周するような曲線になるので、円周の場合、整数の集合が加法に関してなす群と同型な群が得られる。こういう群を、基本群と呼んで、π_1(X,x)とか書く(xは基点という)。π_1という記号から連想する通り、π_2とかπ_3とかetc.もあるけど、それはgroupoidに対しては定義できない

weak ∞-groupoidの場合、Hom(x,x)の要素同士が等しいかどうかは定義されてないけど、同型なものを等しいと見なすことによって、やはり群が得られる。これを以下のように書く
$\pi_1(X,x) = Hom_X(x,x)/\sim$
更に
$\pi_2(X,x) = Hom_{Hom_X(x,x)}(id_x , id_x)/\sim$
と定義して、これを二次のホモトピー群と呼ぶ(この場合も、同型なものを等しいと見なすことによって群となる)。すぐ分かる通り
$\pi_2(X,x) = \pi_1(Hom_X(x,x) , id_x)$
となる。三次のホモトピー群は
$\pi_3(X,x) = \pi_2(Hom_X(x,x) , id_x)$
とかで、以下同様にn次のホモトピー群が定義される。

ホモトピー論の教科書を見ると
$\pi_n(X,b) = [(S^n,a) , (X,b)]$
みたいな定義が書いてある気がする。これはn次元球面からXへの(点aを点bに移すような)連続写像の適当な同値類の集合だけど、weak ∞-groupoidの方は、球面とか出てこないので、二つの定義が同値かどうかは自明ではない(n=1の時は、点bから点bへの連続な曲線というのは、点bを通るような円周からの連続写像と同じというのは何となく分かると思う)。けど、深く気にせず、weak ∞-groupoidに対しては、上のようにホモトピー群が定義されると考えておく

type theoryでは、以前から、Uniqueness of Identity Proofs(UIP)というものが議論されていた。Coqで書くと、以下の性質

(* Uniqueness of Identity Proofs *)
Axiom UIP : forall {U:Type} (x y:U) (p1 p2:x == y), p1 == p2.

(* Uniqueness of Reflexive Identity Proofs *)
Axiom UIP_refl : forall {U:Type} (x:U) (p:x == x), p == id_refl x.

これらの性質は、Coqでは(何か公理を追加しない限り)証明できないことが知られている。この2つの命題は同値であるけれども、特にUIP_reflが言っているのは、「任意の型Uに対して、x:Uを基点とする基本群が自明な群になる」と読める。明らかにUIPを仮定すると、全てのホモトピー群は自明となる。Agdaでは、いつの頃からか、特にオプションなしで起動すると、UIPと同値な命題を仮定するようになってしまって、そのままだと全てのホモトピー群が自明になってしまうので、AgdaでHoTTをやる時には注意がいる

weak ∞-groupoidのホモトピー群と、空間のホモトピー群が同じであることは(type theoryにとって重要でないので)説明しないけど、同じ性質は共有されているべきで、その性質をweak ∞-groupoidの言葉で証明できるか考えることはtype theory的にも意味があるかもしれない。ホモトピー論に於ける基本的な結果として、二次以上のホモトピー群が可換になるということが知られている。この性質を、weak ∞-groupoidの言葉のみで、Coqで証明できるかどうか考えてみる。二次のホモトピー群が可換になることを言えば十分なので証明すべき命題はCoqで書くと

Definition comm {A} {x:A} (a b:(id_refl x)==(id_refl x)): a @ b == b @ a.

となる。この証明は、何も知らず、自分で思いつくのは、かなり難しいと思う。キーとなるのは、(id_refl x)==(id_refl x)には、積の定義の仕方が2種類あって(実際にはこの2つの定義は一致する)、interchange ruleという性質を満たすことを示すことで証明される。これは、Eckmann-Hilton argumentとして数学では知られている議論。2種類の演算というのは、2-圏の言葉で、垂直合成と水平合成と呼ばれるものに相当する。

Coqで書いてしまうと

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 interchange {A} {x y z:A} {p q r:x==y} {s t u:y==z} (a:p==q) (b:q==r) (c:s==t) (d:t==u) :
  (a @ b) [@] (c @ d) == (a [@] c) @ (b [@] d).
Proof.
   induction a;induction b;induction c;induction d.
   apply id_refl.
Defined.

という感じで、もしconcat2が、e=(id_refl (id_refl x))について、unitalであれば(つまり、e [@] x==xかつ x [@] e==x)、
a @ b ==
(e [@] a) @ (b [@] e) ==
(e @ b) [@] (a @ e) ==
b [@] a ==
(b @ e) [@] (e @ a) ==
(b [@] e) @ (e [@] a) ==
b@a
という変形によって、可換性が証明できる(式変形の途中で、b[@]a == b@aを含んでいて、2つの演算が一致することも分かる)。難しくはないけど、trickyではあると思う。

e [@] x==xやx [@] e==xは直接的に示すことはできなくて

Definition concat2_is_left_unital {A} {x y:A} {p q:x==y} (s:p==q) :
  (id_refl (id_refl x)) [@] s == (id_left_unit p) @ s @ !(id_left_unit q).
Proof.
  induction s.
  induction t.
  apply id_refl.
Defined.

Definition concat2_is_right_unital {A} {x y:A} {p q:x==y} (s:p==q) :
  s [@] (id_refl (id_refl y)) == (id_right_unit p) @ s @ !(id_right_unit q).
Proof.
  induction s.
  induction t.
  apply id_refl.
Defined.


Definition concat2_is_left_unital_pt {A} {x:A} (s:(id_refl x)==(id_refl x)) :
   (id_refl (id_refl x)) [@] s == s.
Proof.
   exact( (concat2_is_left_unital s) @ (id_right_unit (_@s)) ).
Defined.


Definition concat2_is_right_unital_pt {A} {x:A} (s:(id_refl x)==(id_refl x)) :
   s [@] (id_refl (id_refl x)) == s.
Proof.
   exact( (concat2_is_right_unital s) @ (id_right_unit s) ).
Defined.

というように、基点を"分裂"させて、inductionを使える形で、一般的な定理を示した後、基点を一致させる

あとは

Definition comm {A} {x:A} (a b:(id_refl x)==(id_refl x)): a @ b == b @ a.
  set (e:=id_refl (id_refl x)).
  assert(p1 := ((concat2_is_left_unital_pt a) [@] (concat2_is_right_unital_pt b))).
  assert(p2 := interchange e b a e).
  assert(p3 := (!id_left_unit b) [[@]] (!id_right_unit a)).
  assert(p4 := (!id_right_unit b) [[@]] (!id_left_unit a)).
  assert(p5 := interchange b e e a).
  assert(p6 := ((concat2_is_right_unital_pt b) [@] (concat2_is_left_unital_pt a))).
  exact ( ((!p1) @ (!(p3 @ p2))) @ ((p4 @ p5) @ p6) ).
Defined.

とかで証明できる

inductive typeのホモトピー群の計算

natやlist Xのような具体的な型に対して、ホモトピー群を計算する。結論としては、これらの型に対するホモトピー群は全て自明となってしまう。このことは、HoTT以前に、Hedbergの定理というものを使って証明されていた(その目的は、特定の型に対して、UIP性が成立することを証明すること)。

とりあえず
A direct proof of Hedberg’s theorem
http://homotopytypetheory.org/2012/03/30/a-direct-proof-of-hedbergs-theorem/
の証明を、そのまま持ってくると、Hedbergの定理は以下の通り

(* "local" Proof irrelevance *)
Definition isprop (A:Type) : Type := forall (t1 t2:A),t1==t2.

(* "local" Uniqueness of Identity Proofs(UIP) *)
Definition isset (A:Type) := forall (x y:A),isprop (x==y).

(* decidablity *)
Definition isdec (A:Type) := forall (x0 x1:A),(x0==x1) + (x0==x1 -> False).

Theorem hedberg (A:Type) : isdec(A) -> isset(A).
Proof.
   intros isdecA x y p q.
   assert ( 
    lemma :
      forall (proof:x == y),match (isdecA x x) , (isdecA x y) with
         | inl r , inl s => proof == (!r @ s)
         | _ , _ => False
      end
   ).
      induction proof.
      destruct (isdecA t t) as [pr|f].
      exact (!id_left_inverse pr).
      exact (f (id_refl t)).
  destruct (isdecA x x) as [H1|H2].
  destruct (isdecA x y) as [H3|H4].
  exact ((lemma p) @ (!lemma q)).
  contradiction.
  contradiction.
Defined.

isdecというのは、decidabilityという性質で、任意のxとyが等しいか等しくないか、どっちかは証明できるということを意味している。

ispropとかissetは、Voevodskyは、n次以上のホモトピー群が自明になるような型を、homotopy level(h-level)が(n+1)の型と呼んでいて、一次以上のホモトピー群が全部自明となる型をh-Setと呼んだりしている。定義しなかったけど、数学ではπ_0というのもあって、これは空間の連結成分の集合に相当するものだけど、これも自明になる場合をh-Propと呼んでいる。h-Propはh-levelが1で、h-Setはh-levelが2となる。h-Setの定義は、一見基本群が自明になることしか主張してないように見えるけど、実際には、全てのホモトピー群が消えることが証明できる。

Definition iscontr (T:Type) :Type := {c:T & forall t:T,t==c}.
Definition isprop' (T:Type) : Type := forall (t1 t2:T),iscontr (t1==t2).

Lemma contr_is_prop': forall A,iscontr(A)->isprop'(A).
  intros  A H x y.
  destruct H as [c H].
  exists ((H x)@(!H y)).
  intro t;induction t.
  exact (!id_right_inverse _).
Qed.

Lemma contr_is_prop : forall U,iscontr(U)->isprop(U).
  assert(H:forall U , isprop'(U) -> isprop(U)).
    intros U X x y.
    destruct (X x y) as [c _].
    exact c.
  intro U.
  assert(H0:=H U).
  assert(H1:=contr_is_prop' U).
  firstorder.
Qed.

Lemma prop_add_prime : forall U,isprop(U) -> isprop'(U).
  intros U H.
  assert(H0:isdec(U)).
     unfold isdec;intros x y;left;exact (H x y).
  assert(H1:=hedberg _ H0).
  intros x y.
  assert(p:=H x y).
  induction p.
  exists (id_refl t).
  intro p;exact (H1 t t p (id_refl t)).
Qed.


Lemma prop_is_set : forall U,isprop(U) -> isset(U).
  intro U.
  assert(H0:= prop_add_prime U).
  assert(H1:isprop'(U)->isset(U)).
     intros H x y.
     exact (contr_is_prop (x==y) (H x y)).
  firstorder.
Qed.

(* h-Setは二次のホモトピー群も自明 *)
Lemma hset_is_htrivial : forall U,isset(U) -> (forall (x:U) ,isset (x==x)).
   intros U H x.
   exact (prop_is_set (x==x) (H x x)).
Qed.

h-Propやh-Setは、階層性があるという類似点を除けば、CoqのPropやSetとは直接の関係はないと思う。また、一般的に、n次以上のホモトピー群が自明になるようなweak ∞-goroupoidをweak (n-1)-groupoidと呼んで、対応関係としては
n次以上のホモトピー群が自明 <=> weak (n-1)-groupoid <=> h-level (n+1)
となる。h-Propは形式的にweak (-1)-groupoidで、iscontrが成立する型は、weak (-2)-groupoidとなる

Hedbergの定理を使って、nat型のホモトピー群が自明であることを証明して見る。通常のeqに対して、natがdecidableであることは、eq_nat_decとして証明されているので、同じことをやって、Hedbergの定理を適用すればいい

Definition pred (n:nat) : nat :=
   match n with
     | O => 0
     | S u => u
   end.


Lemma nat_is_hset: isset(nat).
   assert(P0:forall {A B} (x y:A) (f:A->B) , x==y -> f x==f y).
      intros A B x y f p;induction p;apply id_refl.
   assert(P1:forall n:nat, n == pred (S n)).
      simpl;apply id_refl.
   assert(P:forall (n m:nat),S n==S m->n==m).
      intros n m H.
      exact ( (P1 n)@(P0 nat nat (S n) (S m) pred H)@(!P1 m) ).
  apply hedberg.
  unfold isdec;intro n;induction n.
    intro m;induction m.
       left;exact (id_refl 0).
       right;intro H;inversion H.
    intro m;induction m.
       right;intro H;inversion H.
       destruct (IHn m) as [HL | HR].
          left;induction HL;apply id_refl.
          right;intro H;exact (HR (P n m H)).
Qed.

listに対しても、同様に証明できる。この時、predと同じ働きをする関数として、head関数やtail関数を作ることが必要になる。他のinductive typeについても事情は同様であることが推測できて、inductive typeのみでは、ホモトピー群が自明にならないような型を作るのは難しそうだと分かる("全てのinductive typeについて〜"というタイプの性質は、Coqで形式化するのはできるのかどうかすらよく分からないけど)。

Agdaで、デフォルトでは、UIPが証明できてしまうようになったのは、こういう事情を踏まえて、どうせUIPが成立しない型を作れないんだからいいんじゃね？という気持ちがあったのかもしれない。一方、HoTTの人は、それではツマラナイので、ホモトピー群が自明にならないような型を作れる機構を考えようという方向に進んだのでした。

余談:braided monoidal categoryとしての二次ホモトピー群

上で作ったcommは、モノイダル圏におけるbraidingの公理を満たすことが証明できる。Coqで書くと、以下のようになる(証明は、かなり大変だと思うし、長いので説明はしない)

Definition hexagonL {A} {x:A} (a b c:(id_refl x)==(id_refl x)) :
  (!assoc a b c)@(comm (a@b) c)@(!assoc c a b)==
    ((id_refl a)[@](comm b c))@(!assoc a c b)@((comm a c)[@](id_refl b)).

Definition hexagonR {A} {x:A} (a b c:(id_refl x)==(id_refl x)) :
  (assoc a b c) @ (comm a (b@c)) @ (assoc b c a) ==
     ((comm a b) [@] (id_refl c)) @ (assoc b a c) @ ((id_refl b) [@] (comm a c)).

Definition YBE {A} {x:A} (a b c:(id_refl x)==(id_refl x)) :
  ((comm a b)[@](id_refl c)) @ (assoc b a c) @
  ((id_refl b)[@](comm a c)) @ (!assoc b c a) @
  ((comm b c)[@](id_refl a)) @ (assoc c b a) ==
  (assoc a b c) @ ((id_refl a)[@](comm b c)) @
  (!assoc a c b) @ ((comm a c)[@](id_refl b)) @
  (assoc c a b) @ ((id_refl c)[@](comm a b)).

hexagonLとhexagonRを、じっと眺めると
Braided_monoidal_category#The_hexagon_axiom
http://en.wikipedia.org/wiki/Braided_monoidal_category#The_hexagon_axiom
にあるhexagon axiomと同じ形をしているのが分かる。YBEは、Yang-Baxter方程式と呼ばれるもので、hexagon axiomから簡単に導くことができる

モノイダル圏のことを多少知ってると、commがsymmetricであること

Definition symm {A} {x:A} (a b:(id_refl x)==(id_refl x)) : (comm a b)@(comm b a) == (id_refl (a@b)).

が成立すると期待するかもしれないけど、多分これは成り立たない(万が一証明できてしまった人は、教えてください!)。但し、Coqでは、これを否定することもできない(UIPを仮定すれば、この性質は成り立ってしまうので)

$Hom_{Hom_X(x,x)}(id_x , id_x)$ は、射の合成をモノイダル積とすることで、モノイダル圏(正確には、モノイダル∞-圏)になるだけでなく、逆射の存在からrigidでもある(双対が存在する)。そうすると、例えば、traceが定義できる(これは線形代数のtraceの圏論的な一般化)

Definition inv_sq {A} {x y:A} (p:x==y) : !(!p)==p.
   induction p;apply id_refl.
Defined.

Definition trace {A} {x:A} {a:id_refl x==id_refl x} (f:a==a) :=
  (!id_right_inverse a) @ (f [@] (id_refl (!a))) @
  ((!inv_sq a)[@](id_refl (!a))) @ (id_left_inverse (!a)).

型を見ると、
$trace:\pi_2(A,x) \to \pi_3(A,x)$
となっている(categoricalなtraceの定義は、left traceとright traceがあって、今の場合、この2つは一致すると思うのだけど、証明は出来てない)。特に

W a b = trace ((comm a b)@(comm b a))

は、
$W : \pi_2(A,x) \times \pi_2(A,x) \to \pi_3(A,x)$
を与えるけど、これはホモトピー論でWhitehead積として知られるものの、weak ∞-groupoidによる実現(だと思う)。