Adhesive category theory for graph rewriting in Rocq

Samuel Arsac, Russ Harmer, Damien Pous

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 bott…