ドクトリンは、CCCのような、Cat上の具象圏だとする。ハイパードクトリンは拡張されたドクトリンくらいの意味だが、 ベース圏（論域の圏）の上のインデックス付き圏であり、余域はCCCのようなドクトリンになる。 ベース圏の射に対して、ΣΔΠ随伴性がある。Σは…

ハイパードクトリン インスティチューション ベース対象 型コンテキスト 指標 ベース射 コンテキスト拡張／置換 指標射 ファイバー 命題の圏 モデルの圏 誘導関手 引き戻し リダクト関手 随伴関手 限量子 - 妥当性 - 充足関係 こうして見ると、限量子随伴性…

カリー／ハワード対応を信じるなら、関数の記述と定理の証明はまったく同じはず。だったら同じ書き方ができるはず。 // f:X×Y→Z function f given x:X, y:Y ensures Z begin ... end // t:A∧B→C theorem t given a:A, b:B ensures C begin ... end関数定義に…

コマンドは、先頭が動詞原型または動詞過去分詞形、それに続いてキーワード目的語名詞が続いてもいい。apply, make conjunction, found inconsistency など。「命題 by 根拠名詞 引数並び」でも証明が書けるとする。以下、根拠名詞とコマンド動詞の対応表。 …

命題、証明、規則をそれぞれ0-射、1-射、2-射の意味で使う。 公理 公理証明 ax_A : * -> A * ----[ax A] AAx⊆|C| なので、Axは命題の集合として与えられるが、それはデカルト閉圏の特殊事情で、一般には、 a : X -> A X ---[a] Aつまり、Ax⊆Mor(C)。Axはどん…

A1, ..., Anを仮定（assume）してBを結論（conclude, entail, result, produce, show）する証明があるとき、その証明内で使っている暗黙の知識がある。これを証明の文脈とか環境と呼ぶ。で、文脈とは正確には何か？ が大問題。それと、トンネル論法（コンパ…

最初の案： 暫定版 証明図シリアル化構文 - 檜山正幸のキマイラ飼育記 メモ編 その後の変更： 証明図シリアル化構文 キーワードの現状 - 檜山正幸のキマイラ飼育記 メモ編 BLKと書いてあるのはブロック、そうでなければコマンド。 論理記号 導入 削除 ∧ make…

演繹付きインスティチューション〈institution with deduction〉を定義する。普通のインスティチューションに、指標Σごとの演繹性判断〈deducibility judgement〉|-Σが付いている。 |-Σは、Pow(Sen[Σ])とSen[Σ]のあいだの（二項）関係 演繹性判断は、次の公…

ER図不要論は、純粋リレーション主義者のプロパガンダ、ネガティブ・キャンペーンだ。まずは基本事項： 集合と要素 単元集合と終集合 写像 恒等写像と包含写像 終写像 単射と全射 集合の直積、2項直積とn項直積、要素のペアとタプル 多変数関数と直積からの…

制約の種類とスケッチの描き方 制約 スケッチの描き方 単射性 アロー先端に大なりマーカー 全射性 アロー根本に大なりマーカー 同時単射性 スパンのアロー（複数）に棒 コンポジション 三角形を水色で塗る 直積 三角形をピンクで塗る ファイバー積 四角形を…

ともかく用語がたくさんある。 表示（denotationやrepresentationじゃなくて、presentation） 生成系と関係 ： 古典的な用法、たぶん群表示が起源 生成系と等式系 ： 関係が等式のとき 生成系 ： 関係も生成系の一部と考える コンピュータッド ： 次元（次数…

コンピュータッドがモノイダルとは、各次元のセル（セルはコンピュータッドの要素）の集合に対してモノイド積を許すもの。0セルに対して厳密モノイド＝自由モノイドを作って、それを0-ダイアグラムとして使う。1-セルにも厳密モノイド積を入れて、1-コンピュ…

やはり次元概念が難しい。以前、幾何次元、グレード次元という言葉を使ったが、これはやめよう。射の次元を次数（degree）として、幾何次元を次元としている例がある。 セルは指標＝コンピュータッドの要素の意味で使う。幾何胞体とは異なる。幾何胞体は単純…

動詞squashiはペチャンコに潰すこと。ストリング図のキャンバスボックスを低次元のボックスに射影するとき、重なっているストラータムを低次元に押し込むときにスカッシングをする。スカッシングは、ファイバー方向に並んだストラータムを評価する。つまり、…

射、セル、ストラータムなどの次元を区別するために、 "Surface diagrams for gray-categories" by Hummon, Benjamin Taylor（ http://escholarship.org/uc/item/5b24s9cc, http://www.chimaira.org/archive/SufraceDiagramsForGrayCategories_eScholarship-…

