関手圏によるモデル圏構成、代入系の圏

昨日：

表層的な現象が見えているけど、背後にある仕掛けがわかんない状態はイライラするね。もうヤメタ、、、、って止めないけど。

あいかわらずイライラ。が、わかることだけ記録しておくしかない、クッソー。

とりあえず、Σを普通の多ソート指標とする。つまり、ソート記号の集合Σ_Sと関数（演算子）記号の集合Σ_Fがあって、

• arity:Σ_F→(Σ_S)^*
• coarity:Σ_F→Σ_S

という写像がある。

ambient categoryであるCはデカルト圏だとして、ΣのCモデルMは、M_S:Σ_S→|C|とM_F:Σ_F→Cの組。次の条件を満たす。

• ε（空列）に対してM(ε)=(Cの始対象)、M(s1,...,sn)=M(s1)×...×M(sn)としてMを拡張すると、dom(M(f))= M(arity(f))、cod(M(f)) = M(coarity(f))

Σから記号的に自由生成される圏をΣ~ とすると、MはΣ~からCへの直積保存関手となる。Model(Σ; C) = Functor(Σ~, C) である。Functor(Σ~, C)は自然変換を射とする圏だと考える。これで、モデル圏の圏論的（関手的）な定式化はできる。

Xを勝手な有限（に限る？）集合として、s:X→Σ_Sがあるとき、ソート付き変数集合と呼ぶ。x∈Xに対して直積Πs(x)を作って、これを[X]とする。[X]からの射の全体と対象とする圏（カンマ圏だっけ？）を(Σ~↑[X])とする。項集合T_Σ(X)ってのは、(Σ~↑[X])に近いと思うのだが。項の構成にタプルまで入れれば、T_Σ(X) = (Σ~↑[X]) かな？ ここ、よくわからん。

話は変わって、S=Σ_Sとして、Sソート付き集合の圏Set_S上の項モナドT_ΣのKleisli圏の反対圏（opposite）をAss_Σと書いて代入系の圏と呼ぶ。Model(Σ;C)、つまりFunctor(Σ~, C)から、Functor(Ass_Σ, C)への関手が自然に定まる。その手順：

1. ΣのCモデルMを決める。
2. ψ∈T_Σ(X) に対して、【ψ】=f:[X]→B in C が決まる。
3. Kleisli射 Ψ:Y→T_Σ(X) に対して、:[X]→[Y]が決まる。
4. これは、Kleisli圏からCへの反変関手である。

【ψ】の定義にはvaluationを使うが、valuationの全体が[X]である。valuationや【ψ】はわかるが、どうも背後にある全体的仕掛けがわからない。グギギギギ。