Skip to content

agda-algebras

The Agda Universal Algebra Library, or agda-algebras, is a library that formalizes universal algebra in the Agda proof assistant and programming language.

agda-algebras includes formalizations of general algebras, homomorphisms, congruences, terms, varieties, as well as the equational logic and model theory that underlies universal algebra, all done in pure constructive Martin-Löf type theory with no classical axioms.

One goal of the project is to show that formalizing deep theorems in universal algebra is not only feasible but also practical and relatively painless. To achieve this goal, we used the library to develop a fully constructive, machine-checked proof of Birkhoff's HSP theorem.

The challenge was not the proof of the theorem itself, which has been known since 1935, but rather the fact that a machine will not accept the standard textbook proof. Birkhoff's argument quantifies over all algebras in a class and then builds a free algebra over the carrier of one of them. In predicative type theory those two moves do not live at the same universe level; the formal proof has to say, explicitly and everywhere, at which level each object sits and how to move objects across levels.

The agda-algebras library, the proof of the HSP theorem, and the numbers below are all checkable: the theorem type-checks against Agda 2.8.0 in CI, and the paper is published with a DOI.

With Jacques Carette · 2019– · active
Agda type theory universal algebra setoids

What a machine-checked Birkhoff proof needs that a textbook proof does not

Recall, a variety is a collection of algebras that is closed under the taking of homomorphic images, subalgebras and products. Birkhoff's theorem says a class of algebras is a variety exactly when it is an equational class, the class of all algebras satisfying some set of identities.

The hard direction of Birkhoff's theorem is the assertion that every equational class is a variety. In the library this assertion is formalized as the following type:

Birkhoff : {𝑨 : Algebra a a} → 𝑨 ∈ Mod (Th (V ℓ ι 𝒦)) → 𝑨 ∈ V ℓ ι 𝒦

Read it left to right: if 𝑨 models every identity of the theory of the variety generated by 𝒦, then 𝑨 is already in that variety. This is the textbook inclusion Mod (Th (V 𝒦)) ⊆ V 𝒦, and three things about the formal statement are invisible in the textbook version.

  1. The universe levels are part of the theorem. The private abbreviations a = α ⊔ ρᵃ ⊔ ℓ and ι = ov a are the universe levels at which the proof operates: α is the carrier level of the generating class, ρᵃ the level of its equivalence, ℓ the level of variables.

    𝑨 is pinned to Algebra a a so that its carrier can serve as the generating set of the relatively free algebra 𝔽[ ∣A∣ ], and that free algebra does not fit alongside 𝑨. It lives one universe level higher, at ι = ov a.

    A predicative theory will not let you build a free algebra over a class and keep it at the class's own level, so the proof factors through an explicit lift, Lift-Alg 𝑨 ι ι, whose only job is to move 𝑨 up to where the free algebra lives. Nothing in the textbook proof corresponds to that lift; it exists because the ambient logic is predicative and the paper proof quietly is not.

  2. The "if and only if" is four separate facts. Birkhoff above is one inclusion. Birkhoff-converse is the other. Neither alone says "variety ⟺ equational class"; that also needs

    • the identity-preservation lemma V-id1: if every algebra in 𝒦 satisfies an identity, then so does every algebra in the variety 𝒦 generates, which yields V 𝒦 ⊆ 𝒦 when 𝒦 is an equational class;
    • the expansiveness of V (V-expa : 𝒦 ⊆ V 𝒦).

    Only the four facts together give the theorem. A prose proof gets to call two of those obvious.

  3. It is constructive, and that is a choice with a cost. The proof postulates no function extensionality. That is unusual; extensionality is the standard escape hatch when two functions are provably equal at every argument but not propositionally equal.

    Avoiding function extensionality is well motivated by a desire to keep the proofs computational and composable, and this is a big part of why the library is shaped the way it is.

Why setoids

The library carried two incompatible developments of the same vocabulary through its 2.x line: Base/, which uses propositional equality on raw carrier types, and Setoid/, in which an algebra is a set together with an equivalence relation that its operations must respect.

Both define Algebra, Hom, Con, Subalgebra. Neither could import the other.

Base/ is the easier read, and it is closer to how universal algebra is usually presented in type theory. However, we have frozen the Base layer and recorded our reasoning in the library's Architecture Design Record 001 (ADR-001).

Scale and how to check it

The library's documentation site publishes its own size, and the figure is generated at build time from the source tree rather than typed in. At the time of this writing there are 302 literate Agda modules and roughly 60,000 lines of Agda, counting the canonical tree and excluding the 68 frozen Legacy/ modules.1

The library targets Agda 2.8.0 and the standard library 2.3, both pinned by a Nix flake, and CI type-checks the canonical tree, the frozen legacy tree, and the research certificates on every push.

Artifacts

  • Library source: the 3.0 reconstruction, under active development on master.
  • Documentation site: the rendered library, with every identifier linked to its definition.
  • Birkhoff's HSP theorem, as it is stated and proved: the first proof-of-concept module.
  • TYPES 2021 paper: DeMeo and Carette, A machine-checked proof of Birkhoff's variety theorem in Martin-Löf type theory, LIPIcs vol. 239, pages 4:1–4:21 (the peer-reviewed record of the proof).
  • arXiv:2101.10166: the unabridged 35-page version of the TYPES 2021 paper, which carries the material the proceedings version had to cut.
  • Zenodo deposit — v2.0.1, archived December 2021, the version the TYPES 2021 submission was made against; a new DOI is minted at the 3.0 release.
  • Early formalization notes (2019–2021) — archived on this site at their original URLs. They are where the approach was worked out, and they are superseded by everything above.

What is next

Version 3.0 is a reconstruction rather than a release, and it is not finished.

  • The setoid tree is canonical and the legacy tree is frozen.
  • The new Classical/ layer provides specific theories built on the universal-algebra foundation, each with a Σ-typed core and a record-typed bundle view for standard-library interoperability.
  • A cubical development is the long-term target for 4.0, and is currently a stub.

The honest statement of the library's condition is the one its own ADR makes: the setoid tree was declared canonical before it was self-sufficient, and several of its modules still import basic definitions from the frozen tree. That is type-correct and it is being unwound module by module, but it is the kind of thing a reader deserves to hear from the author rather than discover in the import graph.

The thread worth following from here is the AI tooling built against this library: 60,000 lines of type-checked, human-written Agda with a published theorem at the centre is a rare thing to have, and what it is rare for is training and evaluating machine reasoning on formal mathematics.

  1. That number is reproducible rather than asserted. It counts lines inside the agda code fences of every .lagda.md file under src/ outside Legacy/, and it appears on the documentation landing page, regenerated on every docs build. Recomputing it directly from a clone at the commit this page was written against gives 302 modules and 59,613 lines, which is the same figure. ↩