<figure><img src="image_1.png" /></figure>

HAL
open science

# Adhesive category theory for graph rewriting in Rocq

Samuel Arsac, Russ Harmer, Damien Pous

► To cite this version:

Samuel Arsac, Russ Harmer, Damien Pous. Adhesive category theory for graph rewriting in Rocq. 2025. hal-05263561

HAL Id: hal-05263561

https://hal.science/hal-05263561v1

Preprint submitted on 16 Sep 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
# Adhesive category theory for graph rewriting in Rocq

Samuel Arsac
ENS de Lyon
Lyon, France

Russ Harmer
CNRS
Lyon, France

Damien Pous
CNRS
Lyon, France

## Abstract

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.

**Keywords:** adhesive categories, categorical graph rewriting, graph transformation, Rocq, hierarchies

## 1 Introduction

Categorical graph rewriting, or graph transformation [13, 30], is a framework for defining rewriting rules on graphs, together with the double-pushout (DPO) operational semantics, using categories to abstract away the differences between specific concrete graph models. It has found various applications in computer science, such as model-based software engineering [18]; in mathematical physics, such as the rewriting of string diagrams [6]; and in modeling (bio-)chemical systems, where rewriting rules model the interactions between particles or molecules [3, 11].

In this domain, one often uses adhesive categories [15, 23]; these include all presheaf categories, hence many categories of multigraphs. However, there are important categories of graphs that are not adhesive. This motivated the introduction of weaker notions to cover those cases and still make it possible to establish good properties of the DPO semantics. For example, the category of simple graphs is only *rm-quasiadhesive* [15, 20] while the category of term graphs is *rm-adhesive* (also called *quasiadhesive* in the earlier literature) [10].

The definitions of these classes of categories involve standard notions such as pullbacks, pushouts and monomorphisms; yet, proving the various implications existing between these definitions is sometimes difficult. Their formalization can therefore be seen as an interesting test case for the development of general purpose category theory libraries.

As usual for formalization, a challenging task consists in structuring the definitions so that lemmata can be stated and used in their most general form and instances can be defined in the most efficient way. To this end, we choose to use Hierarchy Builder (HB) [9], which provides a high-level language to define hierarchies of structures, with advanced features such as multiple inheritance. HB checks the consistency of these high-level descriptions and translates them into appropriate Rocq records, canonical structures and coercion declarations [14], to obtain concise notations and robust inference mechanisms without further user input.

Our formalization currently includes (i) a general purpose category theory library; (ii) the definitions of adhesive, rm-adhesive and rm-quasiadhesive categories; (iii) two important theorems providing several characterizations of those structures; (iv) two key theorems from categorical graph rewriting; and (v) prototypical instances (types, setoids, finite types, simple graphs, presheaves and slice categories).

The abstract library is axiom-free, and we detail the axioms which are needed for some of the concrete instances.

The development is available on Gitlab<fnref n="1" />, with a README file linking the theorems in this paper to the relevant parts of the code.

**Outline.** In Section 2, we detail our implementation of the basic category theory<fnref n="2" /> that we require and its organization using HB. A specificity of our work is that we define not only a hierarchy of categories, but also a hierarchy of morphisms (isomorphisms, monomorphisms, epimorphisms and their regular and split variants). This is important, as these concepts are pervasive and we need good inference mechanisms to work with them efficiently. We review the notations we set up; how we cover bundled and unbundled definitions; and how we exploit categorical duality.

In Section 3, we move to the specifics of categories for graph transformation. We recall the key definitions and theorems; we explain how to extend the previous standard hierarchies with these notions, in a modular fashion, while conforming to the forgetful inheritance policy of HB; and we

<footnote n="1">¹https://gitlab.com/SamuelArsac/graph-rewriting</footnote>

<footnote n="2">²While we recall definitions for concepts specific to adhesive category theory, we assume familiarity with the basic concepts of category theory [27].</footnote>
give an overview of the main theorems we have formalized for (rm-(quasi))adhesive categories. In Section 4 we briefly present categorical graph rewriting and the two theorems from it we have formalized. We discuss the formalization of concrete instances in Section 5. We conclude with a discussion of the results (Section 6), related work (Section 7) and directions for future work (Section 8).

# 2 General category theory

## 2.1 Equality on morphisms

The first question when formalizing categories in type theory is “how to compare morphisms?”.

A simple approach uses propositional equality, and rests on axioms such as functional extensionality and proof irrelevance (e.g., to compare natural transformations) and some forms of choice and predicate extensionality (e.g., to quotient functors by functor equivalence<fnref n="3" />).

To reduce the number of axioms while keeping propositional equality, one may consider univalent type theory and formalize univalent categories [2, 29, 39]. However, many categories are not univalent (any category with two distinct yet isomorphic objects), we still need functional extensionality early on for several constructions, and then the univalence axiom to define the category of (h)sets and functions.

To avoid axioms completely, we can instead formalize $\mathcal{E}$-categories [21, 37], where each homset is equipped with a user-defined equivalence relation, and equations between morphisms hold only up to these equivalence relations. Like in [19, 40], this is what we do in the present work, using Rocq support for setoid rewriting [31]. The main advantage is that we keep all the abstract parts of the library axiom-free, postponing the potential use of axioms to specific instances. We further discuss this choice in Section 6.2.

## 2.2 The hierarchies of categories and morphisms

We start from the definition of categories from the examples found in the repository of HB (adapted for $\mathcal{E}$-categories, which we simply call categories in the sequel). It is defined in three steps:

* quivers: objects and homsets;

* precategories: quivers with identity arrows and composition;

* categories: precategories with equations for identities and associativity of composition.

While our development does not strictly speaking require such a level of detail in the definition of categories, this is a good example of the way we use a hierarchy: we define structures that inherit from each other (e.g., every category is a quiver) and define operations and lemmata at the lowest (i.e., most general) point at which they can be stated or proved.

<figure><img src="image_2.png" /><figcaption>**Figure 1.** The two hierarchies in the library. An arrow from a structure A to a structure B means that every instance of A is also an instance of B, i.e., A *inherits* from B.</figcaption></figure>

For example, the notion of terminal object can be defined in any quiver; the notion of isomorphism and the fact that terminal objects are unique up to unique isomorphism require precategories; and the fact that the composition of two isomorphisms is an isomorphism holds only in categories.

Alongside this hierarchy of categories, we define a hierarchy of morphisms: in addition to monomorphisms, epimorphisms, and isomorphisms, we also need the concepts of *regular* and *split* monomorphisms, as well as their duals: regular and split epimorphisms. (A regular monomorphism is a morphism which is the equalizer of some pair of parallel morphisms; a split monomorphism is a morphism with a retraction.) In the rest of this paper, we abbreviate ‘epimorphism’ and ‘monomorphism’ as ‘epi’ and ‘mono’ respectively, as is common in the literature.

These two hierarchies are depicted in Figure 1. We will extend them with more specialized notions, when moving to adhesive category theory, and it is crucial to have proper tool support for this: our use case here, of specializing to adhesive categories, is just one instance of a frequent activity in the context of formalizing large hierarchies of structures. More specifically, we need to be able to:

1. use freely any definition, notation or lemma available, for a given structure, in all structures that inherit from it (i.e., all structures above it in the hierarchy);

2. add new structures without breaking existing code, possibly in the middle of the hierarchy;

3. provide instances incrementally and by various means.

In Rocq, there are two principal ways of implementing such hierarchies: typeclasses [32, 40] and canonical structures [25]. Typeclasses are often easier to set up at first, but are rather fragile and may become inefficient in large hierarchies [4, Section 12]. Canonical structures have been used at a large scale in mathcomp [26], and have been proved robust and efficient, but require expert knowledge of the unification

