Agda の謎

今日もおとなしくしているわけですが。(つまり、酒は飲まないという意味です)

ちょっと前から行き詰まっている Agda を見直してみました。

＊　Floyd の Adjoint Functor Theorem

が目標なわけですが、その前に、

＊　Limit から Equalizer と Product を作る

というのがあって。これ自体は全然難しくないんですけどね。なんだが、そのためには、

＊　Agda 上に有限な射を持つ圏を作る

ちょっと試行錯誤して、List と memberp (ある要素がリストに含まれているかどうかを調べる述語)はできました。これを使って、

＊　Hom(射)とObj(対象)の集合

を作ってやれば良いわけだ。ある record で memberp x list = true になる x を要素すると定義すれば良いんじゃないかな。それで、対象と射はできました。

圏なので、edge の演算を定義するわけなんだけど、

_×_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C

ってな感じ。なんだけど、「ない arrow はどうするの?」って問題が。 Agda はどうも、この「ありません」ってのをどうあつかっていいのか良くわからない。

この A B C にあらゆる可能な Obj の要素が入ってしまうので、困ってしまう。Hom A C は集合なので、空集合でも良いはずなのだが。Hom A Aは必ず一つはあるけど、そうでない場合は空集合な可能性がある。でも、Agad って集合 A があると、

a : A

とかで、必ず要素が取れてしまう。こまったなぁ。

_×_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C

の矢印も「ならば」と思って良くて、BからCへの射と、AからBへの射があれば、AからCへの射があるっていう意味なはずなけどな。

でも証明を書いていくと、A,B,C のすべての組み合わせだが出てきてしまう。射がないところにぶちあたると、そこで矛盾。あだだ。うーむ。この方法ではだめなのか。