Agda

この間からはまっていたのは、ようやっとできました。

＊　振動するんだよね

あっちやって行き詰まって、また別な方向やって、また、元に戻って。しまいには、

＊　やろうとすると、こういう風に行き詰まるというのを思い出すように。

今回は Maybe の使い方と、data を使った制約の書き方を学べました。

まぁ、圏論/Agdaは1個とか2個とかの具体的なことをやろうと思うと大変。証明の場合分けが爆発しちゃう。

入力の射の種類によって場合分けするんですが、

＊　起きないはずの場合わけが出てしまう

まぁねえ。それぞれの射にt0とt1があれば全部の組み合わせが出ちゃうよな。で、証明できない...

と思ったんですが、

＊　Maybeを扱っていると、just/nothingの組み合わせで出ないものがある

nothing と nothing　の等号はnothingになるわけなので、等号のところにはjustとは書けない。逆に等号がnothingだと、その両辺はnothing。

そうか、そうやって場合分けを制約することができるのか! 等号は data で実装されているので、data で場合分けの制約を書ける! とわかったので、なんとかなりました。

まぁ、あんまり綺麗な感じでないけどなぁ。

Agda の data は論理式としては排他的和で異なる型の組み合わせで、データ構造としてはタグ付きのUnion。

record は直積に相当して、用途としては「fieldに記述した論理式を満たす性質を持つもの」というように使うようです。

例えば、等号は、

　data _≡_ {a} {A : Set a} (x : A) : A → Set a where
　　refl : x ≡ x

こんな感じ。Prolog の f(X,X). ですね。同じ値で、refl a a みたいにしないと　a ≡ a を作れない。これを入力で受けると、

　　lemma1 : {a} ( x y : Set a ) ->　x ≡ y　-> ...
　　lemma1 {a} x y eq　= ...

で、x と y は同じ場合しか受け付けなくなるというわけ。なるほど。単一化、Unification という理屈だとはわかっていても、ちょっと気持ち悪いか。

二個の圏の対象は、

　　data　TwoObject {c₁ : Level}　: Set c₁ where
　　　 t0 : TwoObject
　　　 t1 : TwoObject

こんな感じ。t0 と t1 は constructor ですね。

それで、射を

　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　　
data Arrow {c₁ c₂ : Level } ( a b :　TwoObject {c₁} ) : TwoObject {c₁}　
　　　-> TwoObject {c₁} -> Set c₂ where
　 id-a : Arrow a b a a
　 id-b : Arrow a b b b
　 arrow-f :　Arrow a b a b
　 arrow-g :　Arrow a b a b
　 inv-f :　Arrow a b b a

という感じで、id-a は aからa、id-b は bからb。arrow-f は a から b という風に制約してみました。これで、

aからbの射とbからbの射を入力しているのに、abからabへのあらゆる組合せが出てきてしまっていたのが、ちゃん整合しているのものしかでなくなっって、ばっちり。

なるほどね〜　いや、まぁ、あんまい綺麗な方法とも思えないが... とりあえずできてめでたい。

いや、これを使って、LimitからEqualizaerを出して、それを使って、Floyd Adjunction Functor Theorem を証明するはずなのだが、まぁ、それはおいおいだな....