Yoneda Functor

型Bから型Cへの関数全体を考えると、型Aから型Bへの関数fを使って、型Cから型Bへの関数全体を得ることができるってな話です。型Bから型Cへの関数全体ってのは集合だから、いろんな型と関数からなる圏から、型Bから型Cへの関数全体の集合を返すのは Functor と考えることができて、関数 f は、その Functor 間の自然変換を提供するというわけ。

grep と nkf で、nkf を Functor、grep を自然変換と考えて、grep してから nkf しても、nkf してから grep しても結果は同じってのが、grep の自然変換の可換性ってな例を考えました。

この辺りはわりとわかりやすくて、最初に読んだ時にもちゃんと理解していたはずです。役には立たなかったけどな。その後、勉強して理解したつもりになっていた頃は、明らかにずれていた。そういう時もあるよ。

今回、Agda で証明して得るものは、苦労した割には、それほどなかった気もする。Sets と圏が入り交じるのが難しい。あと、Full Embedding ( 二つの型から型への関数全体が等しければ、それぞれの型は等しい )ってのは、どうも証明できないみたい。

＊ Hom A a b = Hom A a a → a = b

背理法を使えば自明なんだけど、Agda は背理法は使えないからなぁ。本の方でも must be とか、歯切れの悪いことが書いてあるので、きっと背理法抜きではできないのだと思います。いや、できるのかも知れないけど。

refl で受けると、a と b が違うと言ってくる。なんていうか「前もって同じだとわかっているものしか同じだと証明できない」みたいな感じ。 A [ f g ] → Category.dom A f ≡ Category.dom A g とかはできるんだけど。

これから、卒業生たちと飲みに行くみたいです。