Aspects of Category Theory in Proof Assistants
Monday 7 July 2025 at 14h00
ENS Paris-Saclay, Room 1B26
Abstract: While the use of proof assistants in mathematical research has yet to become the norm, an increasing number of results have been formalized. The prevalence of category theory in recent mathematical research indicates the need for its formalization in proof assistants. However, category theory is challenging to formalize for reasons we will explore.
The first difficulty is due to the fact that proposition equality in dependently typed theories as a structure that interacts in a complicated way with categories formalised inside those theories. We describe those challenges, and propose some solutions we explored to this problem.
The second difficulty is more pragmatic. One big advantage of category theory is its ability to be reasoned with using graphical languages. However, most proof assistants are text based; thus their notation systems cannot express any graphical language. We implement a plugin to graphically progress category theory proofs in the Coq proof assistant. After a quick demo, we will describe the differents challenges in the implementation of such a software.
The defense will be in English
Jury:
- Assia MAHBOUBI, Inria, Referee and Jury Member,
- Damien POUS, CNRS, Referee and Jury Member,
- Ambroise LAFONT, École Polytechnique, Jury Member,
- Paul-André MELLIÈS, IRIF, Jury Member,
- Samuel MIMRAM, École Polytechnique, Jury Member,
- Clément PIT-CLAUDEL, École Polytechnique Fédérale de Lausanne, Jury Member.
- Gilles DOWEK, Inria, Supervisor,
- Bruno BARRAS, Inria, Assistant Supervisor.