Arrows in String diagrams

(･･･やっぱりつらいので左右逆にならないようにする)

以下、水平方向は考えないで、垂直方向のみ 1-category $\mathtt{Arrow} \mathcal{A}$ の composition $\mathtt{>>>}$ とする。

f:id:mbps:20151111015439p:plain

f:id:mbps:20151111015446p:plain

f:id:mbps:20151111015451p:plain

ただし、naturality は $\operatorname{ob} \mathcal{Hask} = \operatorname{ob} \mathcal{A}$ であることから次の functor により定義する。

$\mathcal{A}(\mathtt{-},\mathtt{+}) : \mathcal{Hask}^{\operatorname{op}} \mathtt{\times} \mathcal{Hask} \to \mathcal{Hask}$
$\mathcal{A}(f,g) := \operatorname{Hom} _ {\mathcal{A}} (\mathtt{arr}(f),\mathtt{arr}(g) )$

Free theorem なしでも、

$\mathtt{arr} : \mathtt{(}X \mathtt{\to} Y\mathtt{)} \to \mathcal{A}(X,Y)$ は、各変数について natural。
は、各変数について (extra)natural。
- $\langle \mathtt{first} \rangle : \mathcal{A}(X,Y) \to \prod _ W \mathcal{A}( \mathtt{(}X\mathtt{,} W\mathtt{)}, \mathtt{(}Y\mathtt{,} W\mathtt{)} )$ もそう。
- End bijection と同様に product bijection も naturality を preserve するので。

f:id:mbps:20151111061916p:plain

f:id:mbps:20151111061925p:plain

f:id:mbps:20151111045437p:plain

$\mathtt{second}$ についても $\mathtt{first}$ と同様の law が成立する。
$\mathtt{***}$ は associative。
は functorial とは限らない。
- $\mathcal{A}$ -morphism 同士を上下にスライドできない。(string 上を自由に移動できない)
- 交差点は移動可能。
- $\mathtt{arr}$ 以外の $\mathcal{A}$ -morphism は、各 y 座標に一個まで。
- string diagram と言いながら monoidal category にならない。*1
一方、各 $\mathtt{arr}$ は monoidal category であるかのように移動できる。

*1:premonoidal category というのになるらしい