指数随伴系は自己函手圏における双対系
from モノイダル閉圏における指数随伴系の自然性
指数随伴系は自己函手圏における双対系
自己函手圏Cat &⟜ Catへの……なんだ？
強モノイダル圏
S-MonC (Cat⟜Cat) (*) Cat^
そもそもこいつが2-圏なら
2-函手を考えてないといけない？
code:なんだろな.sig
&1-morph
prod : Cat &-> (Cat &⟜ Cat)
hom : Cat^{op} &-> (Cat &⟜ Cat)
A.prod : Cat &-> Cat
&2-morph
A.prod&^ : A.prod &=> A.prod
F.prod : A.prod &=> A'.prod
F.hom : A'.hom &=> A.hom
A.unit : Cat^ &=> A.prod * A.hom
F.unit : Cat^ &=> A'.prod * A.hom
F.eval : A'.hom * A.prod &=> Cat^
函手の結合がモノイダル積として解釈されることに注意
code:自己函手圏.sig
‰ = S-MonC (%⟜%) (*)=(&1) Cat&^(@ ‰I)
‰0-morph
A.prod, A.hom
A'.prod * A.hom
‰1-morph
F.prod : A.prod ‰-> A'.prod
F.hom : A'.hom ‰-> A.hom
F.unit : ‰I ‰-> A'.prod * A.hom
F.eval : A'.hom * A.prod ‰-> ‰I
随伴系の話が双対系になってる……
code:dual.sig
Dual A.prod A.hom A.unit A.eval : in ‰
Adjunction Cat Cat A.prod A.hom A.unit A.eval