<footnote n="3">³The appealing axiom stating that equivalent functors are propositionally equal is inconsistent in this setting—see supplementary material, so we are obliged to take a quotient, or to move to bicategories [35].</footnote>
algorithms. Some developers have used a mixture of canonical structures and typeclasses [28]. HB provides an abstract layer and implements packed classes [14], using canonical structures, on behalf of the end user. We have chosen to experiment with its capabilities and we report on its current limitations.

Inference in packed classes is driven by a single *index*. In our hierarchy of categories, the index is the type of objects; in our hierarchy of morphisms, it is the morphism itself. For example, if we ask for the canonical category whose object type is *Type*, we will get the category of types and functions; but if we ask for the canonical category whose objects are functors between two given categories, we will get the category of functors and natural transformations. Similarly, for morphisms, if we ask for the canonical isomorphism whose underlying forward morphism is the identity, we will get the identity isomorphism; if we want to promote a composite morphism into an epimorphism, inference will attempt to promote its two constituents into epimorphisms.

The most important concept for packed classes is that of *mixin*: a datatype depending on the index and on other mixins on that index. For example:

* the mixin for quivers has no dependency but the index type of objects, and consists of a setoid (a type with an equivalence relation) for each pair of objects;

* the mixin for precategories depends on the mixin for quivers and consists of identity arrows and composition;

* the mixin for categories depends on the mixin for precategories and consists of proofs that the identities and composition satisfy the expected equations;

* mixins for morphisms define individual properties of morphisms and so never depend on each other, only on their index, i.e., a morphism;

* the mixin for monos consists of the proof that the morphism is a mono—a property in *Prop*;

* the mixin for a regular mono consists of the pair of morphisms of which it is an equalizer and the corresponding proof; similarly, the mixin for a split mono consists of its right inverse and the corresponding proof. In both cases this additional information must be in *Type* since it is computationally relevant, and often used to construct other values in *Type*; nevertheless, we can safely ignore it when we compare morphisms, thanks to our use of setoids and *E*-categories.

*Structures* in HB are then defined as collections of mixins, and *inheritance* is defined by inclusion: a structure *A* inherits from a structure *B* if it contains *all* its mixins. This point is very important as it means that HB only implements *forgetful* inheritance [9]. This policy has the advantage of robustness—but has several consequences for the way we must structure the code.

In our development, structures are always defined with exactly one mixin in addition to those of the structures it inherits from. We have mentioned some of these mixins above. Observe that, with these definitions, a regular mono contains two mixins: that for regular monos and that for monos, even though the former implies the latter. If we remove the latter for the sake of minimality, the inheritance from regular monos to monos would be *non-forgetful*. For the same reason, an isomorphism consists of seven mixins (cf. Figure 1).

To cope with these redundancies, we use the mechanism of *builders* provided by HB: we prove and declare that the mixin for monos can be derived from that for regular monos, so that it suffices to provide the latter in order to build concrete instances. (See Section 2.5 for details.) We proceed similarly with other standard implications (e.g., split mono implies regular mono), but this is still not enough. For example, it is well known that a regular mono which is also an epi is an isomorphism; and dually, every regular epi which is also a mono is an isomorphism. Thus we have at least two other ways to construct an isomorphism than to show both split epi and split mono, as inheritance would suggest. To this end, we use *factories*, which are mixins that do not appear in structures, but can be used to build other mixins. For the previous example, we declare an empty factory, depending on the two mixins for regular monos and epis, and we define builders constructing all other mixins from this data (and dually for the second alternative).

## 2.3 Notations

Clear and concise notations with overloading are crucial in formalized mathematics [16]. Combined with implicit arguments and Rocq's notation system, the mixture of canonical structures and (reversible) coercions used by HB makes it possible to obtain a notation system which remains close to textbook notations.

For example, we just use $A \sim B$ for the type of arrows from $A$ to $B$ in a category. Since categories are indexed by their object type, the type of $A$ and $B$ canonically determines that category. If they are spans, the arrow denotes a span morphism; if they are functors, the arrow denotes a natural transformation, etc. Similarly, we use the symbol *idmap* for identities, $(\circ)$ for composition, $(\equiv)$ for morphism equality, $(\cong)$ for isomorphisms, whatever the category. For the situations where we want the notation to enforce the choice of category, and thus the type of objects, we also set up variants indexed by the category (e.g., $A \cong C B$).

A recurrent pattern in category theory is the existence of a unique morphism satisfying a given property, where unicity is up to morphism equivalence. As in Wiegley's library [40], we use a single notation $(\Sigma!)$ and a few tools to manipulate such statements. We define this notation in *Type* as the witness is most often computationally relevant (e.g., we need full access to the mediating arrow in a pullback, in order to be able to use it to construct new morphisms).
## 2.4 Bundling

Structures defined with HB are *bundled*. For example, a category is a single package containing the type of objects, the type of the homsets, the identities, etc. This is convenient when we want to quantify on structures, and yields concise and readable proof contexts: we may have a single variable $i: A \simeq B$ that denotes an isomorphism, rather than a variable for the underlying morphism and a separate assumption about it actually being an isomorphism.

However, there are situations where we need unbundled structures. Consider for instance the statement: “pullbacks along isomorphisms are isomorphisms”. The isomorphism taken as input can be fully bundled, but the output one cannot: it is the purpose of the lemma to promote it from being a mere morphism to being an isomorphism; so we need a name for the predicate “being an isomorphism”. Within the hierarchy of morphisms, this phenomenon is frequent within proofs, where we have morphisms in the local context that we must progressively upgrade to regular monos, split monos, etc. To this end, we use either *aliases* or the *packing* mechanism provided by HB. In both cases, we use some ad-hoc boilerplate code which should become a generic promotion tactic in the future.

This tension between bundled and unbundled definitions also occurs with concepts outside our current hierarchies. Consider for instance pullbacks, for which we may use several definitions, each with its own pros and cons:

1. Being a pullback can be stated as a property of four morphisms organized in a square:

Definition isPullback {C: PreCat} {A B C D: C}
(f: A $\rightsquigarrow$ C) (g: B $\rightsquigarrow$ C) (p: D $\rightsquigarrow$ A) (q: D $\rightsquigarrow$ B) :=
f $\circ$ p $\equiv$ g $\circ$ q $\wedge$
$\forall$ E (p': E $\rightsquigarrow$ A) (q': E $\rightsquigarrow$ B),
$\Sigma!$ u: E $\rightsquigarrow$ D, p' $\equiv$ p $\circ$ u $\wedge$ q' $\equiv$ q $\circ$ u.

The corresponding diagram is recalled below:

<figure><img src="image_3.png" /></figure>

This fully unbundled definition is well-suited to state and prove standard facts, such as the pasting lemma of pullback squares, stability of monos under pullbacks or lemmata about isomorphisms that can be moved around the corners of a pullback square:

