Bi-cartesian Closed Category

Topos は Pull back で書くとか割と順調なんですが、教科書通りだと

　　Internal Language つまり、直観主義論理/型付きλ計算

に突入。なんか重いな。なので、去年やり残したところをちょっとやってます。

Cartesian Closed Category は積(つまり∧)しか入ってないので、和(つまり∨)を入れようって話。問題は、

　　○ : Hom A a １

の双対の

　　□ a : Hom A ⊥ a

つまり「矛盾からは何でも出る」って奴が入るってことね。CCC には

　　Hom A (a ∧ ⊥) c ≈ Hom A ⊥ (c <= a )

があるので、

　　 Hom A a ⊥ -> a ≈ ⊥

が出てしまう。(いや、割と道のりは長いんですけど) T 側でも状況は同じで、Bi-cartesian Closed Category には

　　実質的に二つしか対象がない、つまり Bool 代数になる

ことになるわけ。命題論理になってしまうわけだな。なので、直観主義論理/型付きλ計算のモデルには使えないので

　　Topos

ってことになるらしい。あとは、

　　Functional Completeness (= coMonad)

をやると、復習のネタは尽きるみたい。去年はここでGraphに走ってしんだはずです。合流性とかC-Monoid とか載ってるけど、まぁ、いいかな。