functor, あるいはarrow equalityについて

Category TheoryのFormalizationがらみの話。

Category TheoryのFormalizationをするときは、基本的にSetoid-enrichedでやるのが筋がよいということはこの業界(？)では有名な話だし、少し前のブログ記事にも書いたのでそのことを前提として次のようなことを考える。

functorの(strong)equalityは、「object partが等しい」上で「arrow partも等しい」ということで定める。
ところで、この2つのequalityは同じレベルの話ではない。

F == Gをforall A, F A == G Aかつforall f, F f == G fとはできなくて、なぜなら後者は左辺と右辺で型が違う(F a -> F bとG a -> G bはunifyできない)ので、この定義は上手くいかない。
さてどうするかというと、少なくとも今のところは3つの定義を考えている。

F == G := Sigma (eq: forall A, F A == G A) (forall f, extend [F f] with eq == G f)のように、dependent sum typeを使ってequalityを書き換える方法
新たに圏にheterogeneous equality~を定め(定義： ~ : forall a b, hom(a,b) -> hom(c,d) -> Propであって、各homへの制限~ : relation on hom(a,b)はそこでのhomに入っている同値関係に等しい)、F == G := forall f, F f ~ G fとする方法
F == G := exist (k: Nat F G), k a ~ identityとする方法

最初の方法は自明につらい。
少なくとも茨の道であることが明らかなときわざわざそこへ分け入っていこうという人は珍しいと思う。

2つ目の方法は今回やってみたがかなりヤバイことだけがわかった。
詳細は後述。

最後の方法はまだ真面目には試していない。
Natが簡単に取り出せるのでよいのかもしれないが、hetero equalityを使っている以上2番目と同じ危険性を孕んでいるのではないか、と思っているので今は積極的に採用したくない。

つらみへ

上で述べた2番目の方法のつらさについて解説する。

Canonical Extension

~は実は次のようにして、homのequality ==を用いて定義できる。(これはhom equalityの自然な拡張、あるいは貼り合わせとでも言うべき状態になっている)

Inductive Heq_hom {C : Category} {a b : C} (f : hom a b) : ∀ {c d}, hom c d → Prop :=
| mk_Heq_hom : ∀ {g : hom a b}, f == g → Heq_hom f g.

これはつまりconstructorとしてf == gからくるものだけを採用するという意味で、relationとしては異なるhom上では∅として定めるという方法だった。

さてhetero equalityではよくある話として、この型からequalityは取り出せない。
というわけでheq -> eqは公理として追加するのだけど、じゃあ公理はどうするの？という問題があって、

Axiom Heq_eq : ∀ {C : Category} {a b c d : C} (f : hom a b) (g : hom c d),
    f ≈ g → { eq : a = c ∧ b = d | extend (proj1 eq) (proj2 eq) f == g }.

当然これは最初に述べた方法のつらみから(equalityを直接扱うことのつらみから)解放されていないのであまり意味がない。
他の方法として、新たにarrow type(dom,codを無視した射の型)を作ってどうのこうのとする方法は思いついていたけれど、今度はarrow type constructorのinjectiveや他にも何らかの性質を公理として追加する必要がありそうだったのでやめた。

さて、まぁどうにかして上のようなHeq_homを(つらみは無視して)使って色々やっているとわかるのだけど、具体的に圏を作るたびにこのように対応するextended equalityを「公理とともに」追加しなければならない場合があって、実は上の方法はcanonicalだけど常にそれが欲しいものではないことがわかったりする。

例としてcomma圏のarrowのequalityは2本のarrowのpairだから、
定義としては<f,g> as comma_map ~ <h,i> ==> f ~ h & g ~ iとしたい気がするのだけど、これは当然非自明なので使いたいならまた公理として追加しなければならない。

と、ここまでくると、実はhetero equalityは圏によってspecificなものではないかという考えが沸いてくるわけである。

Extended Category

上の方法は一旦忘れて、圏の定義にhetero equalityを含めてしまおう。
つまり、圏のデータに~を要請し、category axiomに「~を各homに制限したものはhomのequalityに等しい」ことを要請することにする。

しかし実はこれだけではだめで、compositionと~のcompatibilityが足りないことがわかる。

Formalization業界ではよくしられていることとして、圏のデータにarrow equality ==を含める場合は実はcompositionとのcompatibilityも新たに定義に含める必要があり、そもそもそういう勝手な演算とそのcompatibilityを無闇に追加することを嫌って「Setoid-enriched」という理屈では素晴らしい定義を採用したのだけれど

我々はここにきてhetero equalityとそのcompatibilityを無闇に追加することと相成ったのである

困ったことに、==はenrichmentという仕組みが上手く隠蔽してくれていたが、~はheteroなので(各homごと、ではない)enrichmentして隠蔽とかいう問題でもない。

あるいは、こういう「圏全体に対するheteroなenrichment」という概念が別にあり、今度はそれが上手く隠蔽してくれるのかもしれない。

まぁしかし私は3つのequalityを使って証明を書く気はおこらないので、素直にhetero equalityを捨てるformalizationを考えようと思った。

なお、まだいい方法は見つかってない。