状態遷移系に関する補足小ネタ その2：
「状態遷移系達の二重圏の直接的定義」で定義したグロタンディーク・レンズの圏を $`\mathbf{Lens}`$ 、単純レンズ〈元祖レンズ〉の圏を $`\mathbf{SimpLens}`$ とします。$`\mathbf{SimpLens}`$ を $`\mathbf{Lens}`$ に埋め込む関手 $`\mathrm{USD}`$（UpSide Down）を構成します。$`%\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} }
\newcommand{\Pair}[2]{ \begin{bmatrix} {#1}\\ {#2}\end{bmatrix} }
\newcommand{\SLensM}[2]{ \begin{pmatrix} {#1}\\ {#2}\end{pmatrix} }
\newcommand{\USD}[1]{ {#1}^\updownarrow}
`$
単純レンズ〈元祖レンズ〉の圏 $`\mathbf{SimpLens}`$ の対象は、集合のペアだとします。つまり：
$`\quad |\mbf{SimpLens}| = |\mbf{Set}|\times |\mbf{Set}|`$
$`|\mbf{SimpLens}|`$ の要素を次の形に書きます。
$`\quad A = \Pair{A_+}{A_-}`$
$`\mbf{SimpLens}`$ の射、つまり元祖レンズは次のように書きます。
$`\quad f = \SLensM{f_+}{f^\sharp}\; : \Pair{A_+}{A_-} \to \Pair{B_+}{B_-}\In \mbf{SimpLens}`$
集合圏に展開して書けば：
$`\quad f_+ : A_+ \to B_+ \In \mbf{Set}\\
\quad f^\sharp : A_+ \times B_- \to A_- \In \mbf{Set}
`$
$`f_+`$ が順行パート〈forward part〉で、$`f^\sharp`$ が逆行パート〈backward part〉です。
グロタンディーク・レンズでは、順行パート〈ベースパート〉が下側で逆行パート〈逆行ファイバーパート〉を上側に書きました。記法の上下が逆です。
という事情で、$`\mathbf{SimpLens}`$ を $`\mathbf{Lens}`$ に埋め込む関手の名前は $`\mathrm{USD}`$（UpSide Down）にします。
$`\quad \mathrm{USD} : \mathbf{SimpLens}\to \mathbf{Lens}\In \mbf{CAT}`$
次の略記をします。
$`\quad \mathrm{USD}(\hyp) = \USD{\hyp}`$
$`\mathrm{USD}`$ の定義は以下のとおり。バンドル（の射影）はすべて直積の第一射影です。
$`\text{For }
\SLensM{f_+}{f^\sharp} : \Pair{A_+}{A_-} \to \Pair{B_+}{B_-}\In \mbf{SimpLens}\\
\quad \USD{\Pair{A_+}{A_-}} := \Bun{A_+\times A_-}{A_+}\\
\quad \USD{\Pair{B_+}{B_-}} := \Bun{B_+\times B_-}{B_+}\\
\quad
\USD{\SLensM{f_+}{f^\sharp} }:=
\LensM{f^\sharp}{f_+}\; :
\Bun{A_+\times A_-}{A_+} \to \Bun{B_+ \times B_-}{B_+}\In \mbf{Lens}
`$
集合圏に展開した図式は：
$`\quad \xymatrix{
{A_+\times A_-} \ar[d]
\ar@{}[dr]|{\text{comm.}}
&{A_+ \times B_-} \ar[l]_{\langle \pi_1, f^\sharp\rangle }
\ar[r]^{f_+\times \id_{B_-}} \ar[d]
\ar@{}[dr]|{\text{p.b.}}
&{B_+ \times B_-} \ar[d]
\\
{A_+} \ar@{=}[r]
&{A_+} \ar[r]_{f_+}
&{B_+}
}\\
\quad \In\mbf{Set}
`$
