次の同型が成立する。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} }`$$`\prod_{i \in I} {\bf Set}[X, A[i] ] \cong {\bf Bun}[I](X \times I, \sum_I A[\bullet]) \\ \cong {\bf Fam}[I](\mrm{K}^X_I, A[\bullet]) `$名前だ…

まだユルユルな議論なのだが、コンテナの次元UPした概念である2-コンテナとインスティチューションを組み合わせてセオリー論を洗練させられる気がする。$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} }`$ コンテナ インスティ…

モットー writing is programming （writing as programming） documents should be formally verified ブリットとは： BLit = Web Literature Web上で利用できる、関連する文書達のアーカイブネットワーク マスブリットとは： MathBLit = Mathematics Web L…

「インスティチューション＋関手意味論」のフレームワーク、なんか名前を付けないと呼びようがない。そのまんまだけど、関手インスティチューションとか。関手インスティチューションの構成素は： 指標の圏、具体的に構成される 指標の圏のinclusive構造 代…

$`\newcommand{\Within}{\sqsubseteq} \newcommand{\conc}{\mathop{\#} } \newcommand{\dmid}{\mathrel{\|} } \newcommand{\mrm}[1]{\mathrm{#1} } %`$$`\mrm{Ext}(\Sigma)`$ は拡張指標（派生指標）の全体。すると、$`\quad \Gamma \in \mrm{Ext}(\Sigma) \…

$`\newcommand{\Within}{\sqsubseteq} \newcommand{\conc}{\mathop{\#} } \newcommand{\dmid}{\mathrel{\|} } \newcommand{\mrm}[1]{\mathrm{#1} } %`$ 証明の定式化が欠けている。→ πインスティチューション 非論理的指標部分と論理条件が分離されている。…

課題と参考文献： インスティチューションがうまく使えない - 檜山正幸のキマイラ飼育記 (はてなBlog) 2005年7月の疑問・課題 はじめての圏論 その第5歩：変換キューの圏 - 檜山正幸のキマイラ飼育記 (はてなBlog) はじめての圏論 第6歩：有限変換キューと半…

ドクトリンは、ドミニオンを支配〈ドミネイト〉する構造として存在する。“指標の圏”達のタワーをバックボーンタワー〈ユグドラシル〉と呼ぶ。ドミニオンの構成素： 自由忘却随伴系 ターゲット代数 上位レイヤーのドミニオンを次のように書く。 自由忘却随伴…

可換モナドとラックス・モノイド・モナド（動機も少し） - 檜山正幸のキマイラ飼育記 (はてなBlog) 指標の圏の上の構文モナドのクライスリ圏を考えるのが基本。だが、圏とその反対圏を同時に考えて、ストリング図を使うと混乱しがち。ストリング図の併置は直…

次の概念が識別されてないと曖昧模糊になる。 具象圏のベース圏 モデルの圏（関手圏）のターゲット圏〈モデルのアビタベース〉 関手インスティチューション〈functorial institution〉のアンビエント圏〈ターゲット圏のアビタ〉 相対モナド（言語モナド）の…

Σを指標として、Σはメタ指標Σ'の配下〈governed by〉にあるとする。Σで導入（新規に定義）された記号を使って書かれた構文的対象物〈syntactic object〉をΣ-項と呼ぶ。Σ-項は、ΣのΣ'による自由閉包〈free closure〉の要素になる。Σ-項に対する演算は、Σ'によ…

n-セオリーとインスティチューション - (保存用) 檜山正幸のキマイラ飼育記 メモ編に書いてあることが我ながら凄いな。なんで気付いたのだ？最近とは用語法・記法が違うので対応表。 過去 最近 Σk kΣ Ak kA k-Spef[-] (-)-kSig k-Mod[-] (-)-kAlg Ck なし Ck…

プログラムfを状態変換子とみたものを f*、プログラムfを述語換子とみたものを f* とすると： < x | f*(q)> = < f*(x) | q> が成立するのではないか、これはインスティチューションの充足関係 x |= f*(q) ⇔ f*(x) |= q と同じではないか。つまり、 状態変換…