CCC gererated from Graph

いつもの Higher order categorical logic には半ページで「○とかπとかの射を足して、CCCになるように射の同値類を入れればできる」とか書いてある。

けど、ぜんぜんできないです。グラフは、

　　vertex (ノード、グラフの点)
　　edge (vertexの二つ組)

の集合。これは record で普通に書ける。これに、id と edge のつながりを表す data を入れてやると、

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

　_++_ : { G : Graph} {a b c : Graph.vertex G } (f : Chain {G} b c ) → (g : Chain {G} a b) → Chain {G} a c
　id _ ++ f = f
　(next x f) ++ g = next x ( f ++ g )

これでGraph から生成した圏のできあがり。簡単。これに、CCC の構造を足して、

　 data Objs {G : Graph } : Set where
　　　atom : (vertex G) → Objs
　　　⊤ : Objs
　　　_∧_ : Objs {G} → Objs {G} → Objs
　　　_<=_ : Objs {G} → Objs {G} → Objs

　 data Arrow {G : Graph } :　Objs {G} → Objs {G} → Set where
　　　arrow : {a b : vertex G} →　(edge G) a b → Arrow (atom a) (atom b)
　　　id : (a : Objs ) → Arrow a a
　　　○ : (a : Objs ) → Arrow a ⊤
　　　π : {a b : Objs } → Arrow ( a ∧ b ) a
　　　π' : {a b : Objs } → Arrow ( a ∧ b ) b
　　　ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
　　　<_,_> : {a b c : Objs } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
　　　_* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )

この二つは vertex と edge に使えるから、

　 DX G = GraphtoCat ( record { vertex = Objs {graph G} ; edge = Arrow {graph G}} )

こんな感じで、CCCの構造が入った圏まではできました。おそらく Positive Logic とか言われるものなはずです。

あとは同値類を入れれば良いわけなんだが、なんか難しい。data CCCeq みたいなのを足すと結構組合せが爆発。

そこて、

　 DX G から Sets への関手を作れば、Sets は CCC だから証明終になるんじゃないか?

ってのを思いついた。確かに、自然数から剰余への関手を作れば同値類な部分圏が作れる。で、順調だったんですが、

　　fmap の定義の termination を Agda 理解してくれない
　　関手の分配則の証明が難しい

なので結局できてないです。

それでも、最後の二つ以外はだいたい通ったので、まったく外れというわけでもないみたい。

_* なしだと、Cartesian までいくけど、Closed でないってことになるらしいです。

あともう少しだな。_* だけ data でなんとかするってのが良さそうだが...