モノイド 自己関手 モナド 自己関手のランベック代数 モナドのアイレンベルク／ムーア代数 付点自己関手 付点自己関手の“代数” 自己関手対の分配系 モナド対の分配系 自己関手対の分配系の“代数” モナド対の分配系の“代数”

米田埋め込み的なもの 米田単元埋め込み $`a \mapsto \{a\}`$ 米田クロネッカー・デルタ $`a\mapsto \delta^a`$ 米田CPS変換 $`f \mapsto f^*`$ 米田ケーリー表現／米田ケーリー加群 米田エルブラン・モデル 淡中埋め込み的なもの 淡中単項フィルター 淡中ゲ…

モノイド指標 Σ Σの圏Cでの付値モデル〈valuation model〉をΣ-代数と呼ぶ。Σ-Alg(C) := MonSIG(Σ, UC) ある種の忘却関手 MonCAT → MonSIG が必要。 モノイド指標はコンピュータッドの一種 Σ-代数装備は、圏Cの対象の弱モノイドからΣ-Alg(C)の対象の弱モノイ…

ファミリーの圏 $`{\bf Fam}[A]`$ は前層圏 順序集合に対するフィルター付き集合 $`\mathrm{FilteredSet}(A)`$ は前層圏 シェープ付き集合の圏 単体集合の圏： $`s{\bf Set}`$ 球体集合の圏： $`g{\bf Set}`$ 方体集合の圏： $`c{\bf Set}`$ 有向グラフの圏 …

$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\hyp}{ \text{-} } `$$`\mrm{K}^X_I`$ を $`I`$ 上の定数ファミリーとして、$`A`$ を任意のファミリーとする。ファミリーの射$`\quad \mrm{K}^X_I \to A \text{ on }I`$は、グロタンディーク同型により次…

eviは証拠〈evidence〉の略記だとする。命題と証明の圏 $`{\bf Ded}`$ から集合圏への関手が定義できる。 $`P\in |{\bf Ded}| \mapsto \mathrm{evi}(P) := {\bf Ded}(\top, P)`$ $`(f:P \to Q) \text{ in }{\bf Ded} \mapsto \mathrm{evi}(f) := {\bf Ded}(\…

依存型に一般化したカリー同型：$`\newcommand{\cat}[1]{ \mathcal{#1} } \newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\In}{ \text{ in } } `$$`\quad \cat{C} \in |{\bf Cat}|\\ \quad A:I \to |\cat{C}|_0 \In {\bf Set}\\ \quad \prod_{i\in I} \ca…

次の同型が成立する。$`\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} }`$ コンテナ インスティ…

この論文、参考になる。 https://kwarc.info/people/frabe/Research/KRW_isabelle_19.pdf Making Isabelle Content Accessible in Knowledge Representation Formats Michael Kohlhase, Florian Rabe, Makarius Wenzel 日付はハッキリしないが、2020以降なの…

型と計算 命題と証明 型演算／構成子 命題結合子 依存型構成子 限量子 型ファミリー (命題ファミリー) インデックス域 論域 インデックス 個体 インデックス変数 限量束縛変数 関数 保証 戻り型 結論命題 ターゲット型 ターゲット命題（質問の） 引数リスト …

Coqの宇宙は {Set, Prop} → Type → Type → ... Leanの宇宙は Prop → Type → Type → ...Typeには番号が付く。別にどっちでもいい。圏論的には次の圏を準備する。$`\newcommand{\mrm}[1]{\mathrm{#1}} `$ $`{\bf Ded}`$ $`{\bf Set}`$ $`{\bf SET}`$ $`{\bf CA…

自然数集合から可換モノイドへのインスタンスメーカーが3つあって、 足し算 掛け算 最大値（小さくないほう） 最小公倍数 それとは別に、ベキ等可換モノイド（演算記号 ◇）をジョイン（演算記号 ∨）半束にするインスタンスメーカーがあるとする。インスタン…

対応表： 定理記述 関数定義 定理のステートメント 関数{定義}?のヘッド 証明項 計算項 定理記述する 関数定義する から導出された定理 から定義された定理 構文と意味は混同される。 関数そのもの（型の圏の射）と関数定義という構文対象 定理そのもの（命…

まだ未整理だが、とりあえず備忘メモ。まず、対称性がある操作達。 無制限タプル構成 無制限コタプル構成（無制限タプル構成の双対） 有限タプル構成（無制限から制限） 有限コプル構成（有限タプル構成の双対） 依存カリー化 カリー化（依存カリー化の非依…

フォワード・リーズニング用に、ステージと同じコンビネータ・コマンドがある： 連言導入用コンビネータ： 既存のn個の証明から連言への証明を作る。 全称導入用コンビネータ： 既存のパラメータ付き証明から全称への証明を作る。 選言除去用コンビネータ： …

ステージ内に居るシーケントは： 事実シーケント 質問シーケント〈問題シーケント | ゴール〉 やること： 事実シーケントの構成（味方を増強する） 質問シーケントの分解（敵を衰弱させる／消滅させる） ステージの種類は： 連言導入用ステージ（連言成分〈…

コンテキストと指標は、構文的には区別できないのだが、次の違いがある。 指標はインスティチューション的な意味での指標である。 指標のあいだの射は指標射で、モデル圏のあいだのリダクト関手を定義する。 コンテキストは、固定した指標に対する構文的圏の…

宣言のみからなるテレスコープ〈依存レコード | 指標〉を純コンテキストと呼ぶことにする。宣言と割り当てが混じったコンテキストを混合コンテキストと呼ぶ。純コンテキスト〈指標〉のあいだの手続きは多型判断〈poly-typejudgement〉と言ってもよい。次が予…

参照可能性を確保するのが重要。それには次の行為が必要。 ラベリング： 外部から参照される項目〈アイテム〉に名前を付ける。 タギング： 外部から参照されるタグを付ける。タグは分類タグと話題タグ。 参照： 公開されている項目を参照する 参照マッピング…

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

MEDLアーティクルは抽象的な存在と言えるが、物理的バイト列としての支え〈サブストレート〉が必要。論理ユニットではなくて物理ユニットを識別する識別子について考える。特殊区切り文字に '@', '/', '|' を使う。名前内に区切り文字は使えない。 物理ユニ…

エージェントは次を持つ： 個体ID： 生成、消滅がある。 現在の状態： 状態は変化する ロケーション： ロケーションは変わるかも知れない 関与宣言 要求宣言 require {feature | associate } 提供宣言 provide feature エージェントは、いわゆるクラスのイン…

関与宣言は、ある主体が環境・組織体に入ったとき（所属したとき）、自分がどんな貢献〈contribution〉ができるか、貢献をするために、環境・組織・同僚〈associate〉に何を要求〈requirement〉するか？ を記述したもの。要求が満たされれば、記述した貢献を…

「インスティチューション＋関手意味論」のフレームワーク、なんか名前を付けないと呼びようがない。そのまんまだけど、関手インスティチューションとか。関手インスティチューションの構成素は： 指標の圏、具体的に構成される 指標の圏の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} } %`$ 証明の定式化が欠けている。→ πインスティチューション 非論理的指標部分と論理条件が分離されている。…

指標テレスコープがあるとする。$`\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の指標テレスコープ 任意の長さの自明テレスコープ 指標テレスコープの最初…