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

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 …

任意の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 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: につい…

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

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

@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 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 …

命題 Functor: について、disjoint union: 上のbinary relation: を含む最小のequivalence relation を使って、 *1 とすると、 は、colimiting coconeになる。 参考文献 limits and colimits by example in nLab Equivalence class - PS Limits in sets - PS…

命題 Category: へのsmall diagram: について、 をそれぞれproductとする。ここで、 なる へのmediator のequalizer を採れば、 はlimiting coneになる。 証明 がそれぞれmono-sourceであることに注意する。 参考文献 The Existence Theorem for Limits « Th…

Evaluation functor Category について、evaluation functor: を定義できる。*1 と書くことにすると Swap functor Category について なるfunctorをswap functorと呼ぶことにする*2。これは明らかにisomorphism。 Yoneda embedding Locally small category …

Bifunctor lemma Functor の族: が を満たすとき and *1 具体的には とすればよい。 系 Bifunctor: について ならば 参考文献 Categories for the Working Mathematician (Graduate Texts in Mathematics) Category Theory (Oxford Logic Guides) Product of…