Graph to CCC の続き

続きです。

　　Graph にCCCの要素を入れて、射の同値類を作ればできる

とか簡単に書いてあるんですが、Agda での同値類の作り方は

　　data を作るか、Set のへの写像 eval を定義して eval f ≡ eval g にするか

なので、格闘していたんですがどうしてもできない。で、わかったのだが、

　　CCCの * とかεを残しておいてはだめ

さらに。

　 data SL : (t : Objs ) → Set　where
　　　func : {a b : Objs } → ( f : SL a → SL b) → SL (b <= a )

と言う風に書けない。つまり、λ計算を data に encode することはできないらしい。 strictly positive でないと文句を言われる。

つまり、 SL a → がだめらしい。

で、結局、諦めかけたんですが、Sets への関手を

　 fobj :　( a　: Objs　) → Set (c₁ ⊔ c₂)
　 fobj　(atom x) = ( y : vertex G ) → Chain y x
　 fobj ⊤ = One
　 fobj　(a ∧ b) = ( fobj　a /\ fobj　b)
　 fobj　(a <= b) = fobj　b → fobj　a

というように書ける。これで同値類を作ってやれば良い。

Chain はGraphから圏を作る時のこれ。　

　data Chain { v v' : Level } ( g : Graph {v} {v'} ) : ( a b : Graph.vertex g ) → Set (v ⊔ v' ) where
　　　 id : ( a : Graph.vertex g ) → Chain g a a
　　　 next : { a b c : Graph.vertex g } → (Graph.edge g b c ) → Chain g a b → Chain g a c

つまり、どこからかわからないが、x に到達する辺のつながりってこと。これを対象にすればよいらしい。これは関数なのでSetsの対象。

射の方は

　 tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b
　 tr f x y　= graphtocat.next f (x y)

とすればよい。つまり、一つ付け加えれば良いだけ。これは、差分リスト、あるいは、trace みたいなものだな。

結局。fmap は

　 fmap :　{ a b : Objs　} → Hom PL a b → fobj　a → fobj　b
　 amap :　{ a b : Objs　} → Arrow　a b → fobj　a → fobj　b
　 amap　(arrow x) =　tr x
　 amap π ( x , y ) = x
　 amap π' ( x , y ) = y
　 amap ε (f , x ) = f x
　 amap (f *) x = λ y →　fmap f ( x , y )
　 fmap (id a) x = x
　 fmap (○ a) x = OneObj
　 fmap < f , g > x = ( fmap f x , fmap g x )
　 fmap (iv x f) a = amap x ( fmap f a )

こんな感じ。CCC になるかどうかも調べましたが、やっぱり、Sets がCCCだってのを確認するのと同じ。

AのF : Functor A B によるBの Subcategory は

　　 Hom = λ a b → Hom B (FObj F a) (FObj F b)

ってだけで、対象は A と同じで、あとは全部Bとおなじですむらしいです。

https://stackoverflow.com/questions/2583337/strictly-positive-in-agda