Topos 一段落

定義の直後にある N≈N+1 まで片付けたので。この後は internal language つまり型つき高階λ計算になるので戦略が異なるはず。

いつものことだが、定義が微妙にずれてて少しはまりました。夜中じゅうやってて眠い。

基本は以下の pull back で、
　　　　○ b
　b ─────→ 1
　|                           |
m |                           | ⊤
　↓       char m     ↓
　a ─────→ Ω
　　　h
　monic m に対して Subobject classifier Ω への char m
　h に対応した equalizr m = Ker m

の二つの方向があると。これで equality とか　∨　とかをなんとかできるらしいです。

char m は唯一つで、m は iso だという定義が微妙だった。

あと

　　f     g
　1 → a → a

の自然数図式の始対象を持っている(単なる for 文)ってのから、N≈N+1 がでるところまでやりました。

集合の濃度の話っぽく見えるけど、そうなのかも知れん。

一階述語論理だとこういう議論は難しいので、圏論/直観主義論理ベースで数学をする方がわかりやすい。

まさかとは思うけど、一時期中学高校に集合論が導入されたのと同じような感じで、圏論/推論が入る可能性もあるかな。