Globularのサンプルを追加しました。
このワークスペースの内容:
次の素材があって、
- 圏 C
- 圏 D
- 関手 F:C→D
- 関手 G:D→C
- 自然変換 η::IdC⇒F*G:C→C
- 自然変換 ε::G*F⇒IdD:D→D
ニョロニョロ関係式(snake relations)を満たすとき、x∈|C|, b∈|D| に対して、次の同型(双射)が作れます。
- D(F(x), b) C(x, G(b))
ただし、対象 x, b と射 f∈C(x, G(b)), g∈D(F(x), b) は、格上げして考えます。
要するに、関手の随伴対に対する「ニョロニョロによる定義」から「ホムセットの同型による定義」が導ける、ってことです。ほんとは、ホムセット同型の自然性も必要ですが、それはやってません。