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…