内部homを用いた随伴系の自然同型

code:Adjunction.sig

signature Adjunction fixed-in Cat

Data

0-morph C, D

1-morph leftAdjoint @ L : C -> D

1-morph rightAdjoint @ R : D -> C

2-morph unit @ η

: C^ => L * R

: C -> C

2-morph counit @ ε

: R * L => D^

: D -> D

Axioms

3-eq snaky-1

: (η * L^); (L^ * ε) ≡> L^

3-eq snaky-2

: (R^ * η); (ε * R^) ≡> R^

code:sig

.0-morph in C

c,c',..

.1-morph

f : c .-> c',..

%0-morph in Cat

%I, C, D

%1-morph

L : C %-> D

R : D %-> C

c%~ : %I %-> C

d%~ : %I %-> D

c%~ %1 L = (c.L)%~

: %I %-> D

%2-morph

η : C^ %=> L %1 R

: C %-> C

ε : R %1 L %=> D^

: D %-> D

f%~ : c%~ %=> c'%~

f'%~ : c%~ %=> c"%~

f%~ %2 f'%~ = (f .1 f')%~

: c%~ %=> c"%~

: %I %-> C

f%~ %1 L = (f.L)%~

: (c.L)%~ %=> (c'.L)%~

: %I %-> D

where %1 = *

&0-morph in CAT

&I, Cat

&1-morph

(%I)&~, C&~, D&~#

: &I &-> Cat

&2-morph

d%~&~: (%I)&~ &=> D&~

c%~&~: (%I)&~ &=> C&~

C^&~ : C&~ &=> C&~

L&~ : C&~ &=> D&~

R&~ : D&~ &=> C&~

: &I &-> Cat

(L %1 R)&~ = L&~ &2 R&~

: C&~ &=> C&~

&3-morph?

η&~ : C^&~ &3> L&~ &2 R&~

: C&~ &=> C&~

: &I &-> Cat

表したいもの

$ \Phi \colon \hom_D(\_.L,\_) \Rightarrow \hom_C(\_,\_.R)

$ \colon C^\mathrm{op}× D \to \mathbf{Set}

code:sig

&2-morph

: &I &× &I &-> Cat

: &I &× &I &-> Cat

-- &I &× &I &~= &I

-- &I &-> Cat は大域要素

%1-morph

: C %-> D

∀ c : %I -> C

: [

∀ f : c * L => d

(f)(c.&Φ) : c => dR

∀ g : c -> c'