Co-Yoneda lemma - PS を( dinaturality でなく普通の) naturality の世界で表現するとこうなるらしい。 Contravariant Yoneda embedding *1 命題 Every set-valued functor is a colimit of representables: functor: forgetful functor: について 具体的に…

(Higher inductive types･･･と言いたいがそれはまた別物らしい。) Family of inductive types たとえば、Free monad - PS: は、 をfixed pointとするinitial algebraが族になっているだけ(で問題ない)。 Inductive family of types 一方、free applicativeに…

記法 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…