CCC from Graph の続き

なんか朝起きて、少し頑張ったらできました。

証明が繋がることは繋がるのだが、同じ式でも穴開けると通ったり。

　　fmap で型の指定が足りないみたい

なので、fmap のmoduleの指定を増やしていく方向に。

　　Graph にCCCの構造を足す　　　　data Arrow
　　それから圏を作る　　　　　　　 data Chain
　　その圏からSetsへの関手を作る　 fmap

という手順だったんだけど、 Arrow と Chain の関数を分離できることに気がついたら一発でした。

ところが、その後、 「これも要らない」「あれも要らない」になってどんどん証明が小さく。


　 amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b
　 amap {G} (arrow x) = smap G x
　 amap (○ a) _ = OneObj'
　 amap π ( x , _) = x
　 amap π'( _ , x) = x
　 amap ε ( f , x ) = f x
　 amap < f , g > x = (amap f x , amap g x)
　 amap (f *) x = λ y → amap f ( x , y )
　 fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
　 fmap {G} {a} (id a) = λ z → z
　 fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ]

　　　 distr : {a b c : Obj (DX G)}　{ f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z)
　　　 distr {a} {b} {c} {f} {next {b} {d} {c} x g} z = adistr (distr {a} {b} {d} {f} {g} z ) x where
　　　　　adistr : fmap (g ++ f) z ≡ fmap g (fmap f z) →
　　　　　　　( x : Arrow (graph G) d c ) → fmap ( next x (g ++ f) ) z　≡ fmap ( next x g ) (fmap f z )
　　　　　adistr eq x = cong ( λ k → amap x k ) eq
　　　 distr {a} {b} {b} {f} {id b} z =　refl

え、こんだけ? あんなに苦労してたのなんだったんだ。

要するに、CCCで拡張した部分は「一つの射」なので、その部分はグラフから圏を作る部分とは独立らしい。

今までダメだったのは、fmap で Arrow と Chainが一緒になっていて、Agda が混乱していたせいみたい。
fmapとamapで分離されていて、fmap の再帰の部分が amap の再帰から切り離されているのでうまくいくみたいです。

amap の部分を見ると、

　 amap (○ a) _ = OneObj'

とかで、「とにかく a から T への射は全部同じ」とか

　 amap π ( x , _) = x

で「積から積の要素への射は、これ一つ」になるのがわかりやすい。

やってみると「smallest equivalence relation between proofs」ってのがどういう意味かわかりました。
そんなもの。

module をまたいだ再帰はだめってのは鉄則みたいだな。