Graph to CCC

元ネタの本では1ページなんですけどね。

　Graph → Positive Logic → Sets

はできたので、CCC全体の圏からGraph全体の圏への忘却関手

　Cart → Grph

と組み合せて随伴関手にするわけですが、

　Graph の Set のLevelが合わない

ここで判明したのは CAT (圏全体の圏)も異なるLevelの対象を許さないってこと。Agdaの限界かな。

で、Grph {suc n} から Grph {n} への変換を仮定することに。ダサいけど。

Sets ではなくSetsの部分圏って話はあったのだが、

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

だけではηは書けて solution の関手

　　 solution : {g : Obj Grph } {c : Obj Cart } → Hom Grph g (FObj UX c) → Hom Cart (F g) c

のFObjまでは書けるんですが、FMap が書けない。

　Graph　1 → Positive Logic 2→ Sets 2
　　　↑　　　　　　　　　　　　　　　　　　　　　 ↓
　Graph　1 ←　 Graph 2　 ←　　　　CCC 2

というのが普遍問題の流れ。

異なるPositive LogicはSetsで同一視されてしまうので情報が消えてしまう。生成手順を覚えてない。なので、部品な射のGraphからCCCを構成できない。

Hom PL を使うとCCCにならないからだめ。結局、

　　　fcat-pl : {a b : Obj PL} → Hom Sets a b → Hom PL a b
　　　fcat-eq :　{a b : Obj PL} → (f : Hom B a b ) → FMap CS (fcat-pl f) ≡ f

を仮定することにしました。

　Graph → PL → Sets

で作ってるんだから元の fcat-pl はあるんだが結果のSetsの射(=関数)から構成的には逆は取れない。

これは CCC の射から Positve Logic の射つまり具体的な証明手順を見つけることに相当するのではないかと。完全性定理ね。

で、それは構成的には証明できないので仮定するしかない。

もちろん Positive Logic なので個々の決定続きはあるんだが任意の対象についての証明は構成的ではないらしい。

そんなところではないかと。これで solution のFMapも一応書けた。まだ、uniquenessもやってないし、穴も多いが、ここまでかな。

　http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/tip/CCCGraph.agda