https://m-hiyama-memo.hatenablog.com/entry/2022/01/18/191815

$\newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\In}{\text{ in } }$

指標の圏の上の構文モナドのクライスリ圏を考えるのが基本。だが、圏とその反対圏を同時に考えて、ストリング図を使うと混乱しがち。

ストリング図の併置は直和か直積を表すが、それは向き（反対圏かどうか）によって解釈が変わる。

Mが構文モナドのとき、

M-手続きは、クライスリ圏の反対圏の射
M-コードは、モナドの基礎圏のM-結果的射〈M-resultic morphism〉
M-手続きの圏は $\mathrm{Proc}(M/\mathcal{S}) := \mathrm{Kl}(M/\mathcal{S})^{\mathrm{op}}$

次が重要：

$\mrm{Proc}(M)$ の射 $p$ は対応するコード $p^\downarrow$ を持つ。コードはプログラミング言語によるソースコードだと思ってよい。
コードは $\cat{S}$ 内のM-結果的射である。
$\cat{S}$ は余デカルト圏である。
はデカルト圏である。
1. $\mrm{Proc}(M)$ は終対象 $\mrm{Void} = {\bf 0}^\mrm{op}$ を持つ。
2. $\mrm{Proc}(M)$ は直積 $\oplus$ を持つ。 $\mrm{Void}$ を単位対象とする対称モノイド積である。
3. $\mrm{Proc}(M)$ は対角 $\Delta_\Sigma$ を持つ。自然変換になる。
4. $\mrm{Proc}(M)$ は終射 $!_\Sigma$ を持つ。自然変換になる。

問題は、 $\mrm{Proc}(M)$ に対するトレースの定義だ。