計算可能世界ってなんだ？ トポス（もどき）かも
計算可能なデータ領域と関数の圏をComputableとでもする。と、名前を決めたところで、The Computableが定義できそうにない。なんか適当な定義をでっちあげても、その圏が The Computableだと主張する根拠がない。だが、いろいろなA Computableを定義できるので、計算可能な世界は、単一の圏ではなくて圏のレルムだと解釈すべきだろう。このレルムを調べることが計算可能性を調べることだろう。
計算可能性の圏論的定式化では、EPペア（レトラクト）、ベキ等射などを使う。この部分は比較的整備されている。例えば、圏C内で対象Xのレトラクトの全体をRetr(X, C)とすると、これはEPペアの圏CEPを使って、Retr(X, C) = CEP/X と書ける。レトラクトからベキ等射を作るのは自明だ。モノ射m:A→X がレトラクタブルなことと、mがEP圏の射であることは同値。レトラクタブルなモノはベキ等射で表現可能。
レトラクタブルなモノ射*1（の同値類）の全体は、把握可能な部分対象だと思ってよい。つまり、Subobj(X) のようなもの。Subobjが出てくると、なんかトポスの匂いがする。計算可能な圏、A Computableはトポスになるんじゃないだろうか？ トポスそのものじゃなくても、かなりトポスに近い。
トポスの部分対象分類子を特性射と呼ぶことにする。特性射の定義には、真偽集合（真偽値集合）に相当する真偽対象が必要だが、対象Ωと終対象1から射t:1→Ωの組が真偽対象となる。対象XからΩへの任意の射p:X→ΩはX上の述語と呼ばれる。
A → 1
｜ ｜
↓ p ↓t
X → Ω
上の四角形がプルバックになるとき、A→Xは述語pの核と呼ぶことにする。pの核は、ほぼpの外延だと思ってよい。気持ちとしては A = {x∈X | p(x) } 。ただし、述語pに核が存在する保証は一般にはない。A→X が先に与えられたときは、pはA→Xの特性射と呼ぶ。気分としては部分対象Aがpで把握される*2。
計算可能関数は集合論的には部分写像なので、計算可能な圏の終対象は空集合である。真偽対象は単元集合で、自明な埋め込みをt（true）として取れる。部分対象が把握可能とは、それが計算可能関数の定義域となる集合のことである。
述語とレトラクトの相互変換は簡単なので、述語で把握可能な集合とレトラクタブルなモノ射（の同値類）は1:1で対応する。この状況は、当該の圏がトポスか、それに近い構造を持つことを示唆するだろう。
