さらにいくつかの証明

否定に関する性質

Stackoverflow から拾った否定の例題

まず、有限なグラフから圏を生成してみます。

examples/graph.agda
Product や Equalizerを離散圏をIndex するLimitとして定義します。

examples/limit-to.agda Sets の完全性、 Sets がLimitなどを持つことを示します。

随伴関手の存在を示すための条件に関する定理。コンマ圏を使います。Yoneda Functor を使った representation 定理もあります。

積(のようなもの)を保存する関手(Monoidal Functor)の可換性を定義します。

Sets 上で同等な積を用いずカーリー化を使って定義する Applicative関手が Monodidal 関手と同等であることを示します。Free theorem を仮定します。

Sets 上のMonadからApplicative funtorとMonoidal functor を導出します。