Lemma isMono_stable_pb ...:
isPullback f g p q $\rightarrow$ isMono f $\rightarrow$ isMono p.
Lemma isPullback_iso_A ... (i: A $\simeq$ A')(f': A' $\rightsquigarrow$ C):
isPullback f' g (i $\circ$ p) q
$\leftrightarrow$ isPullback (f' $\circ$ i) g p q.

(In the first lemma, isMono is our *unbundled* predicate for “being a mono”.)

2. However, the above definition is not convenient to define categories with all pullbacks. Indeed, in such a case, it is preferable to have the (bundled) type of spans that complete a given cospan into a pullback:

Definition Pullback {C: PreCat} {A B C: C}
(f: A $\rightsquigarrow$ C) (g: B $\rightsquigarrow$ C) :=
$\Sigma$ D (p: D $\rightsquigarrow$ A) (q: D $\rightsquigarrow$ B), isPullback f g p q.

This type is not convenient for stating the aforementioned lemmata, but to require all pullbacks in a category C, we can simply ask for a function

pullback: $\forall \{A B C: C\} (f: A \rightsquigarrow C) (g: B \rightsquigarrow C)$,
Pullback f g

3. When it comes to proving that pullbacks are unique up to unique isomorphisms, the best definition is the most categorically-minded one: a pullback is a terminal object in the category of spans completing the given cospan into a commuting square. We prove this characterization: it requires us to define subcategories and the category of spans, but uniqueness then comes for free as a special case of unicity of terminal objects.

In the end, we keep both a fully unbundled definition (stating that a square of morphisms is a pullback) and a partly bundled one (stating that a cospan has a pullback), and we set up appropriate lemmata to move back and forth between them. We proceed similarly with all other concepts in the library. In particular, the aforementioned lemma about stability of monos along pullbacks is rather stated as follows, where $A \to C$ is our notation for the type of monos from A to C.

Lemma Mono_stable_pb {C: Cat} {A B C D: C}
(f: A $\to$ C) (g: B $\to$ C) (p: D $\to$ A) (q: D $\to$ B):
isPullback f g p q $\to$ isMono p.

## 2.5 A concrete example: regular monos

To give a concrete example of how things are set up with HB, here is how we define regular monos in the library.

First, recall that an *equalizer* of a pair of parallel morphisms $f$ and $g$ is the most general morphism $e$ such that $f \circ e = g \circ e$, as illustrated in the diagram below.

<figure><img src="image_4.png" /></figure>

In Rocq we define the following predicate:

Definition isEqualizer {C: PreCat} {A B E: C}
(f: A $\rightsquigarrow$ B) (e: E $\rightsquigarrow$ A) := f $\circ$ e $\equiv$ g $\circ$ e $\wedge$
$\forall$ E' (e': E' $\rightsquigarrow$ A), f $\circ$ e' $\equiv$ g $\circ$ e' $\rightarrow$
$\Sigma!$ $\varepsilon$: E' $\rightsquigarrow$ E, e' $\equiv$ e $\circ$ $\varepsilon$.
A regular mono is then simply a morphism that is an equalizer for some pair of morphisms, and we can prove that every regular mono is indeed a mono:

Definition isRegMono {C E A} (m: E $\rightsquigarrow$ C A) :=
Σ B (f g: A $\rightsquigarrow$ B), isEqualizer f g m.

Lemma isRegMono_isMono {C E A} (m: E $\rightsquigarrow$ C A):
isRegMono m $\rightarrow$ isMono m.

We can now register the structure in HB as follows:

HB.mixin Record IsRegMono C E A (m: E $\rightsquigarrow$ C A) :=
{rmProp: isRegMono m}.

HB 结构 Definition RegMono C E A :=
{m of Mono C E A m & IsRegMono C E A m}.

HB.builders Context C E A m of IsRegMono C E A m.

HB instance Definition _ :=
IsMono. Build m (isRegMono_isMono m rmProp).

HB. end.

First, we define a new Mixin; then we define a new structure
RegMono, consisting of this new Mixin together with all the
mixins (in fact just one) of the structure Mono; and finally,
we register the previous lemma as a builder from the new
mixin to the Mixin of Mono. This builder makes it possible to
define regular monos by providing only the expected prop-
erty, while the redundant definition of the structure RegMono
ensures forgetful inheritance from regular monos to monos.

From this point, we can use both the type RegMono A B
of regular monos from A to B and the unbundled predicate
isRegMono f characterizing such morphisms.

## 2.6 Duality

Another important point in category theory is duality: every
abstract concept or lemma has a dual: epis/monos, equaliz-
ers/coequalizers, initial/terminal objects and their unicity,
pushouts/pullbacks and their pasting lemmata, etc. Like in
other works [2, 19, 28, 35, 40], we try to exploit duality as
much as possible, in order to avoid code duplication. The
central tool is the definition of the dual S<sup>op</sup> of a structure
S (be it a quiver, precategory, category or one of the vari-
ous kinds of morphism): by applying a lemma on a generic
structure S to the structure S<sup>op</sup>, we get the dual statement.

While this is easy on paper, there are several difficulties
to be overcome in our case:

1. The type of isomorphisms of $C^{op}$ is only equivalent to the type of isomorphisms of C (even up to reversing arguments, even with proof irrelevance: if $A \simeq_C B$ is a record with three fields:

{i: A $\rightsquigarrow$ C B; j: B $\rightsquigarrow$ C A; _: i o j $\equiv$ id ^ j o i $\equiv$ id}

then $B \simeq_{C^{op}} A$ is the record:

{i: A $\rightsquigarrow$ C B; j: B $\rightsquigarrow$ C A; _: j o i $\equiv$ id ^ i o j $\equiv$ id}

note that the two conjuncts have been swapped, so
that we may at most prove the two types proposition-
ally equal, using propositional extensionality).

This means we sometimes need to explicitly cast iso-
morphisms of one kind into the other.

2. We want duplicated definitions for readability and end-user experience: neither the definition of pullback, nor that of pushout, should involve $C^{op}$. Nevertheless, the terms @Pushout C and @Pullback $C^{op}$ should be definitionally equal to exploit duality. This requirement prevents us from using dedicated records in such definitions, which is why we have used a generic sigma type in the above definition of Pullback.

3. The categories C and $C^{op}$ share the same type of objects, so that we need to disambiguate in order for canonical structure inference to find the right instances. To this end, we use aliases: we define an identity function catop: Type $\to$ Type, which we bind to the notation $S^{op}$ and use to annotate object types for which we want the dual structures to be inferred. For morphisms, we use the same technique, using the following identity function:

Definition morphop {C: Quiver} {A B}
(f: A $\rightsquigarrow$ C B): B $\rightsquigarrow$^{C^{op}} A := f.

We systematically declare instances for dual structures; for
instance we write

HB. instance Definition _ {C} (A B: C) (m: RegMono A B)
:= IsRegEpi. Build C^{op} B A (morphop m) (rmProp m).

so that morphop *m* is automatically recognized as a regular
epi whenever *m* is a regular mono. Doing so, and using the
aforementioned techniques, we manage to reuse proofs for
most dual statements. For example,

Lemma Epi_stable-po {C} ... (f: C $\to$ A) ... :
isPushout f g p q $\to$ Epi p.

Proof (Mono_stable_pb (C:=C<sup>op</sup>)).

Lemma isPushout_iso_A {C} ... A' (i: A' $\simeq$ A)(f': C $\rightsquigarrow$ A'):
isPushout f' g (p o i) q $\leftrightarrow$ isPushout (i o f') g p q.

Proof (isPullback_iso_A (C:=C<sup>op</sup>)) (iso_op i)).

(In the second proof, `iso_op` is the aforementioned cast operation on isomorphisms.)

In the long term, we would like to develop support for
transporting results along equivalences of categories, which
should make it possible to avoid some of the current contor-
tions and limitations regarding duality.

## 3 Adhesive category theory

Now that we have in place the basic concepts of category
theory that we require, we briefly explain the key ideas of
adhesive category theory and then present our formalization
of this theory—with a focus on the issue of describing this
theory in a modular way, based on the generic category
theory library of the previous section.
## 3.1 Van Kampen squares and adhesive morphisms

We first define three properties of pushout squares and two new classes of morphisms. We provide these definitions to give an idea of the concepts that we need to manipulate; they can be taken as black boxes in what follows.

**Definition 3.1** (Van Kampen square [23]). A pushout is

