12/02/09 08:01:45.94
656 ：446：2011/11/26(土) 10:57:45.95
いや、なんでもできるわけではない。
例えばベクトル空間の圏は、cartesian closed にならない。
cartesian closed categoryの上位にmonoidal categoryがある。
cartesian closed は任意オブジェクトA,Bに対して
AｘB→A
↓
B
さらにB^AｘA→Bのユニーク性、また→1をもつもので、
B^AってのはAからBへの射だから、
a→b∧aならばbっていう三段論法が出てくるのすぐわかる、
これでハイティング代数がcartesian closed になることがわかる。
ハイティング代数⇔直観主義論理。選択公理入れれば古典論理完成。
さらにB^AｘA→Bのユニーク性はλ計算の関数適応にも対応。
関数のカリー化からきた考えだから当たり前だけど。
トポスは集合論を解釈する具体的な真偽値を与えるために
subobject classier（これは大抵真と偽の2元集合）を導入したもの。
函手の表現可能性⇔ universal elementの存在なので、
トポスに出てくるΩってのはこれのこと。
例えば集合の圏Setの簡単な例。
2＝{0,1}、Fは函手、集合S'⊆Sのとき、
F(x)＝1(x∊S')
F(x)＝0(￢x∊S')
これがトポスだと以下のようになる...。
S'⇒S
↓ ↓F
1→2(subobject classier)