圏論のお勉強なら、Catyスクリプトでやってミソ

ステファネスクに従って、用語法をデカルト分配圏からデカルト半環圏（cartesian semiringal category）に変える。

記号の説明：

• θ -- 空集合を域とする唯一の射
• ι -- 標準入射
• ∇ -- 直和のフォールド＝余対角
• λ -- 左unitor自然同型
• ρ -- 右unitor自然同型
• α -- associator自然同型
• プライム付き -- 直和に関するunitor, associator

デカルト半環圏	Catyスクリプト
1	null
!	void
<f, g>	[f, g]
π1	nth 1
π2	nth 2
f×g	[nth 1 | f, nth 2 | g]
Δ	[pass, pass]
λ	nth 2
λ-1	[null, pass]
ρ	nth 1
ρ-1	[pass, null]
α	[nth 1|nth 1, [nth 1|nth 2, nth 2]]
α-1	[[nth 1, nth 2|nth 1], nth 2|nth 2]
0	never
θ	許可しない*1
[f, g]	when {1=>f, 2=>g}
ι1	@1 pass
ι2	@2 pass
f + g	when{1=>@1 f, 2=>@2 g}
∇	when{1=>pass, 2=>pass}
λ'	pass
λ'-1	pass
ρ'	pass
ρ'-1	pass
α'	when{1=>when{1=>@1 pass, 2=>@2 @1 pass}, 2=>@2 @2 pass}
α'-1	when{1=>@1 @1 pass, 2=>when{1=>@1 @2 pass, 2=>@2 pass}}

肝腎の分配法則＝distributor自然同型が簡単には書けない。

• Catyとデカルト分配圏 - 檜山正幸のキマイラ飼育記 (はてなBlog)
• 分配法則を与える同型 - 檜山正幸のキマイラ飼育記 (はてなBlog)

本編ではオブジェクトを使っているが、配列を使うことにする。%は値変数、_は型変数を表す接頭辞として：

• val :: @%t _T -> _T
• tagged :: [string %t, _T] -> @%t _T

このような val, taggedを使えば：

• 左分配 δL [[nth 2 | when{1=>"1", 2=>"2"}], [nth 1, nth 2|val]] | tagged
• 左分配逆 when{1=>[nth 1, @1 nth 2], 2=>[nth 1, @2 nth 2]}
• 右分配 δR [[nth 1 | when{1=>"1", 2=>"2"}], [nth 1, nth 2|val]] | tagged
• 右分配逆 when{1=>[@1 nth 1, nth 2], 2=>[@2 nth 1, nth 2]}

パス式による分岐を with-when構文とすれば、

• 左分配 with $[1] when{1=>@1 [nth 1, nth 2|val], 2=>@2 [nth 1, nth 2|val]}

と短く書ける。実用上使う機会がどのくらいあるかは疑問だが、魅力的な構文だなー。

---

話が前後するが、デカルト半環圏の定義と記号法：

1. 終対象1と直積×を持つ。
2. 終対象への唯一射を ! とする。
3. デカルトペアリングを <-, -> とする。
4. 直積の射影をπ₁、π₂とする。
5. 直積を射に対しても拡張して二項関手とする。同じく(-)×(-) で表す。
6. Δは対角とする。
7. 直積に対する左単位律の自然同型をλとする。
8. 直積に対する右単位律の自然同型をρとする。
9. 直積に対する推移律の自然同型をαとする。

1. 始対象0と直和+を持つ。
2. 始対象から唯一射を θ とする。
3. 余デカルトペアリングを [-, -] とする。
4. 直和の入射をι₁、ι₂とする。
5. 直和を射に対しても拡張して二項関手とする。同じく(-)+(-) で表す。
6. ∇は余対角とする。
7. 直和に対する左単位律の自然同型をλ'とする。
8. 直和に対する右単位律の自然同型をρ'とする。
9. 直和に対する推移律の自然同型をα'とする。

1. 直積と直和の左分配律の自然同型をδLとする。
2. 直積と直和の右分配律の自然同型をδRとする。

それほど一般的な用語法ではないが：

• left unitor ： 左単位律を与える自然同型
• right unitor ： 右単位律を与える自然同型
• associator ： 推移律を与える自然同型
• left distributor ： 左分配律を与える自然同型
• right distributor ： 右分配律を与える自然同型

□は × か + のどちらかを表すとして：

• 左単位律 1□A ⇒ A
• 右単位律 A□1 ⇒ A
• 推移律 (A□B)□C ⇒ A□(B□C)
• 左分配律 A×(B + c) ⇒ A×B + A×C
• 右分配律 (A + B)×c ⇒ A×C + B×C

*1:when{} は構文エラー