Congruence relation Equivalence relationの族: が、以下を満たすとき、category 上のcongruence relationと言う。 *1 これは、 と同値。 Quotient category Category 上のcongruence relation について、quotient category: を次のように定義できる: *2 Ge…

Evaluation functor Naturality square の対角線を返すもの。 Godement product Functor: と、natural transformation: について、Godement product(horizontal composition) を evaluation functor を使って次のように定義する: は、しばしば省略される。 …

Haskell(kan-extensions)のYoneda functor: newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -> b) -> f b } を攻略する試み。 Yoneda lemmaのdual版 Category Theory (Oxford Logic Guides) のyoneda lemmaから を使えば、dual版を作ることができ…

CoYoneda data CoYoneda f a = forall b. CoYoneda (b -> a) (f b) は、圏論っぽくかくと、morphism族: のこと Parametricity theorem Parametricity theoremにより、なんやかんやで はnaturalになる(らしい)。 特に、 についてのnaturalityにより

# 参考文献 How to draw commutative diagrams in LaTeX with TikZ | A Beautiful Place

Comma category 二つのfunctor: について、comma category: のmorphismはこんな感じであった: Comma functor (と呼んでいいと思う) つまり、naturality squareを上下にくっつけるfunctorを返す。 Morphismの実装部(青色)は変化していない。 Hom functor 特に…

Pullback functor Category -morphsim について、pullback functor: を定義できる。 これは、limit functorの一種。 参考文献 Definition:Pullback Functor - ProofWiki Category Theory (Oxford Logic Guides)