左モノイダル閉圏

L-C-MC

signature.icon

code:L-C-MC.sig

sig L-C-MC C ⊗ i α λ ρ LExpsAdjs fixed-in CAT

MonoidalCategory C ⊗ i α λ ρ

Data

LExpAdjs : C -> Adjunction C C

= \a -> Adjunction C C (a⊗) (a⊸) a.unit a.eval

definition.icon

i.e.

任意の左からのモノイダル積$ a \otimes \_ が

dragoon8192.icon 指数函手を定義に直接つっこみたい

out-of.icon

左内部hom函手$ ⊸ \colon C^\mathrm{op}×C → C

code:sig

1-morph

(f⊸) : (a⊸) => (a⊸)

:= (a'⊸) * a.unit

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

; a'.unit * (a⊸)

単位

dragoon8192.iconそれぞれがAdjs : C -> Adjunction C Cの成分っぽい？

構造への射に一般化して考えたい

p-dual.icon