Agda による圏論入門

Menu Menu

Agda で証明しながら圏論を学ぶという予定です。あまり入門ではないかも。

Higher-Order Categorical Logic の 0章に相等する内容です。

BitBucket category-exercise-in-agda source code

  1. Agda の入門の要約

  2. Agda の入門 

  3. Agda の集合の Level 

  4. Agda の record  

  5. Agda のReasoning  

  6. Caategory module と圏の入門

  7. 自然変換

  8. IdentityFunctor と Hom Reasoning

  9. Monad の結合則

  10. Sets と Monoid を使った Monad の例

  11. Kleisli 圏の構成

    ここまでが Monad を理解するための部分。以下は、Adjoint 関連です。

  12. Adjoint から Monad を導く

  13. Kleisli 圏による Monad の Resolution

  14. Kleisli 圏による Conparison Functor

  15. Elienberg-Moore 圏の構成と Resolution

  16. Elienberg-Moore圏による Conparison Functor

  17. Universal mapping と Free Monoid を使った例

  18. Adjoint から Universal mapping

  19. Universal mapping から Adjoint

  20. Hom (F(-),-) = Hom (-,U(-)) と Adjoint

  21. 米田関手

  22. Equalizer

  23. Product, Pullback and Limit

  24. system T

  25. Cartesian Closed Category and Deduction Theorem

  26. さらに進んだトピック

  27. Agda sources

top : Agda による圏論入門


Shinji KONO / Thu May 9 11:52:16 2019