* *stable* iff, for every commutative cube with the arrows as in the diagram below, where the bottom face is the pushout square and where the vertical faces are pullbacks, the top face is a pushout;

* *exact* iff, for every commutative cube with the arrows as in the diagram below, where the bottom face is the pushout square, the left and back faces are pullbacks, and the top face is a pushout, the front and right faces are pullbacks;

* *Van Kampen* if it is both stable and exact.

<figure><img src="image_5.png" /></figure>

The two key properties of Van Kampen squares are that they preserve monos and that they are also pullbacks [23].

**Definition 3.2** (Adhesive morphisms [15]). A morphism is

* *pre-adhesive* iff it has pushouts along any morphism and these pushouts are stable and also pullbacks;

* *adhesive* iff its pullbacks along all morphisms are pre-adhesive.

Adhesive morphisms are pre-adhesive (by pulling back along the identity); pre-adhesive morphisms are regular monos; and isomorphisms are always adhesive.

Accordingly, we turn these two classes into HB structures. We can easily add them to our hierarchy above regular monos, with adhesive above pre-adhesive. However, it is not clear what to do for isomorphisms (Figure 2). Indeed, declaring adhesive morphisms below isomorphisms would require us to update the definition of isomorphism to include the mixins of adhesive and pre-adhesive morphisms. While it is possible to reorganize the code in this way, it is not very satisfactory: since adhesive morphisms are rather specific, we wish to be able to treat the previous hierarchy of epis and monos as a library, and adhesive morphisms as an optional module that we can plug in. We are thus left with two options:

1. Declaring isomorphisms as instances of adhesive morphisms: This gives us the ability to use isomorphisms where adhesive morphisms are expected, but breaks the forgetful inheritance policy of HB. In fact, with

<figure><img src="image_6.png" /><figcaption>**Figure 2.** The extended hierarchy of morphisms: with non-forgetful inheritance (top) or with extended isomorphisms (bottom).</figcaption></figure>

such an instance declaration, HB has two ways of equipping an isomorphism with the mixin of, say, a regular mono: either by direct containment, or by using the proofs that it is adhesive, and thus pre-adhesive, and thus a regular mono. Since these two paths have no particular reason to be equal, this could lead to problematic situations where statements holding along one path cannot be used in contexts mentioning the other. Therefore HB rejects such a definition.

