ニョロニョロからホムセット同型

あ、そうそう。Globularの物凄くイライラするところ - 檜山正幸のキマイラ飼育記 メモ編 -- なんでそう思ったかを書く。

ニョロニョロ関係があるとき、ホムセットの同型としての随伴が出る。それを証明する。n-セルであることを :n で示す。-[-]- はペースティング、^はbump-up、~はinvertible。ニョロニョロ構造は、次のとおり。

1. A, B :0
2. F:1 A -> B
3. G:1 B -> A
4. η:2 A^ -> F[B]G :1 A -> A
5. ε:2 G[A]F -> B^ :1 B -> B
6. SNAKE-1:3 η[G]ε ~-> F^ :2 F -> F :1 A -> B
7. SNAKE-2:3 η[F]ε ~-> G^ :2 G -> G :1 B -> A

B(x.F, b)A(x, b.G) を示すために：

1. *:0
2. x:1 * -> A
3. b:1 * -> B
4. g:2 x.F -> b
5. f:2 x -> b.G

とする。g-mateとg-mate-mateを定義する。

1. g-mate :2 x -> b.G
2. g-mate-mate :2 x.F -> b

ニョロニョロ関係式を利用してgとg-mate-mateが等しいことを証明する。

---

といった手順を、なんで手でメモっておかなくてはならないのだ!? というのが不満。いくつかの対処があるとは思うのだが、考えがまとまらない。