How to prove equations using diagrams, part 1

Initial functors

This post is cross-posted at the Topos Institute blog.

An e-graph, short for “equality graph,” is a data structure that maintains a congruence relation on expression trees: an equivalence relation stable under forming new expressions. First devised by Nelson and Oppen in 1980 (Nelson 1980; Nelson and Oppen 1980), e-graphs received a surge of new attention when Willsey et al demonstrated, via their software package egg, that e-graphs combined with equality saturation can be a fast, powerful, and adaptable tool for equational reasoning (Willsey et al. 2021). In my own work on CatColab, I’ve begun using egg’s successor, egglog (Zhang et al. 2023), to reason about finitely presented categories.

Standard presentations, beginning with Nelson’s PhD thesis (Nelson 1980), emphasize the data structures and algorithms needed to implement e-graphs, such as the union-find data structure. It’s crucial that work in computer algebra ultimately touch the ground in this way. Still, I can’t help but wonder what, abstracted from the implementation details, is really going on with e-graphs. The diagrammatic and visual nature of e-graphs, so apparent in the interactive egglog demo, will suggest to any category theorist that categorical ideas may be implicitly at work.

Two groups have recently proposed categorical semantics for e-graphs (Biondo, Castelnovo, and Gadducci 2025; Tiurin et al. 2025). Without going into specifics, both define an “e-hypergraph” to be a labeled hypergraph equipped with extra structure that, directly or indirectly, specifies an equivalence relation. Their starting point is to say what an e-graph is. Though I’ll eventually propose my own definition of an “e-diagram,” I will start by considering how e-graphs are manipulated, with the ultimate aim being to give an categorical and operational semantics for e-graph computation. The key concept will be that of an initial functor.

In this post, I’ll introduce the main ideas for categories without further structure. In comparison with e-graphs, this will be quite restrictive—it will correspond to allowing only unary function symbols—but it has the advantage of bringing us to the point with a minimum of setup. In future posts, we’ll generalize to categories with finite products and recover the standard setting of e-graphs.

Representing equations using diagrams

If you’ve encountered any abstract algebra, you’ve likely seen how category theorists represent equations between morphisms by drawing commutative diagrams. For example, saying that a square of morphisms

in some category commutes means that equation $g\circ f=k\circ h$ holds.

Let’s recall the formal definitions, which are standard if not without fine distinctions.

Definition 1 A diagram in a category $\mathsf{C}$ is a functor $D:\mathsf{J}\to \mathsf{C}$ whose domain $\mathsf{J}$, the indexing category or shape of the diagram, is a small category. Further terminology:

• the diagram is free if its shape is a free category, i.e., $\mathsf{J}=\mathrm{Path}(G)$ is freely generated by a (possibly infinite) graph $G$;
• the diagram is finitely presented if its shape is a finitely presented category;
• the diagram commutes, or is commutative, if for every pair of morphisms in $\mathsf{J}$ with the same domain and codomain, their images in $\mathsf{C}$ are equal.

Note that a diagram may well be both free and commutative: freeness is a property solely of the diagram’s shape, whereas commutativity also crucially concerns the diagram’s image in the target category.

In practice, we work with diagrams that are free and finitely presented. That means that the diagram’s shape is freely generated by a finite graph, a data structure easily implemented on a computer. When doing computer algebra, the target category will itself be finitely presented by generators and relations. Initially, the only equations that we “know” are the ones explicitly given as relations. Our aim is to derive further equations in the target category by manipulating diagrams in it.

But wait: if a diagram in a finitely presented category can be described using only graph-theoretic concepts, familiar to any computer scientist, what is the point of introducing categories and functors? We’ll see that category theory is indispensable for concisely describing the valid manipulations of diagrams. These manipulations take the form of morphisms between diagrams, which are in the first instance functors.

Initial functors

Reasoning with diagrams, or “diagram chasing,”¹ is the art of transforming a given diagram, say $D:\mathsf{J}\to \mathsf{C}$, into another diagram $D^{\prime }:{\mathsf{J}}^{\prime }\to \mathsf{C}$, following certain rules of inference. In ordinary mathematical practice, nobody bothers to say what these rules are. We aim to be more systematic.