2. Adding a new isomorphism structure (Iso'), inheriting from both original isomorphisms and adhesive morphisms. Proceeding in this way, we comply with forgetful inheritance, but we sometimes need to explicitly promote isomorphisms from the core library to isomorphisms from the extended one. This can be done easily using an empty factory, but it nevertheless induces some overhead, and we would have to
introduce new copies whenever we need new classes of morphisms below isomorphisms.

We have chosen the second approach for the time being, hoping that more satisfactory solutions can be designed in the future to deal with this form of inheritance a *posteriori*.

## 3.2 Subobjects

We shall also need the notion of *subobject*, which is a categorical generalization of set-theoretic inclusions. Given an object *X* in a category *C*, *subobject* is a mono *m*: *A* ↪→ *X*. Subobjects form a category where morphisms from *m*: *A* ↪→ *X* to *n*: *B* ↪→ *X* are morphisms *f*: *A* → *B* such that *n* ○ *f* = *m*. When *C* has pullbacks, this category has all products, called *binary intersections*. Coproducts, which do not always exist, are called *binary unions*. A subobject is *regular* if the underlying mono is so.

## 3.3 The hierarchy of adhesive categories

We can now present the three variants of adhesive categories that we have formalized. Each time, we provide the textbook definition—together with alternative characterizations, if any—and explain the choices we make.

**3.3.1 Rm-quasiadhesive categories.** We start with rm-quasiadhesive categories, the least demanding structure in the hierarchy.

**Definition 3.3** (Rm-quasiadhesive category [15]). A category is *rm-quasiadhesive* iff

* it has all pullbacks,

* it has pushouts along regular monos,

* pushouts along regular monos are stable, and

* pushouts along regular monos are pullbacks.

Since having all pullbacks—which means that every cospan has a pullback—is a common requirement, we first define a structure *CatPb* for those categories; and, similarly, we define a structure *CatRmPo* for categories with pushouts along regular monos—which means that every span where one of the morphisms is a regular mono has a pushout.

We turn the last two requirements of the definition into a new mixin in order to define the structure *RmQAdhesive*. We see here—in a slightly more sophisticated case than for quivers, precategories and categories—how stronger structures are built in HB by combining independent pieces of weaker structures.

At this point, our hierarchy contains the following dependencies:

<figure><img src="image_7.png" /></figure>

Among the theory of rm-quasiadhesive categories, we proved that regular monos are preserved by composition and thus form a subcategory, that pushouts preserve regular monos, and that regular subobjects do have binary unions (these results are non-trivial, see [15, 23]).

**3.3.2 Rm-adhesive categories.** Rm-adhesive categories (originally named *quasiadhesive* categories in [23]) are the next level in the hierarchy of adhesive category theory.

**Definition 3.4** (Rm-adhesive category [15], [23]). A category is *rm-adhesive* iff:

* it has all pullbacks,

* it has pushouts along regular monos, and

* pushouts along regular monos are Van Kampen.

Note that the first two properties are the same as for rm-quasiadhesive categories; but the third property appears, at first sight, to be unrelated. However, we have:

**Theorem 3.5** ([15, Thm. 3.3.]). In a category *C* with all pullbacks, the following are equivalent:

1. *C* is *rm-adhesive*;

2. regular monos are adhesive, and regular subobjects are closed under binary union;

3. *C* is *rm-quasiadhesive*, and regular subobjects are closed under binary union.

Since there are three equivalent characterizations, we can choose the most convenient one as the native definition. While the first point is the textbook definition, the third point in the above theorem shows that rm-adhesive categories actually are rm-quasiadhesive. We thus take this item as the native definition, to optimize modularity: *RmAdhesive* only adds the property of “closure of regular subobjects under binary union” to *RmQAdhesive*.

In HB terms, this means that the second part of point 3 becomes a mixin, and points 1 and 2 are factories with a dependency on categories with pullbacks, i.e., *CatPb*. The implications 1 ⇒ 3 and 2 ⇒ 3 are proved and declared as builders. This means that they are used by HB as instructions on how to construct the mixins in the hierarchy up to *RmAdhesive*, given the data in either factory. This makes it possible to create instances in three different ways, at the user's convenience.

Conversely, the implications 3 ⇒ 1 and 3 ⇒ 2 can be seen as being part of the theory of rm-adhesive categories. We state and prove these implications as standard Rocq lemmata; they can be applied whenever we have an instance of a rm-adhesive category:

* pushouts along regular monos are exact and thus Van Kampen (the remaining part of implication 3 ⇒ 1);

* regular monos are adhesive (the remaining part of implication 3 ⇒ 2, which in fact is a theorem of rm-quasiadhesive categories).
<figure><img src="image_8.png" /><figcaption>**Figure 3.** Extended hierarchy of categories.</figcaption></figure>

**3.3.3 Adhesive categories.** We finally move to adhesive categories, which form the richest structure in our hierarchy:

**Definition 3.6** (Adhesive category [15]). A category is *adhesive* iff:

* it has all pullbacks,

* it has pushouts along monos, and

* pushouts along monos are Van Kampen.

**Theorem 3.7** ([15, Thm. 3.2] and [23, Prop. 6.2]). *In a category C with all pullbacks, the following statements are equivalent:*

1. C is adhesive;

2. all monos are adhesive;

3. C has pushouts along monos, those pushouts are stable and are pullbacks;

4. C is rm-adhesive and all monos are regular.

5. C is rm-quasiadhesive and all monos are regular.

(The fifth point is not mentioned in the above references; it follows from the third item of Theorem 3.5: unions of regular subobjects exist and are monos in rm-quasiadhesive categories, hence regular monos here.) We see from this theorem that adhesive categories are rm-adhesive, and that they have pushouts along all monos. The latter requirement is quite common so that we make it into a structure CatMPo, above CatRmPo. Then we define adhesive categories as rm-adhesive categories with pushouts along all monos and where all monos are regular. The hierarchy we obtain is depicted in Figure 3. We provide four factories to construct adhesive categories, corresponding to items 1,2,3 and 5 in the above theorem (item 4 being superseded by item 5).

As for rm-adhesive categories, we provide the remaining parts of Theorem 3.7 as standard Rocq lemmata about adhesive categories.

Note that due to forgetful inheritance, there are two functions providing pushouts in the structure CatMPo: along monos

<figure><img src="image_9.png" /><figcaption>**Figure 4.** An example of a production with simple graphs. The edge is deleted, and a new vertex with an edge is added</figcaption></figure>

and along regular monos. While the latter can be deduced from the former, it need not be, and the two functions may return different values on the same input (these values are nevertheless isomorphic, by unicity of pushouts).

To reduce the burden of working explicitly modulo isomorphisms, we carefully write our mixins and statements so that they quantify over all possible pushouts (or other kinds of values in different contexts). For instance the third item in Theorem 3.7 is formally modeled as a function providing some pushout for each span of a mono and a morphism and the property that *all* pushouts along a mono are stable and are pullbacks—not just the ones provided by the function.

# 4 Graph rewriting theory

Adhesive categories and their variants make it possible to establish theorems about graph rewriting systems once and for all, abstracting over the precise choice of graphs (simple, directed, labeled, finite, typed, ...). To check whether our library is mature enough to make it possible to formalize state-of-the art results in this field, we have formalized two important theorems [23, Theorems 7.7 and 7.10]. For lack of space, we do not provide their precise statements here, only their overall nature and the rather small number of lines we need to formalize them.

## 4.1 Elementary notions of DPO graph rewriting

In double-pushout (DPO) graph rewriting, rewriting rules (also called *productions*) consist of a span, the two target objects being the input and the output and the source object being an intermediate state. Such a production is depicted in Figure 4. The intuition for the middle object is that it contains the part of the graph (besides the context) that is preserved by the production, i.e. is neither deleted nor added.

We focus on *linear productions*, in which both morphisms of the span are regular monos.

An application of a rewriting rule is called a *derivation*. Given a production $I \leftarrow K \rightarrow O$ and an object $X$ with a morphism $I \rightarrow X$, a derivation is a diagram of the following shape, where both squares are pushouts.

<figure><img src="image_10.png" /></figure>

Intuitively, the morphism $I \rightarrow X$ indicates how and where the left-hand side of the production matches the input graph
(X), Z is the result of applying the production to X, and
the morphism $O \to Z$ shows that the right-hand side of the
production appears in that graph.

## 4.2 Local Church-Rosser theorem

The first theorem [23, Theorem 7.7] gives a characterization
of the local Church-Rosser property from term rewriting
systems [34].

It links two properties: *parallel* and *sequential* indepen-
dence. The first is a property on two derivations starting
from the same graph, stating that neither of them deletes the
part on which the other production applies. The second is
also a property on two derivations, where the second produc-
tion is applied to the output of the first derivation, stating
that the second production neither needs nor deletes what
the first production has added to the graph.

The theorem states that the two properties are equivalent.
Since parallel independence is symmetric, it is equivalent
to sequential independence with the productions in either
order. This enables notably the definition of equivalence of
derivations in graph grammars and of canonical derivations
for each equivalence class [22].

The proof in [23] is written for rm-adhesive categories,
but it applies to rm-quasiadhesive categories. The statement
and its proof take 2 pages on paper, with diagrams involving
up to 11 objects. Thanks to our library, our formalization
took just 80 lines of statements and 78 lines of proof.

## 4.3 Concurrency theorem

The concurrency theorem [23, Theorem 7.10] determines
when and how we can *compose* two productions into a new
one inducing the same derivations as the two productions
applied sequentially. Again this possibility is useful in mod-
eling tools as it enables the grouping of a collection of small
rules into a single larger one, e.g., to represent a complex
refactoring operation in model-based software engineering
[18] as a single atomic operation.

Like above, the proof given in [23] for rm-adhesive categories carries over to rm-quasiadhesive categories. The statement and its proof take 2.5 pages on paper, with diagrams involving up to 19 objects. We formalized it with 107 lines of statements and 105 lines of proof.

# 5 Instances

Now we discuss the key instances we have formalized: types,
setoids, finite types, simple graphs, slice and functor cate-
gories. In each case, we discuss the required type-theoretic
axioms, if any.

## 5.1 Types and functions

We have proven that the category Types with Type as the
type of objects and extensional functions as morphisms<fnref n="4" />

is adhesive. This is the counterpart in type theory of the
category of sets and functions in set theory. We use the third
item of Theorem 3.7 to construct this adhesive category.
Proving that it has all pullbacks is easy, but constructing and
analyzing pushouts is more difficult.

The pushout of two morphisms $f: C \to A$ and $g: C \to B$
can be computed by first taking the disjoint union of A and
B, then quotienting it by the smallest equivalence relation $R$
such that $(f \circ g) R (g \circ f)$ for all $c \in C$.

<figure><img src="image_11.png" /></figure>

In order to build quotient types and to define the coprojec-
tions of the pushout, we have taken a file written by Arthur
Azevedo de Amorim [12]. This implementation relies on the
following standard axioms<fnref n="5" />:

* Predicate extensionality, which states that two point-wise equivalent predicates are equal.

predicateExtensionality:
∀A (P : A → Prop), (∀a, P a ↔ Q a) → P = Q.

* Constructive definite description, which is a form of choice, stating that, if there exists a unique object satisfying a predicate in *Prop*, then we can extract a witness in *Type*.

constructive_definite_description :
∀A (P: A → Prop), (∃!x, P x) → {x | P x}

It should be noted that we are building all pushouts, while
the proof that a category is adhesive only requires pushouts
along monos (injective functions in the case of sets). If *f*
is injective, this leads to a simplification of the relation *R*:
the equivalence classes are either singletons {*a*}, for any
*a* ∈ *A* that is outside of the image of *f*, or contain exactly one
element of *B*. This means we can have a canonical element for
each equivalence class. However, computing this canonical
element for elements of *A* requires computing their inverse
image under *f*, and we have not found a way to do that with
a weaker system of axioms.

Predicate extensionality implies proof irrelevance, which
we need to obtain pullbacks in this category (for unicity of
the mediating arrow). Moreover, we use constructive definite
description to prove that pushouts along monos are stable
and are pullbacks. Conversely, we have shown that under
proof irrelevance, the requirement of adhesive categories that
all monos are regular, in Types, is equivalent to constructive
definite description.

<footnote n="4">⁴More precisely, morphisms are functions, but we compare them pointwise.</footnote>

<footnote n="5">⁵The original file makes use of functional and propositional extensionality, but predicate extensionality happens to be sufficient.</footnote>
## 5.2 Setoids and extensional functions

A standard technique to avoid extensionality axioms in type theory consists in replacing types with setoids: types together with a user-defined equivalence relation. Morphisms of setoids are functions between the underlying types that map equivalent elements to equivalent elements. We prove that the corresponding category Setoids, where morphisms are declared equivalent when they are pointwise equivalent as functions, is adhesive.

Equipping this category with pullbacks and pushouts is easy, this time without any axiom since we get to choose how to compare elements when we define the object. Proving that pushouts are stable and that pushouts along regular monos are pullbacks is slightly harder, but there also we do not need any axiom. Therefore, Setoids is rm-quasiadhesive.

To further establish that it is rm-adhesive (resp. adhesive) it suffices by Theorem 3.5 (resp. 3.7) to prove that regular subobjects are closed under union (resp. that all monos are regular). We have proven the following equivalences:

* regular subobjects are closed under union in Setoids iff disjunctions can be lifted to sums:

$$ \forall P Q: \mathbf{Prop}, P \lor Q \rightarrow P + Q $$

* monos are regular in Setoids iff constructive indefinite description (CID) holds:

$$ \forall A (P: A \rightarrow \mathbf{Prop}), (\exists x, P x) \rightarrow \{x \mid P x\} $$

The latter property is a standard axiom; it is stronger than constructive definite description (CDD) in that it does not require unicity of the witness; the former property also follows from it (by taking $A = 2$).

Therefore, while we had to use predicate extensionality and CDD from the beginning with the category Types, we could add axioms progressively with the category Setoids: nothing for rm-quasiadhesivity, lifting of disjunctions to sums for rm-adhesivity, and CID for adhesivity.

In particular, since the Church-Rosser and the concurrency theorems hold in rm-quasiadhesive categories, we get them in Setoids without any axiom.

## 5.3 Finite types and functions

When we restrict to finite types, we can get an adhesive category finTypes without using any axiom. We formalize it using the finite types and functions from the mathcomp library [26], which is perfectly well-suited for our needs.

In order to factorize the code, we use the functor from finTypes to Setoids which maps a finite set to itself, together with propositional equality. Being full and faithful, this functor reflects pushouts and pullbacks; it moreover preserves (regular) monos, pushouts, and pullbacks. Therefore, we can use it to import properties like (rm-(quasi))adhesivity of Setoids to finTypes.

<figure><img src="image_12.png" /><figcaption>Figure 5. SGraphs is not rm-adhesive.</figcaption></figure>

Since we want this instance to be axiom-free, we only prove rm-quasiadhesivity in this way, and we prove separately that all monos are regular in finTypes.

We could not proceed in this way for the category Types: CID seems to be necessary to prove that the corresponding functor preserves pushouts—even only those along regular monos. Since CID is not necessary for Types to be adhesive, this approach would be sub-optimal. We have also proved that the categories Types and Setoids are equivalent, assuming predicate extensionality and CID; this combination of axioms is known to entail excluded middle in Type; we do not know if it is necessary to prove this equivalence of categories.

## 5.4 Directed simple graphs

A directed simple graph is a set of vertices equipped with a binary relation of edges. (We allow self-loops for simplicity.) We obtain a category SGraphs by considering graph homomorphisms, i.e., functions preserving the edges: given a graph $(V_1, E_1)$ and a graph $(V_2, E_2)$, a morphism $f: V_1 \rightarrow V_2$ must satisfy: $\forall x, y \in V_1, x \in E_1, y \in E_2 \Rightarrow (f(x) \in E_2, f(y))$.

Note that Setoids is not the subcategory of simple graphs whose edges form equivalence relations: graph homomorphisms are compared pointwise but strictly, while setoid morphisms are compared pointwise and up to the target relation.

SGraphs is rm-quasiadhesive [5]; we prove this in Rocq by reusing the fact that Types is adhesive, and checking that the various produced functions preserve edges.

SGraphs is not rm-adhesive, however, because the pushout operation loses information on the multiplicity of edges between two vertices. Figure 5 gives a concrete counterexample: a pushout along a mono which is not a pullback.

## 5.5Functor and presheaf categories

Given categories C and D, the category of functors from C to D and natural transformations has all pullbacks if D has all pullbacks, and is adhesive if D is adhesive. As for slice categories, the main part of the proof is to transfer pullbacks, monos and so on from natural transformations
to their components and vice-versa. Proving that a natural
transformation has a property if all of its components have it
is generally straightforward; however the converse is often
more complicated. If we have a pullback of natural transfor-
mations for example, we cannot use its universal property
on one of its components. We can however use the unicity
of pullbacks along with the fact that canonical pullbacks are
built component-wise, but this requires having a canonical
pullback in the first place. Many of those proofs thus require
to have D a category with all pullbacks.

A similar issue arises for monos: we cannot directly prove
that if a natural transformation is a mono then all of its
components are. In this case, contrary to pullbacks, there is
no notion of a category “having all monos”. We can however
use the fact that being a mono is equivalent to having a trivial
kernel pair (any pullback of a mono along itself is a span of
identical isomorphisms) and then use the proof for pullbacks.
This is the proof from [7, Cor. 2.15.3]. The same is probably
true for regular monos, but would require a similar link with
limits. Proving it would allow us to declare categories of
functors as rm-(quasi)adhesive whenever D is. We leave this
for future work.

Using this instance combined with the **Types** (or **Setoids**) instance, we deduce that the category (*C*<sup>*op*</sup> → **Types**) (or (*C*<sup>*op*</sup> → **Setoids**)*) of presheaves on an arbitrary category **C** is adhesive. This includes the category **MGraphs** of directed multigraphs [5], by instantiating **C** with the category with two objects and two parallel arrows between them. Similarly for finite presheaves (*C*<sup>*op*</sup> → **finTypes**), and thus finite directed multigraphs, without using any axiom.

**5.6 Slice/over categories**

Given an object $X$ in a category $C$, we can define the *slice* category $C/X$. Its objects are the morphisms $f: A \to X$; a morphism from $f: A \to X$ to $g: B \to X$ is a morphism $h: A \to B$ in $C$ such that $f = g \circ h$. (Subobjects of $X$ actually form a subcategory of $C/X$.)

For any instance C of a structure of the hierarchy of categories and any $X \in C$, the slice $C/X$ is an instance of the same structure as C, i.e., the slice is rm-adhesive if the category is rm-adhesive, etc. The proofs mainly consist of lemmata to transfer pullbacks, pushouts, monos and regular monos to and from the slice.

This construction is a useful source of additional concrete
models. For example, the category Types/X is the category of
(intensional) multisets over X; and, for a chosen category of
graphs, the slice category of X is the category of graphs *typed*
by X, i.e. each node of X defines a type and its edges define
the permitted edges, so that an object of this slice category is
a graph respecting the typing constraints and the morphisms
between graphs are those that preserve types [13]. The gen-
eral theory of categorical graph transformations thus lifts
immediately to these richer—and practically useful—settings.

# 6 Discussion

**6.1 Code**

The library consists of about 10k lines of code in total. About 5100 are for the preliminaries and general category part (setoids, categories, pushouts, isomorphisms, functors, etc.), 2400 for the theory of adhesive categories (Van Kampen squares, adhesive morphisms, subobjects, rm-quasiadhesive categories, etc.), 400 for the Church-Rosser and concurrency theorems, and 2100 for the various instances. The development is axiom-free, except for the proofs that the categories of types and setoids are adhesive (see Sections 5.1 and 5.2).

**6.2 Setoids and $\mathcal{E}$-categories**

As explained in Section 2.1, we formalize $\mathcal{E}$-categories rather
than categories: homsets are setoids. The concepts of cate-
gories scale smoothly to $\mathcal{E}$-categories: it suffices to

* replace all occurrences of propositional equality (=) between morphisms by setoid equivalence (≡)

* require that all functions between homsets preserve these equivalences (e.g., composition, or the action of a functor on morphisms).

* define appropriate equivalence relations on morphisms whenever we define a category, e.g., compare natural transformations via their components (ignoring naturality proofs), slice morphisms via their underlying morphisms, functions in Types pointwise, etc.

(The latter point regularly simplifies proofs, as equality most
often *reduces* to the expected property.)

This design choice saves us from having to use axioms
to build explicit quotients: beyond the case of functors and
functor equivalence from Section 2.1, there is also that of
regular monos and other classes of morphisms: while the
requirements for being regular carry computational content
and should be in Type (so we can build on this content to con-
struct pushouts, for instance), we want to ignore this content
when comparing regular morphisms. This is straightforward
to do, in an axiom-free manner, with the proposed setup.

The price to pay is that we systematically have to prove
that concepts are preserved under equivalence of morphisms.
To this end, we use the setoid rewriting tools of Rocq [31].
For instance, we state, prove and use lemmata such as

Instance isPullbackE {C: Cat} {A B C D: C}:
CMorphisms.Proper (eqv= eqv= eqv= eqv= iffT)
(@isPullback C A B C D).

that says that being a pullback square is closed under mor-
phism equivalence (eqv). Since being a pullback carries com-
putational content, it is a property in Type, hence the use
of CMorphisms.Proper and iffT rather than the more usual
Proper and iff for relations in Prop. Rocq’s support for setoid
rewriting in Type is however less robust than that in Prop,
and this requires some occasional unpleasant hacking if the
rewrite tactic fails to use the above instance automatically.
## 6.3 Report on the usability of Hierarchy Builder

HB turned out to be very convenient for the present work, and our evaluation is overall quite positive. It enables us to set up our hierarchies cleanly and efficiently, without having to tweak canonical structures or typeclass inference manually. Below we list suggestions to further improve it.

**Universe polymorphism.** Universe polymorphism is not yet supported by HB, so that we had to duplicate the setoid structures in order to avoid universe inconsistencies when defining the category *Setoids*: small setoids, which are the objects of this category, and large setoids, which are used for the homsets of our $\mathcal{E}$-categories. Since Rocq already has support for universe polymorphic records, we do not see any major obstacles and hope that this restriction will be lifted in the near future by developers of HB.

**Dynamic hierarchies.** A notable phenomenon with our hierarchy of morphisms (Figure 2) is that some classes collapse when going up the hierarchy of categories. For example, in an adhesive category, every mono is adhesive (and thus regular). HB does not currently support such dynamic behavior of hierarchies. We use lemmata with adequate dependencies to promote morphisms easily when the conditions are met. Such promotions have to be explicit, however, and it would be interesting to automatize the process.

**Inheritance a posteriori.** Our main concern is the current inability to add downward inheritance relations *a posteriori*, as explained at the end of Section 3.1. Providing solutions to this problem while preserving robustness of inference seems challenging, but it is probably necessary to design and combine large libraries in a modular way.

## 7 Related work

There are many formalizations of category theory in various proof assistants [1, 2, 17, 19, 29, 33, 35, 36, 38–40].

Very few of these libraries define regular monos [19, 35, 39]. The only formalization of adhesive categories of which we are aware is in Lean mathlib [35], where we find the textbook definition, the fact that pushouts along monos yield monos and are pullbacks, and the *Types* and *function* instances. With respect to this library, we develop more concepts (rm-quasiadhesive and rmadhesive categories), we provide alternative presentations of these categories (Theorems 3.5 and 3.7), we prove the local Church-Rosser and Concurrency theorems, and we provide more instances (finite types, setoids, simple graphs, slices). Another important difference is that, like in [19, 40], we work with $\mathcal{E}$-categories to remain axiom-free, while Lean’s mathlib relies on propositional extensionality and a strong form of the axiom of choice, hence classical logic—with excluded middle in *Type*. In particular, they can freely take quotients and they work with strict categories (cf. Section 2.1).

## 8 Future work

It would be nice to set up tools for rewriting modulo associativity of composition (we mention the associativity law 439 times in our development, in explicit rewriting sequences). While it is easy to design a tactic to prove morphism equations modulo associativity of composition and a few other basic laws of category theory, stating these equations is painful so that we would like to implement a matching algorithm to find occurrences modulo associativity and perform the appropriate transitivity steps automatically, along the lines of [8] but for heterogeneous operations such as categorical composition.

Our library contains many lemmata related to isomorphisms: many concepts are defined only up to isomorphism, and it is often possible to introduce, remove or move isomorphisms around (e.g., lemma `isPullback_isA` from Section 2.4). Unfortunately, their use still induces increased complexity, compared to paper proofs where isomorphisms are often handled implicitly. A typical example can be found in [20, pages 321-322]: “[...] hence $B \approx B'$. In particular, we can erase all the primes from the diagram”. We would like to automate this task and develop a tactic for deleting a given isomorphism, keeping only its source or target object.

For instance, in a goal like

∀ ... A A' (i: A ≈ A') (f: A ⇝ ...) (g: ... ⇝ A), P A f g

