外延性

昨日も(っていうか今朝まで) Agda いじてっていて、なんか珍しく口内炎くらいました。

Monad のいつもの例題をいじっているだけ。しかも、

＊ T : A -> M x A ( A は集合、Mは Monoid 、x は直積)

という極めて簡単なものなんだけど、ある意味で簡単なものほど難しいものだよね。こいつは Haskell では簡単に書けたのに、
Agda では、まったく歯が立たず。 http://seeker-s-eye.blogspot.jp/2013/08/monad.html

Haskell にそって data とかを定義して、それを圏にしてとかいうのは、途中まで頑張ったのですが、どんどん違う方向に
いってしまう。でも、そこで Monoid の要素が Carrier という名前の Set だというのがわかりました。

そこで、最初の頃に作った、Sets (既に定義されている圏で、射が Agda の関数 ) と直積を組み合わせる方向に戻って、
みたら、あっさり、T と ηとμが定義できた。しかも、

＊　　結局、教科書に書いてあるとおりの定義

いや、もちろん、そうでなければならないんだけどさ。

＊ FObj = λ a → (Carrier Monoid) × a
＊ TMap = λ a → λ(x : a) → ( ε , x ) ;
＊ muMap a ( m , ( m' , x ) ) = ( m m' , x )

なんとなく、信用してなかったようです。で、そこから楽勝。だと思ったのだが、Monad の性質を満たすことの証明が、まったくできない。全然できない。

＊ ( λ x → (( ε (proj x)) , proj x )) = ( λ x → x )

を示せば良いだけで、εが Monoid の単位元で、( ε (proj x)) が (proj x) を返すとわかれば、

＊ ((proj x) , proj x ) = x

つまり、直積はその成分の直積だってことで、これ自体は簡単。なんだけど、どうしても証明できない。λ x -> x のλ x を
cong で構成するとかやってたのに歯が立たず。で、証明できない式自身、

＊ (f x ≡ g x) -> (( λ x -> f x) ≡ (λ x -> g x)

でググってみたら、

＊ http://math.stackexchange.com/questions/154704/if-fx-gx-for-all-xa-why-is-it-not-true-that-lambda-x-fx-lambda
＊ If f(x)=g(x) for all x:A, why is it not true that λx.f(x)=λx.g(x)?

え? 証明できないの? はぁ?

＊ http://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/
＊ function extensionality

というものらしい。

＊ ∀x -> (f x ≡ g x) -> f ≡ g

ってのを公理して仮定しろと。確かに、Agda の library にも仮定(postulate)するように式が書いてある。超良くある質問らしいです。

そう言われて見ると、ZFの 外延性の公理 (extensional principle )

＊ ∀ {x} x∈ f ⇔ x ∈ g → f ≡ g

と(要素がすべて同じなら同じ集合)にクリソツ。これを仮定したら、ちゃんと証明出来ました。朝の5時に。あだだだ。 これも元の本では三行なんだよな。