記法 Category of applicative functors - PS Traversable functor その1 functor: natural transformation: *1 のペアで (unitality) (linearity) を満たすもの。 Traversable functor その2 functor: natural transformation: *2 のペアで (identity) (com…

Applicative morphism 二つのapplicative functor: の間のmorphismを を満たすnatural transformation: とする。 Monoidal morphism Applicative functorはmonoidal endofunctorで表現できたので、同様に 二つのmonoidal endofunctor on monoidal or : の間…

(･･･なんて略語はたぶんない) 命題 Right Adjoints Preserve Right Kan extensions: adjunction: functor: functor: right Kan extension along : について、 も、right Kan extension along 。 証明 Adjunction lifting - PS(のpostcomposition版)により で…

Representable functor なるfunctor: のこと。 Copower Power - PSのdual: のこと。 Copowers in sets 特に、 のとき 命題.1 Functor: について、 証明 命題.2 Representable functor: について、functor: が定義できるならば、 証明 参考文献 Representable…

Functor: について･･･ ある圏 三つ組: functor: functor: natural transformation: から同じく三つ組: functor: functor: natural transformation: へのmorphismを、 *1 を満たすfunctor: と定義すれば、categoryを成す(と思う)。 命題 Comma category: から…

(･･･という単語の定義を試みる) Universe 集合族 集合族: とは、関数: のこと、と同時に関数適用を と書くことの表明。 以下、集合族 について･･･ Union Product Mapping なる を mapping such that associates to each a という(と思う)。このことを と書い…

Strong monad Monoidal category: について、もろもろのcoherence conditionを満たす monad: natural transformation: (strength) のペアのこと。 命題 monoidal category: monad: について、 とすれば、 はstrength。 証明 に注意する。 系 同様にして、Has…

Strength monoidal category: endofunctor: について、strength for とは、natural transformation: で *1 を満たすもの。 Strong endofunctor 上記のようにstrengthを持つendofunctorのこと。 用語がlax(普通のmonoidal functor)に対するstrongと被っている…

命題 Haskell-monad: について、 とすると、 は、applicative。 系 monoidal category: monad: について、 とすると、 はmonoidal endofunctor on になる(と思う)。 参考文献 haskell - How to show that a monad is a functor and an applicative functor? …

(･･･とでも呼ぶことにする) Posetal powerset 任意の集合 について、objectを の部分集合、morphismを とするposetal category*1: を定義できる。 以下、任意の関数: について･･･ Direct(existential) image Inverse image Dual(universal) image とすると、…

Haskell-monad Monad laws - HaskellWikiより、Haskell-monad: とは、 endofunctor: natural transformation: *1 関数族: で、left identity則、right identity則、associativity則、および *2 を満たすものとする。 命題 MonadとHaskell-monadは同値。 Endo…

(･･･という用語は無いかもしれない) 任意のmonad: について･･･ Associated adjunction を満たすadjunction: を、associated adjunction with というのであった。 Category of associated adjunctions 上記をobjectとするcategory: をAdjunction category - P…

任意の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の…

Inhabited set 空でない集合のこと。 Pointed set 集合とその要素のペア: からなる代数的構造。このとき、 はinhabited。 Pointed object category: terminal -object: について、 -object: -morphism: のペア(からなる代数的構造) をpointed objectという。…

Monoidal category Monoidal category: とは、 category: bifunctor: (monoidal product) -object: (unit object) natural isomorphism: (associator) natural isomorphism: (left unitor) natural isomorphism: (right unitor) で、pentagon equalityとtria…

Processed string literalの展開 foo"t0${x1}t1 ... ${xn}tn" は、 new StringContext("t0", "t1", ... , "tn").foo(x1, ..., xn) のように展開される･･･のだが、これが有効な式でさえあればよいらしく、 extractorも返せてしまうようだ。*1 例 implicit cla…