Graph からCCC

昔、Graph から圏はできたんだが、CCCをPostive logic経由で作るっ4てのができなくて、
Sets への関手を作って終わらすって技を出してたんですが、

　それだと、Setsの部分圏がCCCになってるかどうかわからない

なので、その関手の値が等しいという等号を使ってCCCを直接証明するというのを考えた

Lambek には「Minimum Equivalenceを定義する」とか書いてあるんですが、定義の仕方がわからん

f ≐ g → h ≐ i → (h ∙ f) ≐ (i ∙ g)

という resp ってのを示すのに苦労してたんですが、 (f ≐ g) → (f ≡ g)を使うのかと思ったんだが、
○ ⊤ と id ⊤ は同じなので、よろしくない。なんだか関手は

　fmap (g ∙ f) z ≡ fmap g (fmap f z)

という分配則があって、それを使うと証明できた。そういうことなのか

それで圏になったので、CCCを示すんだが、大体は refl でいける。ところが、

e4b-lem : {a b c : Obj PLC} {k : Hom PLC c (a <= b)} → PLC [ iv ((PLC [ iv ε (id ((a <= b) ∧ b))
o < PLC [ k o iv π (id (c ∧ b)) ] , iv π' (id (c ∧ b)) > ]) *) (id c) ≈ k ]

が、うまくいかない。でもじっとみてると

　関数外延性を仮定するといける

らしい。SetsのCCCでも *-cong を示すには関数外延性を仮定する。なので、必要ならしいです

で、まぁ、Graph から CCC はできた。

https://github.com/shinji-kono/category-exercise-in-agda/blob/e6cb3a1b8e9cadd3e17125fd999a61809665ab30/src/CCCGraph.agda

このあと、この構成が普遍問題の解であることを示す必要があるらしい。情報は落としてないのでいけるはずだが、できるかどうかは

で、これを使って Polynominal 圏が作れるはず。Comonoad でも示してるんだが、関数完全性が微妙にずれてる