任意のmonad: について･･･ Kleisli adjunction Kleisli category について、 と書くことにすると、functor: と、 を定義できて、 をunit、 をcounitとするassociated adjunction with : を作ることが出来る。 参考文献 Abstract and Concrete Categories: Th…

Monad algebra Monad: について、 monad algebra of とは、 (associative law) (unit law) を満たす代数的構造: のこと。 Eilenberg-Moore category 上記をobjectとするEilenberg-Moore category: を - と同様にして定義できる。 Associated adjunction with…

Adjunction morphism Unit-adjunction: について、 を満たすfunctorのペア: をadjunction morphismという。*1 命題 要件1と2が成立するとき、 のcounitをそれぞれ natural bijectionを とすると、 要件3 Adjunction category Small category上のadjunctionと…

Fork 圏論でよく見かける を満たすdiagram: のことをforkという。*1 Equalizer diagramはforkの一種。 参考文献 fork in nLab *1:フォークの形をしているから？

集合としての族 族 は、集合: とみなすことが出来た。 族としての集合 集合 は、族: *1 とみなすことが出来る。 参考文献 Abstract and Concrete Categories: The Joy of Cats (Dover Books on Mathematics) Indexed family - Wikipedia, the free encyclope…

Javaにて 15.28. Constant Expressionsを参照。 Scalaにて ほとんどのmethod呼び出しは、platform依存ということになっている。 ･･･のだが、実装上は上記のJavaの仕様に従うと思われる。 Arrayがconstant expressionにならない。 Scalaでも仕様上constant ex…

Free theoremのもと、いわゆるfunctor則は一つでいいらしい。 命題 における型族: について、 を満たす関数族: が存在するならば、 証明(の試み) 関数: のrelationによる表現: について、relation: を定義できて*1、 のparametricity: が得られる。 参考文献…

命題 Functor: について、 を満たす関数族: が存在するならば、 証明 Free theoremにより、 は、 についてfreely naturalなので vs. Applicative \f -> \x -> pure f <*> x は、functorialなので、上記の命題より fmap f x = pure f <*> x 参考文献 haskell …

記法 とする。 特に、 のとき、free theoremを想定すれば、naturalityの要件は自明となる。 Monoidal sets は、productとsingleton setにより、monoidal category: を成す。 Monoidal endofunctor over sets Monoidal endofunctor: とは、 endofunctor: natu…

任意のmonad: について･･･ Monadからのadjunction Adjunctionからのmonad - PSの対応: は、surjectiveであったので なるcounit-adjunction: が存在する。 Adjunction liftingによるright Kan extension Adjunction lifting - PSにより、 は、right Kan exten…

命題 Counit-unit-adjunction: について 証明 Category of... 上記の composition により、left adjoint functor を morphism とする category を作ることができるが、category of adjunctions とは言えない。 参考文献 Abstract and Concrete Categories: T…

Free monad Free monads are free - PSにより Free functor Free functor object - PSにより Operational monad とすると、Composition of adjunctions - PSにより は、discrete diagram から作った一番シンプルなmonad。 参考文献 Adjoint functors - Wikip…

Free functor object category: forgetful functor: について、ある -initial morphism: のこと(特に代表してのこと)を、free functor object over ということにする。 Discrete diagramから作った一番シンプルなfunctor、ということ。 Coends in sets Difun…

いわゆるfree monadは、確かに圏論的にもfreeである。 Free object あるforgetful functor: について、-initial morphism: のことを(特に代表して のことを)、free -object over というのであった。 命題 category: endofunctor: forgetful functor: につい…

Element-free law Monad morphism: の要件は、 *1 *2 であった。 Element-wise law 一方、Control.Monad.Morphでは、 morph . (f >=> g) = morph . f >=> morph . g morph . return = return となっていて、あれ？と思ってしまったが、 これはElement - PSの…