タイリングの矩形タイルをブリック（レンガ）とかブロックとか呼ぶこともある。レゴブロックとか、ドミノ牌（牌はタイルの意味）とも言える。ブリック・コンストラクション・ゲームという言葉もあったな、そういえば。牌、タイル、ブリック、ブロックにはラ…

ダイアグラムはキャンバス空間内の模様だが、 キャンバス空間＝キャンバス矩形＝キャンバスボックス＝ボックス エクステント＝一般化ストリング＝ストラータム（stratum; 層素） 0-ストラータム＝ノード＝ドット＝点＝頂点 1-ストラータム＝シーム（縫い目）…

Globularのセルは、セル複体（胞複体）のセルとは全然違う。コンピュータッド理論の生成射（generating morphism）なのだと思う。高次圏の高次射をセルと言うが、これとも違う。任意の高次射がセル（生成高次射）なわけではない。n-セルとn-ダイアグラムの帰…

代数系の種類という意味でドクトリンを使うとして、ドクトリンの事例には次のようなものがある。 mon モノイド grp 群 cat 圏 mon-cat モノイド圏 symm-mon-cat 対称モノイド圏 br-mon-cat ブレイド付きモノイド圏 str-2-cat 厳密2-圏 これらのドクトリン（…

コンピュータッドは、言い換えれば多グラフだが、「形容詞「複」「多」と箙〈えびら〉 - 檜山正幸のキマイラ飼育記」に従えば、高次多箙（higher polyquiver）のことだ。1-quiver＝普通の有向グラフのときと同じに、生成形から自由生成できる。高次多箙の生…

昨日の 型クラスの比較 - 檜山正幸のキマイラ飼育記 メモ編 への補足説明。既存のものに後からゴチャゴチャ文句を言うのは簡単だ。だから文句言う。コアージョン（coercion - 檜山正幸のキマイラ飼育記 メモ編）は必要悪という意味で必須だから、使うのはい…

公理をひとつも持たないセオリーをダムセオリーと呼ぼう。日本語ではアホ理論。

表現と加群は同じことだが、それを考えるために： アンビエント・ドクトリン： 世界となる圏の圏、2-圏構造を使うこともある 単対象サブドクトリン：アンビエント・ドクトリンのなかで、単対象のものだけの集まり。圏になる。 表現サブドクトリン：表現の舞…

nLabのプロップの定義はなんか変だと思う。 http://ncatlab.org/nlab/show/PROP プロップやオペラッドの話だと、セオリーとモデル（代数＝加群＝表現）の混同がけっこうある。んで、スッキリしたプロップの定義がやっと見つかった。 Title: On the category …

ドクトリン http://ncatlab.org/nlab/show/doctrine オペラッドのドクトリン http://ncatlab.org/toddtrimble/published/Towards+a+doctrine+of+operads コスモス http://ncatlab.org/nlab/show/cosmos ユニヴァース http://ncatlab.org/nlab/show/universe …

C = V + H と直和分解されている圏が隠蔽指標。射を次のように呼ぶ。 dom(f) cod(f) fの呼び名 H H transition H V observer V H constructor V V calculation 通常、calculationはないとする。M:C→Set が集合論的なモデル。Vの要素（対象）だけで定義された…

Sをスキーマとか指標と呼ばれる圏（または圏の表示）として、型は関手圏 [S, C] の対象となる。Sが含まれる圏の圏（ドクトリン）をDとする。x:S→X in D が部分関手として、E:S→C も部分関手（部分的に定義された、Cに値を取る意味）として、この状況自体を λ…

ドクトリン、アンビエント圏、derivatorにより構成される構造をアプリケーション領域と呼ぶことにする。基本的なことは、次に書いてある。 一般関手モデル：インスティチューションとの関係 - 檜山正幸のキマイラ飼育記 D⊆Cat と、圏Presがあって、D(Cat(P),…

関手モデルでは、圏Sがデータベーススキーマで、関手 F:S→Partial がデータベースインスタンス。関手指向アプリケーションプランニングでは、圏Sがアプリケーションスキーマで、関手F:S→Partial がアプリケーションインスタンス。って何も差がない。そう、差…

アレ、アレレ？形式言語理論の言語は、列とかツリーとかグラフとかの集合だけど、結局は関手圏なのではないか。GとHがグラフのとき、GからHへのグラフ準同型の集合は、準同型を関手とみなしてよいので、関手圏 [G, H] となる。形式言語理論のたいていの問題…