Formalization of Setoids-enriched category theory

最近書いてるCoqの話。

主にこれの解説をします:
Yoneda.v · GitHub

Setoidをベースにすることについて

多分圏論formalize業界(狭そう)では有名な話。
Coqの場合はSetoidのequalityに対してもrewrite tacticが使えるのでそれでやる。

Proper

Setoid morphismをここではMapoidとよぶ.
Mapoidは写像(underlying set間の写像)でsetoidのequalityを保つもの.

Structure Mapoid (S S' : Setoid) :=
  {
    mapping :> S → S';
    is_mapoid :> Proper (equality ==> equality) mapping;
  }.
Existing Instance is_mapoid.

ここでのProper (equality ==> equality) mappingがそれで、
意味としてはmappingなるfunctionによってequality relationがequality relationに写ることを表す(==>はrelationのimplication).

Proper (R ==> R') fの元で、rewrite : a R b ~> f a R' f bなる書き換えができるようになる*1のでここではExisting InstanceによってこのPropernessをトップレベルに展開している。

Proper Instance

さて上のようにProperについてのinstanceを使わないとrewriteはできないので、例えばa == bからP a == P bとするにはPがProperであることを証明する必要がある。

上のコードでは、新たに定義したS ** S'(setoidの直積)のconstructing function Spair : S -> S' -> S ** S'がProperであることなどは自力で証明を書いて補っている。

rewriteが効いて欲しい場所で効かない場合はProperのinstanceをかこう。

Category, Functor, Natの定義

圏の定義その他については

github.com

などが参考になる。

ただしCat_on_Coqでは平易に書き下しているようなPropernessも、上のコードでは「おおもとの定義」では全てSetoid上で作るようにしてある。

つまり、例えばcategoryの定義は

Structure Category :=
  {
    object :> Type;
    morphism : object → object → Setoid;
    identity : forall {x}, carrier (morphism x x);
    compose : forall {a b c}, morphism b c ** morphism a b -⇒ morphism a c;
    is_category :> Is_Category (@identity) (@compose);
  }.

となっていて、composeは2つのSetoidの直積からSetoidへのmapoidになるように定義してある。

あるいはfunctorのarrow partも同じようにfmorphism : forall {a b}, @morphism fdom a b -⇒ @morphism fcod (fobj a) (fobj b);などと、hom-setoidの間のmapoidであることを要請している。

こうするとcategoryやfunctorの定義の中に「〜のproperness」のような条件がいちいち現れてこないので、「表面上は」通常の圏論でfunctionとされている場所をmapoidに置き換えるだけでいい。

あるいは、ここではすべてSetoids-enriched category theoryをやっていると思えばいいので理論的にはすっきりする。

ただしcategoryのinstanceを与える際にいちいちmapoidで定義するのは面倒なので(データを定めてからmapoidであることを証明する、という順番で行きたい)、上のコードではsetoidベースでない(条件ベタ書きの)categoryも定義しておいて相互変換できるようにしている。

このやり方だとコードが多少長くなるのでこれが嫌な場合はCat_on_Coq方式でいいと思う。

Equational Reasoning

Agdaに毒された自分のような人間はequational reasoningがないと死んでしまうのでNotationで用意した。

参考:

gist.github.com

使用例:

Notation "`begin p" := p (at level 20, right associativity).
Notation "a =⟨ p 'at' C ⟩ pr" := (@Equivalence_Transitive (@morphism C _ _) _ _ a _ _ p pr) (at level 30, right associativity).
Notation "a =⟨ p ⟩ pr" := (@Equivalence_Transitive _ _ _ a _ _ p pr) (at level 30, right associativity).
Notation "a ↓⟨ p ⟩ pr" := (a =⟨ p ⟩ pr) (at level 30, right associativity).
Notation "a ↑⟨ p ⟩ pr" := (@Equivalence_Transitive _ _ _ a _ _ (@Equivalence_Symmetric p) pr) (at level 30, right associativity).
Notation "a `end" := (@Equivalence_Reflexive _ _ _ a) (at level 30).


(* 例 *)

...
exact (`begin
      fmap H f ∘ (β a ∘ α a)
     =⟨ ltac: (rewrite <- assoc_of; reflexivity) ⟩
      (fmap H f ∘ β a) ∘ α a
     =⟨ ltac: (rewrite (naturality_of β); reflexivity) ⟩
      (β b ∘ fmap G f) ∘ α a
     =⟨ ltac: (rewrite assoc_of; reflexivity) ⟩
      β b ∘ (fmap G f ∘ α a)
     =⟨ ltac: (rewrite (naturality_of α); reflexivity) ⟩
      β b ∘ (α b ∘ fmap F f)
     =⟨ ltac: (rewrite <- assoc_of; reflexivity) ⟩
      (β b ∘ α b) ∘ fmap F f
     `end).

ちなみにltac: (...)と書くとLtacで作った項をCICの項に変換できるので、
reasoning中ではtacticとproof termを混ぜて使うことができる。

意外と便利。

これを使って思ったこととしては、やっぱりAgdaのようなhole推論機能がないと若干苦しい(エラーメッセージからどの部分までreasoningが上手く行っているかを推測する必要がある; ただし慣れればできるようになるため問題ないとも言える)。

しかし読みやすい証明のためには致し方ない。