Let’s consider the obvious moves we could make. Given a diagram $D:\mathsf{J}\to \mathsf{C}$, we could pull it back along a functor $R:{\mathsf{J}}^{\prime }\to \mathsf{J}$ to obtain another diagram $D^{\prime }:=D\circ R:{\mathsf{J}}^{\prime }\to \mathsf{C}$. Conversely, we could extend the diagram $D$ by finding a functor $R:\mathsf{J}\to {\mathsf{J}}^{\prime }$ and along with a diagram $D^{\prime }:{\mathsf{J}}^{\prime }\to \mathsf{C}$ such that $D=D^{\prime }\circ R$:

Without assuming more, neither contemplated rule of inference is valid in the sense (to be made precise) of exactly preserving solutions to the equations presented by diagrams. For that, we need $R$ to be a special kind of functor, an initial functor, characterized by the following definition/theorem.

Definition

Theorem 1 (Initial functors) A functor $R:\mathsf{J}\to \mathsf{K}$ is initial, here denoted $R:\mathsf{J}\twoheadrightarrow \mathsf{K}$, if any of the following equivalent conditions hold:

• Pullback along $R$ preserves limits: if $\mathsf{C}$ is a category and $D:\mathsf{K}\to \mathsf{C}$ is a diagram in $\mathsf{C}$, then the canonical morphism between limits $$\underset{\mathsf{K}}{lim}D\to \underset{\mathsf{J}}{lim}(D\circ R)$$ is an isomorphism, whenever the limits in question exist.
• Pullback along $R$ preserves limits of sets: if $D:\mathsf{K}\to \mathsf{Set}$ is a diagram of sets, then the canonical function between limits $$\underset{\mathsf{K}}{lim}D\to \underset{\mathsf{J}}{lim}(D\circ R)$$ is a bijection.
• Slices relative to $R$ are connected: for any object $k\in \mathsf{K}$, the comma category $R/k$ is non-empty and connected.²

For a proof of (the dual of) this equivalence, see (Riehl 2014, Lemma 8.3.4).

With a good intuition for limits, the limit characterization of initiality is useful because you can often see at a glance whether a given functor is initial just by imagining what will happen to a limit of sets. On the other hand, the slice characterization is useful in being concrete and syntactical. Recall that, given a functor $R:\mathsf{J}\to \mathsf{K}$ and an object $k\in \mathsf{K}$, the comma category $R/k$ has

• as objects, an object $j\in \mathsf{J}$ together with a morphism $f:R(j)\to k$ in $\mathsf{K}$;
• as morphisms $(j,f)\to (j^{\prime },f^{\prime })$, morphisms $h:j\to j^{\prime }$ in $\mathsf{J}$ making the triangle commutes:

In the typical case that the categories involved are free and finitely generated, proving initiality—checking that each comma category $R/k$ is non-empty and connected—thus reduces to a combinatorial problem.

Interpretation

Why are initial functors relevant to equational reasoning? In general, a limit of a diagram can be thought of as an object representing all possible solutions to the equations postulated by the diagram. This interpretation is clear in the ur-category $\mathsf{Set}$, where a general formula gives the limit of a diagram of sets as the subset of all tuples of elements obeying equations indexed by the shape’s morphisms. Namely, a limit of a diagram $D:\mathsf{J}\to \mathsf{Set}$ is the set of all tuples $(x_j{)}_{j\in \mathsf{J}}$, where $x_j\in D(j)$, such that the equations

$$D(f)(x_i)=x_j,\mathrm{\forall }f:i\to j\text{in}\mathsf{J},$$

are satisfied (Leinster 2014, Example 5.1.22). So, as pullback along an initial functor preserves limits, the initial functors are intuitively those that preserve the “solution set” of the system of equations presented by a diagram.

However, our interest lies in diagrams $D:\mathsf{J}\to \mathsf{C}$ whose target is a finitely presented category $\mathsf{C}$. Such categories rarely have many nontrivial products or equalizers. We can circumvent this problem in two ways.

First, we can always consider set-theoretic interpretations of the presentation, namely functors $F:\mathsf{C}\to \mathsf{Set}$. Then the composite $F\circ D:\mathsf{C}\to \mathsf{Set}$ is a diagram of sets and we are returned to the standard setting where all limits exist. This viewpoint is taken in the e-graph community when they speak of “uninterpreted functions” or “function symbols” (for us, generating morphisms of $\mathsf{C}$). Any equation deduced for uninterpreted functions remains true in any interpretation of them by actual functions between sets. Thus, if you have a formal system of proofs that is complete for equational reasoning with functions, then there exist proofs in that system for equations deduced using initial functors.³

