昨日（2019-06-06(日曜)）、インスティチューション理論についてほんの少しだけ説明しました（チアガールズの説明のほうが長かった気がする）。インスティチューションについては、「キマイラ飼育記」の初期の頃からチョコチョコ触れています。
インスティチューションに関する資料として、僕が最初に思い浮かべるのはゴグエン〈Joseph Goguen〉による次のページです。
Maintained by Joseph Goguen
Last modified: Fri Jan 6 07:46:59 PST 2006
ゴグエン先生は2006年7月3日に亡くなられているので、それ以降はメンテナンスされていません。このページに目ぼしい論文へのリンクがあります。外部サイト（arXivとか）へのリンクではなくて、ローカルリンクですね。PostScript形式が多いです。
インスティチューション理論では、指標の圏Signと、指標Σに対するモデルの圏 Model[Σ] は公理的に与えられるのですが、Sign, Model[Σ] を具体的に作りたいことが多いので、作り方（の一例）を述べます。
まず、指標Σはコンピュータッド（nLab項目 computad）だとします。（適当な条件を付けた）コンピュータッドとコンピュータッド準同型からなる圏が Sign = (指標の圏) ですね。コンピュータッドΣから生成されるn-圏をΣ◇としましょう。モデル（指標の意味となる実体）が棲むn-圏をCとして、Model[Σ] を次のように定義します。
- Model[Σ] = C-Model[Σ] := [Σ◇, C]
[Σ◇, C] は関手圏です。n = 2 、つまりΣは2-コンピュータッドであり、CがSetを自明に2-圏とみなしたもの*1であるケースが一番よく使われる設定です。
例えば、有向グラフ（ここでは単に「グラフ」と呼ぶ）の指標は次だとします。
signature Graph :=
begin
sorts
V /* 頂点集合 */
E /* 辺集合 */
operations
src:E→V /* 辺の始点 */
trg:E→V /* 辺の終点 */
laws
/* 特になし */
end指標Graphから、ソートEとオペレーション src, trg を落としてしまえば、集合の指標になります。
signature Set :=
begin
sorts
V
operations
laws
endSet⊆Graph という包含を表す指標射を j:Set→Graph in Sign として、Model[j]:Model[Graph]→Model[Set] in CAT が対応する忘却関手です。
- 参考： 肖像権・著作権処理済みスライド [追記]既に非公開[/追記]
- 仏教とインスティチューションの関係は： 大乗仏教中観派と一般モデル理論
