Monad algebra Coherence 参考文献 Comonadic Notions of Computation Eilenberg-Moore adjunction - PS

いわゆる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: につ…

Algebraically compact category 任意のendofunctorのinitial algebraとterminal coalgebraが存在し、互いにinverseとなるcategoryのこと。 等がそうらしい。 命題 endofunctor: initial algebra: terminal coalgebra: algebra: coalgebra: について なる -m…

命題 Initial algebraの族: について *1 なるfunctor: がただ一つ存在する。 証明 Fusion law vs. Parameterized algebra *2 参考文献 Theory and Practice of Fusion(pdf) *1:naturalityはevaluation functorによる *2:Initial algebras with parameters - …

命題 endofunctor: forgetful functor: について、initial algebra: が存在するならば、そのcatamorphimの族: は、mediatorを とする limiting cone of になる: (fold/build fusion) 参考文献 Initial algebra semantics is enough

命題 functor: initial algebraの族: について なるfunctor: がただ一つ存在する。 証明 参考文献 thesis.pdf

Endofunctor: について･･･ Lambek's lemma Every initial algebra is an isomorphism: *1 系 initial algebra: -morphism: *2 について なる -morphism: がただ一つ存在する。 参考文献 art08_geuvers_poll.pdf initial algebra of an endofunctor in nLab *…

複雑なGADTsはYoneda lemmaを使ってInductive family of types - PSにもっていける、ということらしい。 例 data Z data S n data IntList n where Nil :: IntList Z Cons :: Int -> IntList m -> IntList (S m) Covariant Yoneda lemma: をこっそり使って *…