インスティチューション、マルチ・インスティチューション、マンダラ
最近、マンダラの精神を忘れていたかも知れない。「この世はマンダラだ」
- マンダラ→ http://d.hatena.ne.jp/m-hiyama-memo/searchdiary?word=%2A%5B%A5%DE%A5%F3%A5%C0%A5%E9%5D
- ミニマンダラ→ http://d.hatena.ne.jp/m-hiyama-memo/searchdiary?word=%2A%5B%A5%DF%A5%CB%A5%DE%A5%F3%A5%C0%A5%E9%5D
マンダラ状況を説明するのに向いている構造がインスティチューションだが、そのインスティチューションでも、とこかしっくり来ないことがある。
インスティチューションをJとして、ModJ(Σ) をモデル圏とする。モデル圏は単項引数で決まるが、これは、ModJ(Σ, C) と二項であるべきだ。二項にすることによって、説明できることが拡がる。例えば、F:C→D で誘導されるセマンティック圏Cの切り替えが説明できる。
- ModJ(Σ, C)→ModJ(Σ, D)
例えば、Set→Boolに基づくセマンティック圏の切り替えは、型付きラムダ計算のモデルと古典二値論理のモデルのあいだの関係を説明できる。
複数のインスティチューションを同時に考えることは必要だ。このとき問題になるのは、
- 指標圏は、単なる圏ではなくて、2-圏や二重圏になっている。
- モデル関手 Mod(-, -) の行き先はCatではなくて、構造を持つ圏からなる2-圏（ドクトリン）のことが多い。
- モデル関手は関手ではなくて、疑関手（タイト2-関手）になっている。
高次圏、少なくも2次元の圏で考える必要がある。標語は、
- 指標圏は2-圏（指標が圏だから）、モデル圏の圏も2-圏なので、モデルファミリー（インデックス付き圏）は2-関手である。
次に問題なのが、Sen(Σ)だ。実際は、Mod(Σ, C)の対象XごとにLogic(X)のようなX上の論理系が付随していて、全体としてハイパードクトリンになっているのではないか。各モデル圏に終対象1Σがあり、Logic(1Σ) = {true, false} と古典二値真偽値になっている、と。
Sen(Σ)はあるだろうが、実際には、p∈Sen(Σ) に対して、(p on X)∈Logic(X) が決まるのではないか。この(p on X)をハイパードクトリンの前送りにより1に持っていくと真偽が決まる。その真偽が決まる機構を |= と表している。と、そういうことなのではないかな？
