System(Γ, Σ)

疲れた、ヘロヘロだ。朦朧状態。

インスティチューションIの上のプログラムの圏Progは、|Prog| = |Sign|であり、自然な埋め込み Sign ⊆ Progがある。つまり、SignがProgの広大部分圏で入っている。

[追記]自然な埋め込みがあるのではなくて、埋め込みの族があるような気がする。それは、翻訳系（トランスデューサ）の圏に単なる写像の圏を埋め込むようなことだろう。このときは、状態空間で添字付けられた埋め込みの族が存在する。[/追記]

射 Σ→Γ in Prog とは、集合レベルでの写像 Σ → Term(Γ) 。つまり、{σi := τi}のように書ける。τiはTerm(Γ)に属するので、use Γ provide Σ なプログラムコードとなる。

Prog(Σ, Γ)は、リファクタリング（プログラムの規則的書き換え）により圏となるから、Prog全体は2-圏となる。p:Σ→Γ in Prog があると、ΓのモデルからΣのモデルを構成できるので、Mod(Γ)→Mod(Σ)の関手としての解釈ができる。つまり、Modの拡張Mod'を Prog→Catとして構成できるが、これは2-圏の関手（2-関手っていうのか？）になるような気がする。

それで、p:Σ→Γの意味を Functor(Mod(Γ), Mod(Σ))のなかで求めるのだが、それより手前(?)にシステムの圏とでも呼ぶべき2-圏があって、pの意味はProg→Systemという反変2-関手で定式化されるべきだ、という気がしてきた。

んじゃ、Systemって2-圏はなにか？ 特にhome-catであるSystem(Γ, Σ)ってのがなにか？ それは、use Γ provide Σ なプログラムコードのコンパイル結果（なんらかの実行可能なもの）なんだと思う。e:Γ→Σ in System があると、指標Γなモデルから、指標Σなモデルを構成できるから、Mod(Γ)→Mod(Σ)という解釈が可能となるのだろう。

もっと大事なことは、System(Γ, Σ)が余代数の圏（と似た）の構造を持ち、終対象を持つことだろう。Φが空指標だとして、use Φ provide Σな実行プログラムは、ライブラリやプラットフォームなしのネイティブ・プログラムのはず、となると、System(Φ, Σ) = Mod(Σ) なのかもしれない。|Sign|上の2-圏Systemは、Modより基本的な存在かもしれない。 -- 朦朧としているから、幻想か？