圏論内で使う等式的推論を、圏論のなかで定式化してみます。等式的推論は高次射になるので、少しだけ高次圏論を使います。内容： 等式的推論 高次圏 高次圏における結合 結合の演算子記号 恒等射 2-圏の3-射、4-射 恒等射だけの圏 恒等射の計算と等式的推論 …

「米田テンソル計算 3： 米田の「よ」、米田の星、ディラックのブラケット 再論」にて： 圏の対象・射の{余}?米田埋め込みと関手・自然変換の{余}?米田埋め込みの両方に米田の星を使ってますが、これはオーバーロードです。両者はすこし別な対応です。僕は、…

「自然変換の集合のエンド表示」で、自然変換の集合がエンドで表現できることを示しました。投稿の時間順序は前後してますが、必要な基本事項を「ホム関手とサンドイッチ結合」で解説しています。また、「米田テンソル計算 3： 米田の「よ」、米田の星、ディ…

ホム関手は非常に基本的かつ初等的な概念です。初等的なゆえにむしろ、シッカリと語られなかったり、ボンヤリした理解のまま先に進んでしまったりがアリガチかも知れません。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\id}{\mathrm{id} } \newcomma…

昨日の「有法則代数と無法則代数」から連想した小ネタ。 昨日の話 （記号の乱用）を圏 上のモナドとします。このモナドのクライスリ圏とアイレンベルク／ムーア圏は次のように書くことが多いです（僕だけでなく世間的に）。 クライスリ圏： アイレンベルク／…

「圏論的レンズ 最初の一歩： ストリング図を中心に」において、レンズには有法則レンズ〈lawful lens〉と無法則レンズ〈lawless lens〉があると書きました。「有法則／無法則」という形容詞を使うのは初めて見ました（レンズ以外で見たことがなかった）。こ…

昨日の記事で話題にした長／ジェイコブス論文の Proposition 3.10 （p.11）のそば（p.10）に次の絵（描画方向は ↑→）があります。 これを見ると、次のように思えます。 integration は同時化： disintegration はベイズ反転： 実際、integration ＝ 同時化、…

表題の事実は、長／ジェイコブスの以下の論文の p.11 Proposition 3.10 として記述されています。 Title: Disintegration and Bayesian Inversion via String Diagrams Authors: Kenta Cho, Bart Jacobs Submitted: 29 Aug 2017 (v1), 8 Feb 2019 (v3) Pages…

デカルト閉圏では、単純型理論とラムダ計算が気持ちよく出来ます。が、実用上、もう少し広い範囲の型 -- 依存型と再帰的型も扱えたほうがいいですね。依存型と再帰的型も扱えて、手で触れる感じ（あくまで“感じ”）の圏を考えましょう。内容： 実用上必要そう…

記法をどう取り決めるか？ どうでもよさそうでも深刻に悩んでしまうのですよね。悩んだ経緯も含めて、現時点での約束ごとを記しておきます。表題に挙げた 米田の「よ」、米田の星、ディラックのブラケット の概念と記法について述べます。$` \newcommand{\Co…

Haskell風構文の擬似コードで記述された概念をデカルト閉圏で解釈してみます。翻訳の過程でけっこうな“忖度”が要求されます。内容： 理想化Haskell デカルト閉圏に対する直訳 忖度翻訳 関連する記事： Haskellの二重コロン「::」とバインド記号「>>=」の説明…

オプティックは双方向データ変換の技法ですが、抽象的定式化の枠組みとしては丹原／ペイストロ*1／ストリート理論〈Tambara-Pastro-Street theory〉が使われているようです。なので、オプティックのための丹原／ペイストロ／ストリート理論の枠組みについて…