How to prove equations using diagrams, part 1

The piece develops a categorical account of diagrammatic equation proving, motivated by e-graphs: data structures that maintain equivalences between expressions and support automated equational reasoning. Rather than begin with implementation details, it asks what makes a transformation of diagrams a valid inference rule. A diagram is a functor from a “shape” category into a target category, and its equations arise when different paths in the shape map to the same morphism. The proposed key tool is an initial functor, a map between diagram shapes whose pullback preserves limits. Since limits of set-valued diagrams encode all assignments satisfying the diagram’s equations, initiality means the transformation preserves exactly the same solutions. Initiality can be checked concretely by verifying that certain comma categories are nonempty and connected, making the criterion amenable to computation.

This framework supports reasoning even when the target is a finitely presented category, which may lack useful limits: diagrams can be interpreted in sets, or a singleton diagram can be transformed while retaining its limit, forcing paths from its object to commute. The piece begins demonstrating inference patterns that arise from initial functors, including introducing an operation as a diagram edge and reducing multiple copies of a shared result through congruence. These patterns explain how diagram transformations can justify equations rather than merely redraw them. The treatment is deliberately limited to categories, corresponding roughly to unary function symbols; later extensions to categories with finite products are intended to recover the richer setting of ordinary e-graphs.