…反変関手と、2-圏のストリング図 // 反変関手」参照）と $`よ`$ は同一視することにして、いちいちチルダを乗せるのはやめます。また、記法をスッキリさせるために、次のように約束します。（$`\YY`$ も米田〈Yoneda〉から。） $`{^\cat{C}\YY}(\hyp, \hyp) := \cat{C}^\wedge(よ^\hyp, \hyp) : \cat{C}^\op \times \cat{C}^\wedge \to {\bf Set}`$ $`{^\cat{…

…） 三番目の用法は、ストリング図において次の形で多用されます。（例えば、「絵算をはじめた人への注意」参照。）$`\quad \xymatrix{ A \ar@{-}[d] & F \ar@{-}[d] \\ (f) \ar[d] & (\alpha) \ar[d] \\ B & G }\\ f.\alpha : A.F \to B.G `$ストリング図内で、エレベーター法則でノードを上下スライドさせてもいいことは、等式（ストリング図書き換え）としての $`f.\alpha`$…

…ょう。「米田の補題とストリング図」で述べた手法が使えます。 このテの計算に絵算は使えるし、実際に僕は絵算を使っています。テキストで記述・計算するより、ずっと見通しがいいと思います。が、ややこしい問題もあります。ストリング図のワイヤーに向きを付けるとき、どんな約束にするか？ -- これ、ややこしい。通常は、キャンバスの描画方向を決めておくだけでいいのですが、反対圏／反変関手が出てくると、状況は単純ではなくなります。$`\newcommand{\cat}[1]{\mathcal{…

…に混乱します。「層化ストリング図 // 裏返し反変関手」で導入した裏返し反変関手〈reversing contravariant functor〉を使って説明します。関手 $`F`$ が共変関手、$`G`$ が反変関手であることを次のように表すことにします。$`\quad F:\cat{C} \to \cat{D} \text{ (covar)} \In {\bf CAT}\\ \quad G:\cat{C} \to \cat{D} \text{ (contravar)} \…

…で紹介しています。 ストリング図とストリンググラフ、何が違う？ 上記過去記事に幾つかの参考文献を挙げていますが、ひとつだけ引用すると： [KMS12-14] Title: Pattern graph rewrite systems Authors: Aleks Kissinger, Alex Merry, Matvey Soloviev Submitted: 30 Apr 2012 (v1), 1 Apr 2014 (v3) Pages: 13p URL: http://ar…

…味があれば： 絵算（ストリング図）における池袋駅問題の真相 双対や随伴に強くなるためのトレーニング 対称モノイド圏 $`\cat{C}`$ がダガー $`(\hyp)^\dagger`$ を持つとき、次の条件を加えると、ダガー特殊可換フロベニウス代数〈dagger special commutative Frobenius algebra〉の公理になります。$`\quad \Delta^\dagger = \nabla\\ \quad \bot^\dagger = \top …

…を粗視化して眺めたいときです。具体的な詳細や一部の構造を捨ててしまえば、演繹系の枠組みで捉えられることは多いでしょう。 *1:生成系がやせていても、それから生成された複圏〈オペラッド〉がやせている（複ホムセットが単元集合か空集合）とは限りません。 *2:この条件は、スパンに対する jointly monic 条件です。 *3:証明ツリーは、有向辺が項でラベルされ、頂点〈ノード〉がステップでラベルされたツリーです。このツリーは、オペラッドのストリング図をみなすのがよいでしょう。

…の補題「米田の補題とストリング図」の最後のほうで、「米田の補題の補題」として次の絵図等式〈{graphical | pictorial} equation〉を挙げました。この絵で： ワイヤーの方向はどこでも上から下 '☆' は、単一対象と恒等射だけの自明な圏 斜線網掛けは、集合圏 $`{\bf Set}`$ 点線は、単元集合（集合圏の終対象） $`{\bf 1}`$ のポインティング関手 $`\quad {\bf 1}^\sim : ☆ \to {\bf Set} \In {…

「層化ストリング図」では、"layer"を「層」としたのですが、「層」は"sheaf"の翻訳語であり、トラブルの原因になりそうなので「層」から「レイヤー」に変更します。ただし、過去の記事は変更しません*1。で、レイヤー化ストリング図〈layered string diagram〉ですが、これは余インデックス付き圏／インデックス付き圏のトータル圏（「最近の型理論： 拡張包括構造を持ったインデックス付き圏」の最初の節参照）の対象・射・等式の描画に有効です。この記事で描画法をもう少…

…た〈layered〉ストリング図が有効に使えるよ、ってことが、この論文の眼目です。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\twoto}{\Rightarrow} \newcommand{\hyp}{\text{－}} \newcommand{\In}{\text{ in }} `$内容： 裏返し反変関手 余インデックス付き対称厳密モノイド圏 層化プロ…

…同型”を作る作業は、ストリング図と相性がいいので、（ストリング図を使うなら）比較的簡単です。この記事でやってみます。“自然なホムセット同型”から“単位と余単位を含む代数系”を作るほうは、（僕は）うまくストリング図が描けなくて毎回行き詰まります。なので、やりません（うまくいったら報告するかも）。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\twoto}{\R…

…行すれば分かります。ストリング図を使って計算するのがオススメです。結局、$`\cat{E}, w \mapsto \cat{E}_{(w\land)}`$ という構成は、デカルト圏からデカルト圏を作り出します。$`\psi :v \to w \In \cat{E}`$ があると、デカルト圏のあいだの関手*2 $`\cat{E}_{(w\land)} \to \cat{E}_{(v\land)}`$ を構成できます。全体として次のような関手（インデックス付き圏）になります。$`…

