随伴系のなす圏

signature.icon

code:AdjMorph.sig

2-signature AdjMorph in Cat

1-morph

c→ : c -> c'

d→ : d -> d'

2-morph

l→ : l * d→ => c→ * l'

: c -> d'

r→ : r * c→ => d→ * r'

: d -> c'

3-eq

η→ : η * c→; l * r→; l→ * r'

=3= c→ * η'

: c→ => c→ * L' * R'

: c -> c'

ε→ : ε * d→

=3= r * l→; r→ * l'; d→ * ε'

: R * L * d→ => d→

: d -> d'

definition.icon

対象

$ \left\lang \mathrm{Adj}\colon C,D;L,R;η,ε \right\rang

where

$ C,D \colon \mathbf{Cat}

$ L: C→D

$ R\colon D→C

$ η\colon C^\wedge ⇒ L*R

$ ε\colon R*L ⇒ D^\wedge

射

https://gyazo.com/f88b66fe302519b940f33bd2dba95e2f

https://gyazo.com/8dfa23023b29dfbbeca899adb67a4add