Functional completeness

なんか、かっこいい名前でな〜 圏 A の任意の対象 a (つまり適当な命題)を真だと仮定する、つまり、

　　x : T → a

というの付け加えるのを Polynominal A[x] っていうだけなんですが、二年前からさっぱりわからなくて。

なんだが、なんか降ってきて、別に圏Aそのままで良くて、おまけに x : T → a を使ってる部分を付ければ良いんじゃないかと。

　record PHom {a ⊤ : Obj A } { x : Hom A ⊤ a } (b c : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)　where
　　field
　　　 hom : Hom A b c
　　　 phi : φ x {b} {c} hom

でも、そうすると、A[x]を作る部分には何もしなくて良くなる(計算はhomだけな)のでだめだろと思ったんですが、A[x]があれば、

　　Functional completeness を Agda で書き下せる

で、取りあえず書いてみたら、なんか教科書通りの証明式が...

　　なんだ、それでいいのかよ!

CCCな圏をグラフに戻してxを付け加えて再構成とか書いてあったのに使わないんですか。そんなんで良いんですか。

まぁ、わかんなかったのができたのはめでたい。