…倒な作業になります。ストリング図で記述すれば直感的なんだけどね（「証明と計算は同じこと： 形式証明におけるノードとコネクター」参照）。プログラミング言語（のソースコード）はテキストで書くので、多値関数の記述は面倒で難しくなります。（おそらく）そのため、プログラミング言語では多値関数は人気がありません。しかし、形式証明の記述では、多圏の多射を使うほうが自然で分かりやすい記述ができます。関連する記事： 多値関数関連：自家製まとめリンク集 自然演繹はちっとも自然じゃない -- 圏論…

…圏・多圏 形式証明のストリング図 変数名・ラベルの利用 ラベル利用の事例 ノードとコネクター 追記・補足の記事： 自然言語混じり形式証明の意味論 シリーズ・ハブ記事： チャットAIで形式証明も自然言語混じりで書ける（はず） カリー／ハワード／ランベック対応と複圏・多圏我々がバックボーンとする考え方はカリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉です。つまり、型付きラムダ計算と論理とモノイド閉圏（特にデカルト閉圏）は同じ…

…れるとは思えません。ストリング図の、満足すべき自動レイアウト・アルゴリズムは存在しないようです（僕が知らないだけかも知れませんが）。自然言語混じり形式言語をソース言語として採用できれば、それはブレークスルーとなるでしょう。自然言語混じり形式言語からの多方向翻訳により、色々な目的に沿った記述・表現形式が得られますから。シリーズ・ハブ記事： チャットAIで形式証明も自然言語混じりで書ける（はず） *1:Legoという証明支援系の証明項〈証明オブジェクト〉です。出典である論文は、現…

…です。今の証明は次のストリング図で表現できます*2。水色のノードの意味は次のとおりです。 copy : (P, Q) → (P, Q), (P, Q) -- ワイヤーの束のコピー、2本から4本に proj1 : (P, Q) → P -- 左のワイヤーだけを取る（右のワイヤーを切り落とす）第一射影 swap : (P, Q) → (Q, P) -- 左右のワイヤーを入れ替えるスワップ AND : (Q, P) → Q∧P -- 論理AND導入 AND : (P, Q∧P) →…

…をワイヤーで表現したストリング図を描くのもオススメです。型を丁寧に明示した書き方は：$`\quad \big\langle x\in A, y\in B \mapsto f(x, y) \in C\big\rangle\\ = \big\langle x\in A, y\in B \mapsto \lambda\,t\in B.f(x, t)\;y \in C\big\rangle\\ \quad : A\times B \to C \In {\bf Set} `$上の等式の…

…〉の対象の集合です。ストリング図のワイヤーの端点のラベルが変数だという絵図的解釈もあります。まー、細かいことはともかく、変数を含んだ型判断も圏論的に解釈できるってことです。さて、次のような場合はどうしましょう。$`\quad g := (x : X, y : Y \vdash \tau : Z) \In \cat{C}`$圏 $`\cat{C}`$ が直積を持つなら、$`g:X\times Y \to Z \In \cat{C}`$ を、項 $`\tau`$ で定義していると…

… の対象・射を普通のストリング図として描いて、関手 $`F`$ を表すボックスまたはストライプ〈シース | sheath〉で包む、という描き方が関手ボックス／ストライプ図です。圏論的な絵図を描くソフトウェアがあるとしたら、ワイヤーやノードをクリックするとボックスになったり、あるいはストライプに変形するようなUIが備わるでしょう。実体が変化するのではなくて、描き方／表示方法が変わるだけです。圏論的な絵図を描いたり操作できる対話的ソフトウェアがあるといいのですが、残念ながら存在し…

…の使用法 域と余域 ストリング図 ペースティング図（タイル）二重圏のひとつの2-射を表すペースティング図〈タイル〉は次のように描くことにします。 射の描画方向： 縦方向、上から下 プロ射の描画方向： 横方向、左から右 プロ射の矢印には、何か印を付けることにします。上の図では矢印に垂直な棒ですが、TeXで書くときに一番簡単なのは、$`X_1 \not\to Y_1`$ です。TeXコードで \not\to と書いています。可換図式を描く AMScd パッケージ／拡張などでは、矢…

