2014-10-01から1ヶ月間の記事一覧
いわゆる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: につ…
Functorが絡んだときのparametricityの求め方。 以下、 において･･･ Image Relation Graph Relation lifting Endofunctor: に対応する、relation間のmapping*1を と定義する。 命題 特に、関数: に対応するrelation: について、 証明 *2 参考文献 Theorems f…
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 - …
いわゆるif文の圏論的表現。 Distributive category has finite products: has finite coproducts: なるcategory のこと。 以下、distributive category について･･･ Predicate Guard If expression 参考文献 thesis.pdf
命題 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: をこっそり使って *…
(Primitive recursive functionの圏論による表現) *1 命題 endofunctor: initial algebra: -morphism: について なる -morphism: (paramorphism) がただ一つ存在する。 証明 参考文献 art08_geuvers_poll.pdf *1:かえって分かりやすい(と思う)
