Sets な Topos

圏論の続き。Topos の定義はだいたい合っていたので例ぐらい書くだろと、Sets (関数型言語の圏)のToposと思ったんですが...

　　全然できない

Ωが要素二の集合ってのまで覚えていたんですが、米田先生のには{1,⊥}とある。でも⊥は作れないから1と同じじゃん...
nlab を見たところ Bool だと書いてある。結局、Agda 的にはBoolが良いらしい。

　　m
b →a →Ω

で、x : b で m x : a 、つまり、b の m による像が a にできるわけですが、その像に入っていれば true そうでなければ false.

ところが、その判定には排他律が必要。なるほど、Sets なToposは非構成的なのか。

m は monic ( f m ≈ g m →f ≈g )なんですが、使い所がわからなかったんだが、像とbが一対一対応するのに必要なのね。なるほど。

まだ、技術的な問題は残っているんですがなんとかできそう。Topos ま、なんとなくわかってきたかな。

きっと internal language までいけるが、もう授業が始まってしまうな。