We present a new design for an algebraic simplification library
structured around concepts from universal algebra: theories,
models, homomorphisms, and universal properties of free algebras and
free extensions of algebras.
The library's dependently typed interface guarantees that
both built-in and user-defined simplification modules are terminating,
sound, and complete with respect to a well-specified class of
equations.
We have implemented the design in the Idris 2 and Agda dependently
typed programming languages and shown that it supports modular
extension to new theories, proof extraction and certification, goal
extraction via reflection, and interactive development.