• Login

en fr

Cours: Introduction to Categories

Objectives : One focus of category theory is on studying relationships between structures occurring in mathematics and the foundations of computer science. Instances of abstract categorical concepts appear in many different fields, to which general categorical theorems can then be applied. For instance, the basic categorical concept of a "binary product" can be instantiated in the category of sets (cartesian product), in the category of vector spaces (direct sum), and in any poset (meet). Similar remarks apply to, among others, the categorical concepts of "functor", "natural transformation", and "monad". Category theory thus provides a useful level of abstraction for proving generic results. Moreover, categories themselves can also be used as models for logics and type theories. This establishes a strong back-and-forth connection between category theory, logic, and programming languages: the Curry-Howard-Lambek correspondence. For instance, the category-theoretic notion of "monad" was exported to functional programming languages such as Haskell. Categorical methods also feature prominently in research on the semantics of dependently typed languages (such as Agda, Lean, and Rocq) and have been used also in the context of quantum computing. Finally, during the course we may also mention some connections between category theory and automata theory.

Summary:

1. Basic concepts, e.g. categories, objects, morphisms.
2. Functors and natural transformations.
3. Universal and couniversal constructions, e.g. (co)products.
4. Adjunctions.
5. Monads.
6. Cartesian closed categories.

References :

• Introduction to Categories and Categorical Logic. Samson Abramsky and Nikos Tzevelekos. https://arxiv.org/abs/1102.1313
• Livre "Categories for the Working Mathematician" par Saunders Mac Lane. ISBN: 978-1-4757-4721-8, URL: https://doi.org/10.1007/978-1-4757-4721-8
• Page web du cours: https://ensps-categories.github.io/