< Retour au sommaire

CaTT - A type theory for higher categories

Thibaut Benjamin le

Lieu: https://rdv5.rendez-vous.renater.fr/semainaire-lsl

I will present an approach of the use of formal methods to reason about algebraic structures, with the example of the type theory CaTT. This type theory describes an algebraic structure called weak omega-categories, and it allows for an interactive theorem prover dedicated specifically to reasonning on these structures. Weak omega-categories are a particularly relevant example to illustrate this approach for several reasons. Fistly they are very intricate and complex structures to define, let alone to manipulate. Formulating them as a type theory provides a definition which is accessible to computer scientists with no particular affinity with category theory, together with a very concrete and computational way of manipulating them as terms of a language. Secondly the computer-checkability of this language provides with guarantees about the correctness of the proofs, allowing to formalize advanced results that would have been beyond the reach of a pen-and-paper mathematician. The fact that we are able to obtain a type system for such a complicated structure illustrates the power of this apporach.

I will illustrate this presentation with concrete examples of computations within the theory, as well as their corresponding formalization in CaTT.

After presenting this system, I will show the benefits of having a syntax to manipulate by defining a bit of automated reasoning adapted to this structure, called the suspension. It takes the form of a meta-operation on the syntax and we define it and check its correctness by purely syntactical methods. I will show the advantages of having such a feature for a few examples of explicit computations and show how this very concrete manipulation of the syntax also provides theoretical insight about the theory, that were not necessarily available in a more usual mathematical formalism.