November 25, 2024
Samuel Arsac (ENS Lyon)Adhesive categories are categories with structures that allows for some key results of graph rewriting theory to hold. There are also some weaker variations of this concept: rm-adhesive and rm-quasiadhesive categories.
I will present a formalization in Coq of the hierarchy of adhesive categories. This formalization relies on the Hierarchy Builder tool from the MathComp library. It is modular, with adhesive categories being at the top of a hierarchy which contains the weaker variants of adhesive categories and starts at the level of categories. Each level is equipped with several equivalent interfaces to define instances. It comes with a library of lemmas about more basic categorical concepts, such as pullbacks and regular monomorphisms.
This is my current work as a PhD student, supervised by Russ Harmer and Damien Pous.
The code can be found on this GitLab repository: https://gitlab.com/SamuelArsac/graph-rewriting