How to prove equations using diagrams, part 1

E-graphs are data structures that maintain equivalence relations on expression trees and have recently gained attention as powerful tools for equational reasoning, particularly through the software packages egg and egglog. Recent work has proposed categorical semantics for e-graphs by defining "e-hypergraphs" as labeled hypergraphs with extra structure specifying equivalence relations. This post introduces a categorical framework for understanding e-graphs through commutative diagrams and initial functors, starting with the simplified case of unary function symbols before generalizing to more complex settings.