Initial algebraの族からのadjunction category: endofunctor: forgetful functor: について、initial algebraの族: が存在するならば、Initial algebras with parameters - PSより、これをnaturalにするfunctor: を作ることが出来る。いま、 とすると は、i…

Constant expressions SLS 6.24より、constant expressionとは(基本的に)以下のいずれかである: A literal of a value class, such as an integer A string literal A class constructed with Predef.classOf An element of an enumeration from the underly…

showCode Scala 2.11からshowCodeというすごいmethodが追加されており、 これは「コンパイル可能な文字列を返す」ということで、 c.TreeとStringが相互に変換可能になっている。 object Parse { def apply(x: String): Any = macro Impl.apply final class I…

記法 Regular (epi)monomorphism 何かの(co)equalizerになっているmorphismのこと。*1 Extremal (epi)monomorphism を満たす(epi)monomorphism のこと。 命題 参考文献 Abstract and Concrete Categories: The Joy of Cats (Dover Books on Mathematics) *1:…

scala.Singletonって何？という話 エラーメッセージによると、scala.Singletonはfinal traitでありextendsできない。 Path Scala言語仕様(以下SLS) 3.1より Paths are not types themselves, but they can be a part of named types ... ざっくり言うと、val…

shapelessのLazyを攻略する試み。*1 実装 implicitlyのためにmacroで実装される。quasiquoteを使うと trait Lazy[T] { val value: T } object Lazy { implicit def mkLazy[T]: Lazy[T] = macro mkLazyImpl[T] def mkLazyImpl[T](c: Context)(t: c.WeakTypeTa…

型を返すmacroがボツになり、 type t = typeOf("hello") と書けなくなったので替わりになるもののアイデアメモ。*1 その１ valを経由して val t = typeOf("hello") type t = t.unwrap とする。 その２ Annotation macroを使って @typeOf val t = "hello" と…

はてなブログのtexがMathJaxに対応したらしい。 変更点 \limitsが多くの記号に使えなくなった(ようだ)。 \oversetと\undersetを使う \congが使えるようになった。 記号の隙間が適切になった。 dash(\unicode{x2013})が使えるようになった。 Text attributes…

2.10辺りからの変更点 Untyped macroがなくなった。 替わりに文字列を使う。*1 Type macroがなくなった。 言語の見た目を拡張するのはよろしくない、という方針か。 どうエミュレートするか悩みどころ Contextがwhitebox.Contextとblackbox.Contextに分かれ…

記法 任意のuniversal morphism: について、 とのmediator を、 のような感じで、 と書くことにする。 Power functor その1 Power projectionの族: が存在するならば、これをnaturalにするただ一つのcontravariant functor: を作ることが出来る。 Power func…

Codensity monad Functor: について、right Kan extension of along : が存在するならば、 *1 は、monadを成す。このmonadをcodensity monad of という。 Adjunctionからのcodensity monad 特に、 がleft adjoint: を持つとき、Adjunction lifting - PSによ…

Power をlocally small categoryとする。 について、constant functor: *1 のlimit、つまりproduct: を、power of といい、 等々と書く。そのprojectionは、 のようなmorphism族である。 Natural bijectionによる表現 Power projectionは-terminal morphism…

Precomposition functor Category と functor について、precomposition functor: *1 を定義できる。 命題 counit-adjunction: category: について は counit-adjunction となる。ここで *2 は、-ran *3 の族である。 逆に、二つの -ran: が存在するならば *…

Functor: について･･･ Pointwise Kan extension がlocally smallのとき、right kan extension: で、 を満たすものを、pointwise right Kan extensionという。 Limiting coneの族からのKan extension 自明なforgetful functorを としたとき、limiting coneの…

Canonical natural transformation of comma categories Comma category: について、その定義により、-objectを添字とするmorphism族: は、natural。 詳しくは、自明に定まるfunctor: を使うと、 は、canonical natural transformation: になる。 Dense func…

Preservation of right Kan extensions Functor: と、right Kan extension of along : について、 とのwhikering: が、right Kan extension of along になるとき、 preserves a right Kan extension という。 Preservation of left Kan extensions 同様にし…

@Deprecated 替わりにAdjunction lifting - PSを参照。 命題 Functor: について、 *1 *2 *3 そのdual: 記法 参考文献 Anderson.pdf The Comonad.Reader » Kan Extensions II: Adjunctions, Composition, Lifting *1:universal morphismの族 *2:ひとつのunive…

Functor: について、 命題 *1 そのdual: 記法 参考文献 Anderson.pdf *1: はconstant functor

記法 Terminal natural transformation*1 と natural transformation との mediator を と書くことにする。 命題 Functor: について、 しかも、 についてnatural。 証明 は complete なので、ending wedge の族: を作ることができるが、ここで、 とすると は…

命題 Functor: について、 しかも、 についてnatural。 具体的には、 はcocompleteなので、coending cowedgeの族: を作ることができるが、ここで、 とすると、 は、left Kan extension of along になる。 参考文献 Categories for the Working Mathematician…

(Co)Yoneda reduction Yoneda lemmaの(co)endによる表現: を、(co)Yoneda redunctionという(と思う)。 (Co)Yoneda reduction for free (Co)Ends for free - PSとより、 Functor.(Co)Yoneda 上をHaskellで実装したのが、kan-extenstionsの module Data.Functo…

Free dinaturalityのもと、difunctor について･･･ Ends for free Limits for free - PSと同様にして、projection: は、 のending wedgeになる: このending wedgeは、identity function: と本質的に等しい。 Coends for free Colimits for free - PSと同様に…

Free dinaturality Free theoremはdinaturalityについても有効である(らしい)。 命題 Free naturalityが成立するならば、free dinaturalityも成立する。 以下、非常に怪しい証明･･･ 証明 Twisted arrow category - PSによる、 を利用する。詳しくは、morphis…

以下、Limits for free - PSのdual。 Cocones for free Functor のcoproduct: について、function: を のcocone for freeと勝手に呼ぶことにする。 これは、以下のcategoryにより のcoconeと本質的に等しい。 Cocone category for free なる をcocone for fr…

以下、category と (的なもの) にて、free naturalityが成立するとする。 Cones for free Functor のproduct: について、function: を のcone for freeと勝手に呼ぶことにする。 これは、以下のcategoryにより のconeと本質的に等しい。 Cone category for f…

Free theorem ある種の体系では、naturalityが常に成立するという(ことを含む)定理。 このnaturalityをfree naturalityと勝手に呼ぶことにする。 命題 Functor について、product: に関してfreely naturalならば、coproduct: に関してもfreely natural。 証…

Co-Yoneda lemma Category をlocally smallとする。 任意の -object と functor について、 しかも、 と についてnatural(と思う)。 具体的には、関数: とすると、 がcoending cowedgeになる。 Contravariant co-Yoneda lemma 特に、 とすると、functor につ…

Yoneda lemma Category をlocally smallとする。 任意の -object と functor について、 しかも、 と についてnatural。 具体的には、関数: とすると、 がending wedgeになる。 Naturalityはpointwise endsにより定義される(と思う)。 Contravariant Yoneda …

Precomposition functor Category と functor について、whiskering functor precomposition functor: *1 を定義できる。 Right Kan extension Functor: について、-terminal morphism*2: を、right Kan extesion of along (-ran) といい、 を、 で表す: Hom…

Arrow category Arrow category とは、comma category: のことであった。 Twisted arrow category 任意のcategory について、morphismの向きを逆にするfunctor: を使ったcomma category: のことを、twisted arrow categoryと呼び、 と書くことにする。 さら…