$`\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} } %`$ 証明の定式化が欠けている。→ πインスティチューション 非論理的指標部分と論理条件が分離されている。…

指標テレスコープがあるとする。$`\newcommand{\Within}{\sqsubseteq} \newcommand{\conc}{\mathop{\#} } \newcommand{\dmid}{\mathrel{\|} } %`$$`\quad \Sigma_1 \Within \Sigma_2 \Within \cdots \Within \Sigma_n`$それ自身が指標でなくても、なんらかの…

$`\newcommand{\mrm}[1]{ \mathrm{#1} }`$ 0-指標の場合は関数の定義 1-指標の場合は関手の定義 型理論： 証拠〈witness〉付き型判断（コンテキスト＝名前付き指標） 論理： 証明 プログラミング：ソフト実装、アダプター 手続きの域は指標だが、ソース・コ…

長さ1の指標テレスコープ$`\newcommand{\Within}{\sqsubseteq}`$ $`(\emptyset \Within S)`$ 指標の標準分解： 宣言の個数と同じ長さの指標テレスコープ 無法則パートと全体で長さ2の指標テレスコープ 任意の長さの自明テレスコープ 指標テレスコープの最初…

以前にも書いたが、包含的圏〈inclusive category〉は、 Composing Hidden Information Modules over Inclusive Institutions (2004) Joseph Goguen, Grigore Rosu 25p https://fsl.cs.illinois.edu/publications/goguen-rosu-2004-dahl.pdf 包含系は： Grot…