we would like to move more or less automatically to the goal

∀ ... A' (f: A' ⇝ ...) (g: ... ⇝ A'), P A' f g

where i and A have been deleted and the types of f and g modified, using appropriate lemmata ensuring P is preserved along isomorphisms. (This is a typical case where it is far easier to work with univalent categories: isomorphisms become propositional equalities and can always be eliminated.)

In the same vein, we need to develop ways of transporting results along equivalences of categories. For example, the category of directed multigraphs can be defined either as a presheaf category (cf. Section 5), or more concretely with any user-given definition for the type of such graphs and the type of morphisms between them. By transporting our adhesivity proof along an equivalence of categories, we would obtain for free the fact that such end-user variants are also adhesive. As mentioned in Section 2.6, there are cases where such tools would help for duality: sometimes we cannot get duality definitionally but only up to categorical equivalence. A challenge here is to be able to transport computational content in a sensible way.

Finally, having a tool to display graphically the diagram currently being worked on would make the proof process easier—even just in read-only mode, unlike in the work of Ambroise Lafont [24], whose more ambitious objective is to perform proofs graphically.

**Acknowledgments.** We would like to thank Cyril Cohen and Kazuhiko Sakaguchi for many helpful discussions on the
subject of this paper and on Hierarchy Builder generally. This
work was partially funded by the ANR project CoREACT:
Coq-based Rewriting: towards Executable Applied Category
Theory (ANR-22-CE48-0015).

References

[1] The 1Lab Development Team. 2024. *The 1Lab*. https://1lab.dev

[2] Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. 2015. Univalent Categories and the Rezk Completion. *Mathematical Structures in Computer Science* 25, 5 (June 2015), 1010–1039. doi:10.1017/S0960129514000486

[3] Jakob L. Andersen, Christoph Flamm, Daniel Merkle, and Peter F. Stadler. 2016. A Software Package for Chemically Inspired Graph Transformation. In *Graph Transformation. ICGT 2016 (LNCS, Vol. 9761)*, Rachid Echahed and Mark Minas (Eds.). Springer, Cham, 73–88. doi:10.1007/978-3-319-40530-8_5

[4] Anne Baanen. 2025. Use and Abuse of Instance Parameters in the Lean Mathematical Library. *J. Autom. Reason.* 69, 1 (2025), 1. doi:10.1007/S10817-024-09712-7

[5] Nicolas Behr, Russ Harmer, and Jean Krivine. 2023. Fundamentals of Compositional Rewriting Theory. *Journal of Logical and Algebraic Methods in Programming* 135 (2023), 100893. doi:10.1016/j.jlamp.2023.100893

[6] Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. 2022. String Diagram Rewrite Theory I: Rewriting with Frobenius Structure. *J. ACM* 69, 2 (March 2022), 14:1–14:58. doi:10.1145/3502719

[7] Francis Borceux. 1994. *Handbook of Categorical Algebra: Volume 1: Basic Category Theory*. Encyclopedia of Mathematics and Its Applications, Vol. 1. Cambridge University Press. doi:10.1017/CBO9780511525858

[8] Thomas Braibant and Damien Pous. 2011. Tactics for Reasoning Modulo AC in Coq. In *Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 7086)*, Jean-Pierre Jouannaud and Zhong Shao (Eds.). Springer, 167–182. doi:10.1007/978-3-642-25379-9_14

