指数単位律子

モノイダル圏における同型"x^1=x"

$ ν :i⊸\_ \cong \_

からそれぞれ構成できる

code:sig

&2-iso

ν : (i⊸) ~= C^

i.e.

&2-morph

ν : (i⊸) => C^

ν- : C^ => (i⊸)

&3-eq

ν = (i⊸) * λ- ; i.eval

ν- = i.unit ; λ * (i⊸)

where

MC C ⊗ i α λ ρ

Adjunction C C (i⊗) (i⊸) i.unit i.eval

$ :\_⟜i \cong \_