Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2509.17392 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917304318558208 |
|---|---|
| author | Arsac, Samuel Harmer, Russ Pous, Damien |
| author_facet | Arsac, Samuel Harmer, Russ Pous, Damien |
| contents | We design a Rocq library about adhesive categories, using Hierarchy Builder (HB). It is built around two hierarchies. The first is for categories, with usual categories at the bottom and adhesive categories at the top, with weaker variants of adhesive categories in between. The second is for morphisms (notably isomorphisms, monomorphisms and regular monomorphisms). Each level of these hierarchies is equipped with several interfaces to define instances. We cover basic categorical concepts such as pullbacks and equalizers, as well as results specific to adhesive categories. Using this library, we formalize two central theorems of categorical graph rewriting theory: the Church-Rosser theorem and the concurrency theorem. We provide several instances, including the category of types, the category of finite types, the category of simple graphs and categories of presheaves. We detail the implementation choices we made and report on the usage of HB for this formalization work. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_17392 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Adhesive category theory for graph rewriting in Rocq Arsac, Samuel Harmer, Russ Pous, Damien Logic in Computer Science We design a Rocq library about adhesive categories, using Hierarchy Builder (HB). It is built around two hierarchies. The first is for categories, with usual categories at the bottom and adhesive categories at the top, with weaker variants of adhesive categories in between. The second is for morphisms (notably isomorphisms, monomorphisms and regular monomorphisms). Each level of these hierarchies is equipped with several interfaces to define instances. We cover basic categorical concepts such as pullbacks and equalizers, as well as results specific to adhesive categories. Using this library, we formalize two central theorems of categorical graph rewriting theory: the Church-Rosser theorem and the concurrency theorem. We provide several instances, including the category of types, the category of finite types, the category of simple graphs and categories of presheaves. We detail the implementation choices we made and report on the usage of HB for this formalization work. |
| title | Adhesive category theory for graph rewriting in Rocq |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2509.17392 |