[9] Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. 2020. Hierarchical Builder: Algebraic Hierarchies Made Easy in Coq with Elpi. In *FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 167)*. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 34:1 – 34:21. doi:10.4230/LIPIcs.FSCD.2020.34 https://github.com/math-comp/hierarchy-builder.

[10] Andrea Corradini and Fabio Gadducci. 2005. On Term Graphs as an Adhesive Category. *Electronic Notes in Theoretical Computer Science* 127, 5 (May 2005), 43–56. doi:10.1016/j.entcs.2005.02.014

[11] Vincent Danos, Russ Harmer, and Glynn Winskel. 2013. Constraining Rule-Based Dynamics with Types. *Mathematical Structures in Computer Science* 23, 02 (April 2013), 272–289. doi:10.1017/S0960129512000114

[12] Arthur Azevedo de Amorim. 2024. Poleiro. https://github.com/arthuraa/poleiro

[13] H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer. 2006. *Fundamentals of Algebraic Graph Transformation*. Springer, Berlin, Heidelberg.

[14] François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. 2009. Packaging Mathematical Structures. In *Theorem Proving in Higher Order Logics. TPHOLs 2009*, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). Springer, Berlin, Heidelberg, 327–342. doi:10.1007/978-3-642-03359-9_23

[15] Richard Garner and Stephen Lack. 2012. On the Axioms for Adhesive and Quasiadhesive Categories. *Theory and Applications of Categories* 27 (May 2012), 27–46. http://tac.mta.ca/tac/volumes/27/3/27-03abs.html

