Coqで圏論
CLTT読書会で最近話題になるネタ。
ConCaT
http://coq.inria.fr/pylons/contribs/view/ConCaT/v8.3
というライブラリがあるんで、これをベースにCLTTの証明なんかを書いていけば、色々よいんじゃないか的な。
ドキュメントらしいものはないけど、論文を読むと、結構詳しい解説がある。あと、どういう順番でソースを追いかけるべきかが分かる。元になった論文は、
Constructive Category Theory
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.4193
10年以上前の論文。
実は、昔読んだらしい。
http://d.hatena.ne.jp/m-a-o/20070202#p3
基本的に、「集合」としてSetoidというものを使っていくんだけど、それで普通の圏論と同じと考えていいのか、よく分からない。この構成的圏論で証明できることは、普通の圏論でも証明できるということが担保されてれば、それでいいのだけど。
が、まあ、差し当たっては、そんな細かいことは気にしないで先に進む強い心をこの数年で得たのだった。
論文と今では微妙にnotationが変わってたりするので、思い出すのも兼ねて、メモ。
・Chapter2
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.RELATIONS.Relations.html
らへんの話。内容は同値関係の定義。等号関係は同値関係なので、そのために必要になる。
・Chapter3.1/Chapter3.2
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.SETOID.Setoid.html
らへんの話。Setoidの定義。Setoid自体は、型理論の範疇で、集合の代替物を作る常套手段の一つらしい。
http://en.wikipedia.org/wiki/Setoid
例として、自然数のSetoidを定義している。
Inductive Nat : Type := Z : Nat | Suc : Nat -> Nat.
が自然数の型。等号関係の定義は、Haskellでderiving Eqした時のと同じもの。これが同値関係になることは別途証明する必要がある。
Setoidは
Structure > Setoid : Type :=
{Carrier :> Type;
Equal : Relation Carrier;
Prf_equiv :> Equivalence Equal}.という定義になってる。:>とかは、
http://pauillac.inria.fr/cdrom_a_graver/www/coq/doc/node.3.3.8.html#Coercions-and-records
とかに説明されているもので、暗黙のうちにSetoidをCarrierに型変換してくれる感じらしい。このように定義すると、
Coq < Check Equal.
Equal
: forall s : Setoid, Relation sとなるのに対して、
Structure > Setoid : Type :=
{Carrier : Type;
Equal : Relation Carrier;
Prf_equiv : Equivalence Equal}.だと、
Coq < Check Equal.
Equal
: forall s : Setoid, Relation (Carrier s)になる
あとは、Structureの後の>のおかげで、
Definition Set_of_nat : Setoid := Eq_Nat_equiv.
で、Setoidが定義できてしまう。
Definition Set_of_nat := Build_Setoid Nat Eq_Nat Eq_Nat_equiv.
と書いても同じことのはず。こっちの方が分かりやすいと思うけどな
・Chapter3.4
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.SETOID.Map.html
らへん。Setoid間の写像の定義。Mapの定義は普通に。自然数の時と同様、Mapという型を作っただけでは、Setoidにはならないので、適切な等号関係を定義してやる。これは単に「f=g<=>forall x.f(x)=g(x)]という外延性に基づく通常の定義
・Chapter4.1
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.CATEGORY.Category.html
圏の定義。Objectの集まりは、Ob:Typeで、射は、Hom:Ob->Ob->Setoidとして定義される。圏論では、対象が等しいかどうかは問題にしないので、Objectの集まりは、Setoidである必要はない。
・Chapter4.2
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.CATEGORY.Hom_Equality.html
圏論では、対象が等しいかどうかは問題にならない(というか、問題にしてはいけない)けれど、射が等しいかどうかは定義できる必要がある。
Definition Equal_hom (C : Category) (a b : C) (f g : a --> b) := (f =_S g). Lemma Equal_hom_refl :forall (C:Category),forall(a b :C),forall(f : a-->b),Equal_hom C a b f f. Proof. intros;unfold Equal_hom in |- *. apply Refl. Qed.
etc.とかでもよいような気はするけど、ライブラリの作者は、f : a-->bとg : c-->dの比較がしたいらしい。それができて嬉しい状況が分からないけれど。ナイーブには、aとcが等しくて、bとdが等しい時とか書きたいけど、Objectが等しいかどうかの判定はできないので、複雑な定義になってる。まあ、正直この定義でよい理由は、あんまり分からない
このへんまで理解すると、圏論を知ってる人には、あとは割と自動的なので、さくっと。
・Chapter4.3
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.CATEGORY.Dual.html
categoryのdualの話。
・Chapter4.4
http://www.lix.polytechnique.fr/coq/V8.2pl1/contribs/ConCaT.CATEGORY_THEORY.CATEGORY.CONSTRUCTIONS.CatProperty.html
epi/mono/isoの定義。
・Chapter4.5
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.CATEGORY.SET.html
Setoidの圏を定義する。ライブラリには、Setoidを使った群やモノイドの定義があるので、それを利用して、群の圏やモノイドの圏も定義することができるはず
・Chapter5.1
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.FUNCTOR.Functor.html
関手の定義。
・Chapter5.2
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.FUNCTOR.HomFunctor.html
Hom Functorの定義。
・Chapter5.3
http://coq.inria.fr/distrib/8.2/contribs/ConCaT.CATEGORY_THEORY.FUNCTOR.CAT.html
あたり。圏の圏。2-category的なもの
・Chapter5.4
ただのExcercise
・Chapter6.1
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.NT.Ntransformation.html
自然変換
・Chapter6.2
自然変換の例。
・Chapter6.3
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.FUNCTOR.CAT.html
関手圏。そろそろ「モナドは単なる自己関手の圏におけるモノイド対象だよ。何か問題でも？」とか、どや顔で語るべきところ
・Chapter7
謎
・Chapter8
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.NT.YONEDA_LEMMA.YonedaEmbedding.html
米田の補題
・Chapter9
論文には、極限や随伴の定義はなかったけど、ちゃんとできるよ！という話が書いてある。今は、ライブラリにも含まれている。
極限
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.LIMITS.Limit.html
余極限
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.LIMITS.CoLimit.html
随伴
http://coq.inria.fr/pylons/contribs/files/ConCaT/v8.3/ConCaT.CATEGORY_THEORY.ADJUNCTION.Adjunction.html
とりあえず、CLTTを形式化するのに、必要なものは一通り揃っていそう(少なくとも、一章に関する限り)。とりあえず、練習として、
・モノイドの圏を定義する
・モナドを定義して、Setoidの圏上でList functorを定義して、こいつがList Monadになることを言う
とかやってみようかと思う
別に難しいことはないはず(続く