…、ペースティング図かストリング図かにより（描画法により）縦・横が変わります。混乱を避けるために、縦・横で形容しない呼び名にしましょう。 圏 $`\cat{D}_0`$ の対象： 0階の対象 ＝ 対象 圏 $`\cat{D}_0`$ の射： 0階の射 ＝ 射 圏 $`\cat{D}_0`$ の結合： 0階の結合 ＝ 射の結合 圏 $`\cat{D}_0`$ の恒等： 0階の恒等 ＝ 恒等射 圏 $`\cat{D}_1`$ の対象： 1階の対象 ＝ プロ射 圏 $`\cat{D}…

…くペースティング図とストリング図を紹介しました。ストリング図では、縦方向ワイヤーは上から下、横方向ワイヤーは左から右で、常識的な書字方向に一致していて「あー、気持ちいい」「これが落ち着く」と思っていました。しかし、次のような描画法を見かけました。あれっ、横方向ワイヤーが右から左。ンー ‥‥ いや待て、こっちのほうが合理的か。左側にあるペースティング図の横方向矢印を時計回りに90度回転すると上から下になります。同様に、縦方向矢印を時計回りに90度回転すれば右から左です！ もし、…

…はペースティング図（ストリング図ではない）における描画方向です。 射の種類 パレ nLab この記事 0-射 ラテン大文字 ラテン小文字（後方） (不要) 1-射 ラテン小文字 → ラテン小文字 → ギリシャ大文字 ↓ 内部1-射 ラテン小文字（後方）↓ ギリシャ小文字 ↓ ラテン大文字 → 2-射 ギリシャ小文字 ↓ ギリシャ小文字（後方）↓ ギリシャ小文字 → パレの図： nLabの図： シュルマン〈Mike Shulman〉も、パレ／nLabと同じ描画方向を使っています…

…らを先に説明します。ストリング図で描けば、4本脚のノードを、縦方向の射とみなすか横方向の射とみなすかにより、$`\cat{C}`$ の射から $`\cat{G}`$ の射への変換を定義します。ただし、縦と横の選び方は恣意的です。次は白旗論文からの絵です。アブラムスキーの絵を時計回りに90度回転した反時計回りに90度回転してからモノイド積の方向も変更したレイアウトになっているので、「縦」と「横」の意味は変わってしまいます。いずれにしても、以下のような対応を考えます。 $`A^+…

…io Roman〉のストリング図は確かに便利ですが、大規模高次な代数系を直接的に表現する記法・描画法が欲しいところです。 ヘッジーズ／ロマン〈Jules Hedges, Mario Roman〉のテレオロジー圏に対して直截的で正確な記述を試みてみましょう。テレオロジー圏を大規模高次な代数系〈large-sized higher algebra〉と捉えて定式化します。台〈underlying stuff〉となるコンストラクタ系（「コンストラクタ系と変換手性」参照）に対して、自然…

…io Roman〉のストリング図は確かに便利ですが、大規模高次な代数系を直接的に表現する記法・描画法が欲しいところです。 関手性や自然性を持たたい対応／変換を使うことになりますね。この話題はn回目。$`\newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\op}{\mathrm{op}} \newcommand{\id}{\mathrm{id}} \newcomm…

…ぇ。通常使われているストリング図表現では、$`\lact, \lact', \odot`$ の関係がうまく処理されるように工夫されています。自然性としてのタイトニングテレオロジー圏の $`\varepsilon^M_{[-, -]}`$ は次のような射の族になります。$`\quad \varepsilon^M_{[-, -]} : \J(M\odot [-, -]) \to \J([-, -]) \In \cat{T}`$以下の可換図式（を含む命題）が成立するなら、$`\va…

…ンズ 最初の一歩： ストリング図を中心に 以下の記号は「圏論的レンズ 4： テレオロジー圏」と同じ意味で使います。 対称モノイド圏 $`\cat{M}=(\cat{M},\otimes,I,\alpha,\lambda,\rho, \sigma)`$ （記号の乱用） 圏 $`\cat{C}`$ 左モノイド作用 $`(\lact) : \cat{M}\times \cat{C} \to \cat{C}`$ 圏 $`\cat{T}`$ 埋め込み関手 $`\iota`$ は考えずに…

…のようなものです。 ストリング図のテキスト化： ボックス＆ポート方式 モノイド圏上のテンプレート・オペラッド：具体例とソフトウェア的解釈 内容： ワイヤリング図とポート ケリー／マックレーン・グラフ ワイヤリング図からケリー／マックレーン・グラフへ 極性付き集合 ワイヤリング関数 ワイヤリング図とポート次の図は、スピヴァック〈David I. Spivak〉のスライド "Wiring diagrams and state machines" からコピーしたものです。これは、簡…

…の出力を持つ。 射をストリング図で表すとき、入力は上側のワイヤー、出力を下側のワイヤーとして描くことにします。n入力-m出力の多圏の射は次のように描きます。多圏の射は多射〈polymorphism | polyarrow〉と呼びます。（絵で描くと）入力のワイヤーがn本、出力のワイヤーがm本である多射を (n→m)-多射〈(n→m)-{polymorphism | polyarrow〉と呼ぶことにします。かつて僕は、(n→m)-多射を描いた図をスパイダーと呼んでいました。が、用…