日々の流転

λ. topos の internal language は?

ふと思ったので、調べもせずに書く。

• CCCの internal language は単純型付ラムダ計算
• LCCCの internal language は ∑ と ∏ による依存型を持つ型理論

では topos の internal language は何だろうか?

基本的には、∑ と ∏ による依存型を持つ型理論に対して、subobject classifier に関する項と規則を追加すればよいのだとは思うが、もしmonomorphismの判定(judgement)を入れるとすると、結構大きな拡張になるような気がする。 どう形式化するものなんだろうか……

【2008-04-20追記】 トポス (数学) - Wikipedia に「Kripke-Joyalの意味論とよばれる手続きによって集合論的論理式をトポスの対象と射についての言明として解釈することができる」とあった。 Kripke-Joyalの意味論については知らないのだけど、この意味論はトポスに対して完全なのだろうか?