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 による圏論入門