[16] Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. 2013. A Machine-Checked Proof of the Odd Order Theorem. In *Interactive Theorem Proving. ITP 2013 (LNCS, Vol. 7998)*, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer, Berlin, Heidelberg, 163–179. doi:10.1007/978-3-642-39634-2_14

[17] Jason Gross, Adam Chlipala, and David I. Spivak. 2014. Experience Implementing a Performant Category-Theory Library in Coq. In *Interactive Theorem Proving. ITP 2014 (LNCS, Vol. 8558)*, Gerwin Klein and Ruben Gamboa (Eds.). Springer, Cham, 275–291. doi:10.1007/978-3-319-08970-6_18

[18] Reiko Heckel and Gabriele Taentzer. 2020. *Graph Transformation for Software Engineers: With Applications to Model-Based Development and Domain-Specific Language Engineering*. Springer International Publishing, Cham. doi:10.1007/978-3-030-43916-3

[19] Jason Z. S. Hu and Jacques Carette. 2021. Formalizing Category Theory in Agda. In *Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021)*. Association for Computing Machinery, 327–342. doi:10.1145/3437992.3439922

[20] Peter T. Johnstone, Stephen Lack, and Pawel Sobociński. 2007. Quasitoposes, Quasiadhesive Categories and Artin Glueing. In *Algebra and Coalgebra in Computer Science. CALCO 2007 (LNCS, Vol. 4624)*, Till Mossakowski, Ugo Montanari, and Magne Haveraaen (Eds.). Springer, Berlin, Heidelberg, 312–326. doi:10.1007/978-3-540-73859-6_21

[21] Yoshiki Kinoshita. 1997. A bicategorical analysis of Categories. https://www.researchgate.net/publication/2710125_A_bicategorical_analysis_of_E-categories

[22] H. J. Kreowski. 1977. Transformations of derivation sequences in graph grammars. In *Fundamentals of Computation Theory. FCT 1977 (LNCS, Vol. 56)*, M. Karpiński (Ed.). Springer, Berlin, Heidelberg, 275–286. doi:10.1007/3-540-08442-8_94

[23] Stephen Lack and Pawel Sobociński. 2005. Adhesive and quasiadhesive categories. *RAIRO - Theoretical Informatics and Applications* 39, 3 (July 2005), 511–545. doi:10.1051/ita:2005028

[24] Ambroise Lafont. 2024. A Diagram Editor to Mechanise Categorical Proofs. In *35es Journées Francophones Des Langages Applicatifs (JFLA 2024)*. Saint-Jacut-de-la-Mer, France. https://hal.sciences/hal-04407118

[25] Assia Mahboubi and Enrico Tassi. 2013. Canonical Structures for the working Coq user. In *Interactive Theorem Proving. ITP 2013 (LNCS, Vol. 7998)*, Sandrine Blazy, Christine Paulin, and David Pichardie (Eds.). Springer, Berlin, Heidelberg, 19–34. doi:10.1007/978-3-642-39634-2_5

[26] Assia Mahboubi and Enrico Tassi. 2022. *Mathematical Components. Zenodo*. doi:10.5281/zenodo.3999478 With contributions by Yves Bertot and Georges Gonthier. Version 1.0.2.

[27] Benjamin C Pierce. 1991. *Basic Category Theory for Computer Scientists*. MIT Press. doi:10.7551/mitpress/1524.001.0001

[28] Damien Pous. 2013. Kleene Algebra with Tests and Coq Tools for While Programs. In *Interactive Theorem Proving. ITP 2013 (LNCS, Vol. 7998)*, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer, Berlin, Heidelberg, 180–196. doi:10.1007/978-3-642-39634-2_15

[29] Egbert Rijke, Elisabeth Stenholm, Jonathan Prieto-Cubides, Fredrik Bakke, Vojtěch Štěpančík, and others. [n. d.]. *The agda-unimath library*. https://github.com/UniMath/agda-unimath/

[30] Grzegorz Rozenberg. 1997. *Handbook of Graph Grammars and Computing by Graph Transformation*. Vol. 1. https://www.worldscientific.com/worldscibooks/10.1142/3303

[31] Matthieu Sozeau. 2009. A New Look at Generalized Rewriting in Type Theory. *J. Formaliz. Reason.* 2, 1 (2009), 41–62. doi:10.6092/ISSN.1972-5787/1574

[32] Bas Spitters and Eelis Van Der Weegen. 2011. Type classes for mathematics in type theory. *Mathematical Structures in Computer Science*
21, 4 (2011), 795–825. doi:10.1017/S0960129511000119

[33] Eugene W. Stark. 2016. Category Theory with Adjunctions and Limits. *Archive of Formal Proofs* (June 2016). https://www.isa-afp.org/entries/Category3.html

[34] TeReSe. 2003. *Term Rewriting Systems*. Cambridge University Press.

[35] The mathlib Community. 2020. The Lean Mathematical Library. In *Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020)*. Association for Computing Machinery, 367–381. doi:10.1145/3372885.3373824

[36] Amin Timany and Bart Jacobs. 2016. Category Theory in Coq 8.5. In *1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 52)*, Delia Kesner and Brigitte Pientka (Eds.). Schloss

Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 30:1–30:18. doi:10.4230/LIPIcs.FSCD.2016.30

[37] Djordje Čubrić, Peter Dybjer, and Philip Scott. 1998. Normalization and the Yoneda embedding. *Mathematical. Structures in Comp. Sci.* 8, 2 (April 1998), 153–192. doi:10.1017/S0960129597002508

[38] Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2021. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. *Journal of Functional Programming* 31 (2021), e8.

[39] Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et al. 2015. UniMath — a Computer-Checked Library of Univalent Mathematics. https://github.com/UniMath/UniMath

[40] John Wiegley. 2014–2018. Category Theory in Coq. https://github.com/jwiegley/category-theory