Taking a little extra care, we can go further to deduce equations that hold in an arbitrary category $\mathsf{C}$. Suppose we start with a singleton diagram in $\mathsf{C}$, indexing a single object $X\in \mathsf{C}$. The limit of that diagram exists trivially, being $X$ itself. Thus, any diagram obtained by pulling back or extending the diagram along an initial functor will continue to have $X$ as its limit. In particular, any path in such a diagram originating at $X$ must commute. We will use this technique in the calculations that follow. It will become more powerful when we extend to categories with finite products, since we can then start with any finite discrete diagram, the indexing objects of which act as “free variables.”

Examples and calculations

The remainder of the post will illustrate the concept of initial functor through commonly occurring examples and explicit calculations. The aim is to suggest how initial functors can be deployed for mechanical reasoning with diagrams, deferring to next time a further theoretical development.

Motifs among initial functors

Let’s begin with a few minimal examples of initial functors, acting as motifs or patterns. Each such example will give rise to a rule of inference for diagrammatic reasoning.

The target category $\mathsf{C}$ for the diagrams is fixed throughout. That is, any initial functor should also be a morphism in the category of diagrams in $\mathsf{C}$, the slice category $\mathsf{Cat}/\mathsf{C}$.

• Operation introduction: for any morphism $f:X\to Y$ in $\mathsf{C}$, the map of diagrams

  

  is initial.

• More generally, for any path $X_0\stackrel{f_1}{\to }{X}_1\stackrel{f_2}{\to }\cdots \stackrel{f_n}{\to }{X}_n$ in $\mathsf{C}$, the map of diagrams

  

  is initial.

• Congruence reduction: for any morphism $f:X\to Y$ in $\mathsf{C}$, the map of diagrams,⁴

  

  sending both $y$ and $y^{\prime }$ in the domain shape to $y$ in the codomain shape, is initial.

• Subsuming both operation introduction and congruence reduction, for any morphism $f:X\to Y$ in $\mathsf{C}$ and number $n\ge 0$, the map of diagrams,

  

  sending all of $y_1,\dots ,y_n$ to $y$, is initial.

• Equation introduction: suppose that the equation $g\circ f=k\circ h$ holds in $\mathsf{C}$, as depicted earlier. Then both maps in the span of free diagrams

  

  are initial. More generally, this works for any path equation in $\mathsf{C}$. As another example, we can introduce a nullary path equation, say ${\mathrm{id}}_X=g\circ f$, as:

  

Later, we will formalize not just the rules but how to apply them, using ideas from category-theoretic rewriting. For the moment, we take for granted that when applying the rules in a larger context, the resulting functors are still initial. Or, you can check initiality by inspection in each application.

Pasting commutative squares

We’re ready to do our first calculation, proving the pasting law for commutative squares: that two commutative squares with a common edge can be juxtaposed to produce a commutative rectangle. The notation makes this seem obviously true—that’s what makes it good notation!—but it still needs a proof. We’ll present the proof in a highly mechanical style, where each diagram in the sequence is related to the previous one by an initial functor or, when introducing an equation, by a span of initial functors.

Assume: We are given the two commutative squares

By this we mean, the target category $\mathsf{C}$ is generated by six objects, called $X,X^{\prime },Y,Y^{\prime },Z,Z^{\prime }$, and seven morphisms, called $f,f^{\prime },g,g^{\prime },h,k,\ell$, subject to those two equations.

Construct: Start with the singleton diagram on $X$, whose limit is trivially $X$. Introduce the left- and right-hand sides of the path equation we want to prove:

Recognize the path $X\stackrel{h}{\to }{X}^{\prime }\stackrel{f^{\prime }}{\to }{Y}^{\prime }$ as the left-hand side of the first square, then introduce that equation:

Apply congruence reduction to the occurrences of $f$:

Now recognize the path $Y\stackrel{k}{\to }{Y}^{\prime }\stackrel{g^{\prime }}{\to }{Z}^{\prime }$ as the left-hand side of the second square, then introduce that equation:

We’re already done, but we might as well tidy up by congruence reducing the occurrences of $g$ and then $\ell$:

Conclude: The outer rectangle commutes, since the limit of the diagram is still $X$.

A monoid presentation

Consider a monoid with an element $f$ satisfying the equations

$$f^3=\mathrm{id}=f^5.$$

That is, the target category $\mathsf{C}$ is a generated by a single object, say $\bullet$, and an endomorphism, $f:\bullet \to \bullet$, satisfying those two equations.

