世界と分類とハイパーインスティチューション

圏論的な世界〈world〉を次のようなものだとする。

1. 世界の構成素を領地〈dominion〉と呼ぶ。
2. 領地は、高次の圏、複圏、多圏のいずれかである。
3. 領地は有限個である。
4. それぞれの領地は小さいn-圏, n-複圏, n-多圏である。
5. 領地の次元は有限で、最高次元nが領地ごとに決っている。最高次元より高い次元の射は考えない。
6. 領地はなんらかのドクトリンに所属して、ドクトリンにより振る舞いが制御されている。
7. 領地のあいだの関手、複関手、多関手、自然変換、その他の関係などがあり、それが世界の構造を決めている。

世界を背景とした構文システムを考える。構文システムの基本は名前である。名前は世界のなかのモノを指す。名前とモノの対応（名前→モノ）を意味割り当て〈semantic assignment〉と呼ぶ。

名前に意味割り当てする前に、名前のソートとプロファイルを決める。名前のソート／プロファイルを決めることを、ソーティング、プロファイリングを呼ぶ。（ソート／ソーティングの代わりに、ディヴィジョン／ディヴィジョニングがいいかも。）

• 名前のソートとは、その名前が指すモノが所属する圏と次元のペアで、Cn の形で書く。例えば、Set0 なら「集合圏の対象を指す」、Vect1 なら「ベクトル空間の圏の射を指す」。
• 名前のソートの次元（ランクと、レベル、グレイドなどと呼ぶかも知れない）が1以上のとき、プロファイルは、A→B とか F⇒G:C→D のような、域と余域を明示した形。特定のホムセットが決まる。

便宜上、0次元の名前のプロファイルは、圏（の名前）そのものだとしておく。圏の対象類は0次元のホムセットだと言えなくもない。高次元の射ほど、プロファイルによる絞り込みの度合いが強い。高次射のプロファイルを求めるには、下位次元の射のプロファイルをすべて確定しなくてはならない。

名前は単純項とも言える。名前より複雑な構造を持つ項〈term〉を考えるが、項もソーティングとプロファイリングされる。項のプロファイルを求める計算をプロファイル計算と呼ぶ。型推論はプロファイル計算の特殊事例である。

名前にプロファイルを指定する（プロファイルの宣言、プロファイリング）には、次の構文を利用する。

• 次元0のプロファイルは、name in 圏 の形で、キーワード'in'を使う。
• 次元1のプロファイルは、name : A→B in 圏 の形。A, Bは圏の対象で、nameは射を指すことになる。A, Bのプロファイル（所属する圏）が事前に分かっているなら、in 圏 は不要（書いてもいい）。
• 次元2のプロファイルは、name :: F⇒G:A→B in 圏 の形。F, Gは圏の1-射で、A, Bは圏の対象〈0-射〉。nameは2-射を指すことになる。in 圏 と :A→B は場合により省略可能。
• コロンは、射の次元と同じだけ並べる。1-射なら１個、2射なら2個。矢印の太さも射の次元と合わせる。3射は、苦し紛れで '≡>' を使う。0-射はコロン0個なので、代わりにinを使う。

プロファイリングされた名前に対して、同じプロファイルを持つ項を対応させることを、構文的割り当て〈syntactic assignment〉と呼ぶ。構文的割り当てを、束縛と呼ぶ場合が多いが、束縛変数を作ることも束縛なので、ここでは接着〈attach〉を使う。

• 名前に対して、項を束縛する → 名前に対して、項を接着する

名詞も接着〈attachment〉。

名前の集合、またはコレクション（編成構造を持つ集合）に含まれる名前に、すべて意味割り当てをしたモノをその集合またはコレクションのモデルと呼ぶ。モデルに対しては、その準同型射が自動的に決まるので、特定の集合／コレクションに対してモデルの圏が自動的にできる。

上記の名前の集合／コレクションが指標〈signature〉しがって、指標（プロファイリングされた名前のコレクション）があれば、自動的にモデル圏を構成できる。

名前と項の接着の集まりは、指標（プロファイリングされた名前のコレクション）のあいだの射を定義する。よって、適当な条件を満たす接着の集まりを指標射〈signature morphism〉と呼ぶ。

指標を型文脈／型環境、指標射を代入／置換と呼ぶことがある。しかし、項を定義する構文が複雑だと、指標射はプログラムになる。項を定義する構文（文法）は、単純な指標圏（名前集合の単なる写像の圏）の上のモナドになり、その項モナドを使ったクライスリ圏が（複雑な）指標圏となる。クライスリ圏構成は対象類を変えないので、指標圏の対象は最初と同じ指標である。

実際の指標の構文としては、名前のソートごとに区分したセクション化名前集合がいいだろう。この構文だと、セクションにより最初からソーティングされている。セクションの名前＝ソート〈種〉のラベル となる。

最初に与えられたアンビエント圏が、その上にハイパードクトリンを備えているとする。すると、指標圏の上にハイパードクトリンを拡張できる。拡張したハイパードクトリンは、もとのハイパードクトリンと大差ない。

世界があれば、モデルが定まる。指標圏上には、モデルを対応させるモデル・インデキシング（インデキシングとインデックス付き圏は同じ）がある。一方、拡張したハイパードクトリンからもインデキシングが決まる。モデル・インデキシング＝意味的インデキシングと、ハイパードクトリン＝構文的インデキシングを組み合わせてインスティチューションを作れるだろう。このインスティチューションを非制約インスティチューション〈unconstrained institution〉と呼ぶ。

非制約インスティチューションのなかでは、論理式〈formula〉と定理・公理・証明と推論規則がハイパードクトリンとして備わっているが、指標圏＝インデキシングのベース圏では、プロファイリングしかしてなくて、論理的制約はまったく使われてない。

論理的制約を指標の命題部〈命題セクション〉と規則部〈規則セクション〉を持つ名前コレクションを作り、それを新たに指標と考えて指標圏を作る。これは、もとの非制約インスティチューションからグロタンディーク構成をしたもの。新しい指標圏をハイパー指標圏、またはハイパーベース圏と呼ぶ。ハイパー指標圏上に作ったインスティチューションを制約付きインスティチューション、あるいはハイパーインスティチューションと呼ぶ。

ハイパーインスティチューションに関して、次の定理が欲しい。

• エルブランの定理： ハイパーインスティチューションのモデル圏はエルブランモデルだが、同じ構文的インデキシングを持つ、どんなインスティチューションに対しても、そのインスティチューションにおける真概念は、エルブランモデルのインスティチューションで確認できる。したがて、エルブラン・インスティチューションだけを考えておけば良い。
• ゲーデル／カリー／ハワードの定理： ハイパーインスティチューションをもとの非制約インスティチューションに埋め込むことが出来る。この埋め込みはレイフィケーションで、ゲーデル符号化の一種と考えられる。埋め込みは、メタ巡回的的埋め込み〈meta-circular embedding〉となる。

もし2つの定理が成立するなら、ハイパーインスティチューションには、自動的にメタ巡回構造が備わっていて、同一の構文・論理フレームワークを持つインスティチューションのなかで普遍的なインスティチューションであることが分かる。

ゲーデル／カリー／ハワードの定理は、それ以上にメタ階層を昇る必要がないことを示し、エルブランの定理は、それ以上にモデルを考える必要がないことを示す。もし、これがホントなら、ハイパーインスティチューションは閉じた（正確には閉じてもよい）構文的・意味的構造を提供することになる。あくまでも「ホントなら」だが。