左内部hom函手の構成

code:sig

% = L-C-MC C ⊗ i α λ ρ Adjs

where

a.Adjs = Adjunction C C (a⊗) (a⊸) a.unit a.eval

モノイダル積の右カリー化

code:sig

2-morph

(f⊗) : (a⊗) => (a'⊗)

: C -> C

https://gyazo.com/d88768a9fde3035cf835cadd785877be

任意のaについての左指数函手は既に持っているので

code:sig

(a⊸) : C -> C

左内部hom函手の右カリー化を構成できる

dragoon8192.icon内部余米田埋込

code:sig

1-morph

(⊸)&∩ : C^op -> C &⟜ C

a.(⊸)&∩ : C -> C

:= (a⊸)

f.(⊸)&∩ = (f⊸) : (a⊸) => (a⊸)

:= (a'⊸) * a.unit

; (a'⊸) * (f⊗) * (a⊸)

; a'.eval * (a⊸)

https://gyazo.com/5240585d98e4807454118a841b058d68

これを反カリー化して