Lens
いわゆるgetter/setterの圏論による表現。
Associated (co)monad with an adjunction
Adjunctionからのmonad - PSより、adjunction:
について
はmonadに、
はcomonadになる。
EM category for a (co)monad
Eilenberg-Moore adjunction - PSより、monad:
について、-algebraをobjectとするcategoryを
と書くのであった。同様にして、comonad:
について、-coalgebraをobjectとするcategoryを
と書くことにする。
記法
以下、
- cartesian closed category:
- -object:
について・・・
View-operation adjunction
Slice category からのforgetful functor:
とfunctor:
について
Cartesian closure adjunction (Curry adjunction)
Curryingによるadjunctionのこと。
Costate(Store) comonad
上記のadjunctionからassociated comonad:
を作れる。
命題
Lens
上記の同値なEM category(のいずれか)のobjectをlens、morphismをlens morphismという。
Lens laws
- in
とすると、 の定義により
- (get-put law)
- (put-get law)
- (put-put law)
特に のとき、これらは
に対応する。*2