圏論と Agda の続き

Sheaf の方は、6月にできそうとか思ってたんだが、Γ と L の随伴関手を示すんだが、Γはできたんだが、L が...

https://github.com/shinji-kono/category-exercise-in-agda/blob/41031f5d52ff5563888262ae6619aa4ba582fda4/src/Sheaf.agda

それでも、かなり、うまってきて、随伴関手の自然変換まで行き着いたんだが

　Agda が止まらなくなってきて

どうも、implict variableを書かないと止まらなくなるらしく

そこで、少し飽きたので、別な方を始めました

＊ 圏とグラフの随伴関手

ね。CCCでやるんだが、難し過ぎるので圏とグラフで。二週間くらい戦ったら書けた
https://github.com/shinji-kono/category-exercise-in-agda/blob/41031f5d52ff5563888262ae6619aa4ba582fda4/src/CCCGraph.agda

で次は

＊ Polymonimal 圏と、関数完全性

なんだが、こっちは、なんかだめ。

1) Polymonimal 圏ってのは、x : 1 → a を付け加えた CCC で、演繹定理で作れる
2) だが、その時に x の違いを無視する同値類で考える
3) すると関数完全性が成立する
4) それは実は coklisli 圏で、Polinominal 圏は、それに iso

いや、なんかPolymonimal 圏っぽい CCC は作れる。coklisli圏も。だが、関数完全性がだめ

同値類がうまく作れない。coklisli 圏で関数完全性を記述する方法がわからない

https://github.com/shinji-kono/category-exercise-in-agda/blob/41031f5d52ff5563888262ae6619aa4ba582fda4/src/Polynominal.agda

ちっとあきらめかな

また Sheaf をやるかと考え中