状態遷移系に関する補足小ネタ その1：
「状態遷移系達の二重圏の直接的定義」において、状態遷移系をバンドルのあいだのレンズ射として定式化しました。状態遷移系（＝レンズ射）を図式に描くとき、野球のホームベース形に描くと具合がいいです。$`%\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\mrm}[1]{\mathrm{#1}}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\In}{\text{ in }}
%\newcommand{\twoto}{\Rightarrow }
%\newcommand{\op}{\mathrm{op} }
%\newcommand{\id}{\mathrm{id}}
%\newcommand{\u}[1]{\underline{#1}}
\newcommand{\o}[1]{\overline{#1}}
%\newcommand{\hyp}{ \text{－} }
%\newcommand{\Iff}{ \Leftrightarrow }
%\newcommand{\Imp}{ \Rightarrow }
%\newcommand{\base}[1]{ {{#1}\!\lrcorner} }
\newcommand{\Bun}[2]{ \begin{bmatrix} {#1}\\ \downarrow\\{#2}\end{bmatrix} }
%\newcommand{\BunM}[2]{ \begin{bmatrix} {#1}\\{}\\{#2}\end{bmatrix} }
%\newcommand{\BunF}[2]{ \begin{pmatrix} {#1}\\{}\\{#2}\end{pmatrix} }
\newcommand{\LensM}[2]{ \begin{pmatrix} {#1}\\{\leftarrow}\\{#2}\end{pmatrix} }
`$
次の状態遷移系を考えます。
$`\quad f = \LensM{f^\sharp}{f} : \Bun{\o{\alpha}}{A}\to \Bun{\o{\beta}}{B} \In \mbf{Lens}`$
状態遷移系とそのベースパートは記号の乱用で同じ名前にします。この状態遷移系を表わす図式は以下のように描きます。
$`\quad \xymatrix{
{}
&{f^*\o{\beta} } \ar[dl]_{f^\sharp} \ar[dr]^{f^\uparrow} \ar[ddl]
\ar@{}[dd]|{\text{p.b.}}
&{}
\\
{\o{\alpha} } \ar[d]
&{}
&{\o{\beta}} \ar[d]
\\
A \ar[rr]_f
&{}
&B
}\\
\quad \text{commutative }\In \mbf{Set}
`$
ラベルがない矢印はバンドルです。
もうひとつの状態遷移系を $`g`$ とします。
$`\quad g = \LensM{g^\sharp}{g} : \Bun{\o{\beta}}{B}\to \Bun{\o{\gamma}}{C} \In \mbf{Lens}`$
ホームベース形描画のメリットは、レンズ射達のレンズ結合がうまく描けることです。
$`\quad \xymatrix{
{}
&{}
&{f^{\uparrow *}(g^*\o{\gamma}) }\ar[dl]_{f^{\uparrow *}g^\sharp }
\ar[dr]^{f^{\uparrow \uparrow}}
\ar@{}[dd]|{\text{p.b.}}
&{}
&{}
\\
{}
&{f^*\o{\beta}} \ar[dl]_{f^\sharp}\ar[dr]^{f^\uparrow}\ar[ddl]
\ar@{}[dd]|{\text{p.b.}}
&{}
&{g^*\o{\gamma}} \ar[dl]_{g^\sharp}\ar[dr]^{g^\uparrow}\ar[ddl]
\ar@{}[dd]|{\text{p.b.}}
&{}
\\
{\o{\alpha}} \ar[d]
&{}
&{\o{\beta}} \ar[d]
&{}
&{\o{\gamma}} \ar[d]
\\
{A} \ar[rr]_f
&{}
&{B} \ar[rr]_g
&{}
&{C}
}\\
\quad \text{commutative }\In \mbf{Set}
`$
外側の大きなホームベース形が、レンズ結合 $`f;g`$ の図式になります。
$`\quad \xymatrix{
{}
&{}
&{f^{\uparrow *}(g^*\o{\gamma}) }\ar[dl]_{f^{\uparrow *}g^\sharp }
\ar[dr]^{f^{\uparrow \uparrow}}
\ar[dddll]
\ar@{}[ddd]|{\text{p.b.}}
&{}
&{}
\\
{}
&{f^*\o{\beta}} \ar[dl]_{f^\sharp}
&{}
&{g^*\o{\gamma}} \ar[dr]^{g^\uparrow}
&{}
\\
{\o{\alpha}} \ar[d]
&{}
&{}
&{}
&{\o{\gamma}} \ar[d]
\\
{A} \ar[rr]_f
&{}
&{B} \ar[rr]_g
&{}
&{C}
}\\
\quad \text{commutative }\In \mbf{Set}
`$
$`f^{\uparrow\uparrow};g^{\uparrow} = (f;g)^{\uparrow}`$ と $`f^{\uparrow *}(g^*\o{\gamma}) = (f;g)^*\o{\gamma}`$ を使うと、次のコンパクトな図式になります。
$`\quad \xymatrix{
{}
&{(f;g)^*\o{\gamma} } \ar[dl]_-{(f^{\uparrow *}g^\sharp)\, ; f^\sharp}
\ar[dr]^{(f;g)^\uparrow} \ar[ddl]
\ar@{}[dd]|{\text{p.b.}}
&{}
\\
{\o{\alpha} } \ar[d]
&{}
&{\o{\gamma}} \ar[d]
\\
A \ar[rr]_{f;g}
&{}
&C
}\\
\quad \text{commutative }\In \mbf{Set}
`$
この方法で図式を描けば、レンズ結合の結合律や単位律も、ファイバー積の性質（「ん？ ファイバー積はそれほど簡単じゃないよ」参照）から導けることが分かります。