Start with the singleton diagram $\{\bullet \}$ and introduce both defining equations, noting that since each equation has an identity on one side, they appear as cycles:

We neglect to label the arrows since they are all over the generating morphism $f$. We’ll now compute the congruence closure, iteratively applying congruence reduction until that is no longer possible. Arrows affected by a congruence reduction are colored the same on either side of the reduction, starting with the two blue arrows above. The first reduction is:

Next:

Congruence reducing three more times gives the sequence:

We could stop here, but we might as well reduce twice more, yielding the diagram that is the self-loop over $f$. We have proved the equation

$$f=\mathrm{id},$$

since the limit of the diagram is the one we started with, namely the unique object $\bullet$. In other words, the monoid presented is actually the trivial monoid. You might remember this is as a special case of the fact in group theory that if a group element $g$ satisfies $g^m=\mathrm{id}=g^n$ for relatively prime numbers $m$ and $n$, then $g=\mathrm{id}$.

Discussion

Category theory is often said to be abstract, even “abstract nonsense,” but it is the interplay between abstract and concrete that gives category theory its power. Initial functors, with their complementary intrinsic and syntactical descriptions, exemplify this interplay.

We’ve begun to explore how initial functors are the basis for an operational semantics for e-graphs. Rather than defining the individual steps and then chaining them together, as in the usual “small-step” operational semantics, we define the valid transformations invariantly via initial functors and then look for useful specializations. Beyond its conceptual content, this flexibility matters because practical systems tend to batch reductions together to improve efficiency. For us, that will often just amount to composing initial functors.

We haven’t yet made a direct connection with e-graphs, though there have been many hints. Another hint is that our final example is lifted directly from Nelson and Oppen’s early work (Nelson 1980; Nelson and Oppen 1980), where it is a running example. In future posts, we’ll tighten up the connection with e-graphs. We’ll also explain how the formalism generalizes to categories with finite products, the categorical counterpart to algebraic theories.

References

Biondo, Roberto, Davide Castelnovo, and Fabio Gadducci. 2025. “EGGs Are Adhesive!” arXiv:2503.13678.

Leinster, Tom. 2014. Basic Category Theory. Cambridge University Press. DOI:10.1017/CBO9781107360068. arXiv:1612.09375.

Nelson, Greg. 1980. “Techniques for Program Verification.” PhD thesis, Stanford University.

Nelson, Greg, and Derek C. Oppen. 1980. “Fast Decision Procedures Based on Congruence Closure.” Journal of the ACM 27 (2): 356–64. DOI:10.1145/322186.322198.

Riehl, Emily. 2014. Categorical Homotopy Theory. Cambridge University Press. DOI:10.1017/CBO9781107261457. https://math.jhu.edu/~eriehl/cathtpy.pdf.

Tiurin, Aleksei, Barrett Chris, Dan R. Ghica, and Nick Hu. 2025. “Equivalence Hypergraphs: DPO Rewriting for Monoidal e-Graphs.” arXiv:2406.15882.

Willsey, Max, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. “Egg: Fast and Extensible Equality Saturation.” Proceedings of the ACM on Programming Languages 5 (POPL): 1–29. DOI:10.1145/3434304. arXiv:2004.03082.

Zhang, Yihong, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, and Max Willsey. 2023. “Better Together: Unifying Datalog and Equality Saturation.” Proceedings of the ACM on Programming Languages 7 (PLDI): 468–92. DOI:10.1145/3591239. arXiv:2304.04332.

Footnotes

1. In this series, we work first with bare categories and later generalize to cartesian categories. Diagram chasing in its most traditional form takes place in additive and abelian categories, a different direction of generalization. It would be fun to try to extend our methods to the additive setting, beginning with categories enriched in commutative monoids or abelian groups.

2. A category is connected if any two of its objects can be connected by a zig-zag of morphisms, i.e., there is an undirected path between them.

3. That is not to say that exhibiting a proof implied by completeness is easy or convenient. As I understand it, proof extraction is a topic of active work in the e-graph community.

4. When drawing a diagram $D:\mathsf{J}\to \mathsf{C}$, the “type-theoretic” notation $x:X$ names an object $x$ in the indexing category $\mathsf{J}$ that is mapped to the object $X$ in the target category $\mathsf{C}$. Thinking of the diagram as a term graph, the object $x$ is indeed a “term of type $X$.”