Graph から CCC

ってのを agda で書くってのをやってるんですが、ぜんぜんできないです
もちろん、Graph から圏は、辺のリストを使えば簡単

ずいぶん昔に、Positive Logicってのを圏だと示すってのはやってて。
その延長でできるだろうってことなんですが

　　id と ○ a が唯一である必要がある

ってところからわかんない

教科書(LambekのIntroruction to Higer order categorical logic)には、
Graph から Deduction System を作って、それから smallest equivalence relation を使ってCCC を作るとか書いてある

Sets がCCCは割と簡単に示せる。(*-cong には関数外延性が必要) 。Deduction System って Sets のことか?

Setsだと、射は関数なので、○ a : a → ⊤ は、tt : ⊤ を返す関数でよい。aが ⊤ なら、id と一緒だ

comonad で A[x] を書くってのはできたが、Functional compleness がなんかおかしい。なので、Graph からCCCを書くという
気になったのだが...