Skip to content

The Agda Universal Algebra Library

A constructive formalization of universal algebra in dependent type theory β€” from signatures, algebras, and homomorphisms to a machine-checked proof of Birkhoff's variety theorem β€” written in literate Agda and type-checked on every commit.

𝖡(𝒦) = 𝖧𝖲𝖯(𝒦)

Get started Browse the library GitHub

283literate modules
38klines of Agda
100%machine-checked
2.8.0Agda Β· stdlib 2.3

Landmark theorems of universal algebra, each formalized and type-checked here β€” follow a face to the proof.

Richard Dedekind Congruence lattices Richard Dedekind Β· 1831–1916 Emmy Noether Homomorphism theorems Emmy Noether Β· 1882–1935 Garrett Birkhoff Subdirect representation Garrett Birkhoff Β· 1911–1996 Anatoly Maltsev Maltsev conditions Anatoly Maltsev Β· 1909–1967 Bjarni JΓ³nsson JΓ³nsson's Theorem Bjarni JΓ³nsson Β· 1920–2016 Alan Day Day's Theorem Alan Day Β· 1941–1990 Garrett Birkhoff Birkhoff's HSP theorem Garrett Birkhoff Β· 1911–1996

What's formalized

The classical-structures layer builds the algebraic hierarchy on the universal-algebra core. Each row is a structure (follow it to its module); each column an equational axiom it satisfies.

StructureAssoc.Comm.Identity InverseIdemp.Absorp.Distrib.
Magma
Semigroup βœ“
Comm. semigroup βœ“ βœ“
Monoid βœ“ βœ“
Comm. monoid βœ“ βœ“ βœ“
Group βœ“ βœ“ βœ“
Abelian group βœ“ βœ“ βœ“ βœ“
Semilattice βœ“ βœ“ βœ“
Lattice βœ“ βœ“ βœ“
Distrib. lattice βœ“ βœ“ βœ“ βœ“
Ring βœ“ βœ“ βœ“ βœ“ βœ“
Comm. ring βœ“ βœ“ βœ“ βœ“ βœ“

Rings carry two operations; coral βœ“ marks an axiom of the additive group, plain βœ“ the shared/multiplicative axioms.

Explore

  •   Quickstart

    Clean checkout to green build in three commands with the pinned Nix toolchain.

    Installation

  •   The canonical library

    Setoid/ β€” algebras as setoids, every definition stated up to the carrier's equivalence.

    Setoid tree

  •   Classic Agda HTML

    Prefer the bare agda-html view? The clickable, fully-highlighted source with Everything as index.

    Browse the source

  •   Where it's going

    The 3.0 reconstruction in milestones M1–M10 β€” classical structures, the Cubical track, corpus artifacts.

    Roadmap

What is this?

agda-algebras is a library of universal algebra developed in Agda, a dependently typed programming language and proof assistant. It defines the core objects of the subject β€” signatures, algebras, homomorphisms, terms, subalgebras, and varieties β€” together with the equational logic that underlies them, and carries each construction all the way to a fully constructive, machine-checked proof of Birkhoff's HSP theorem.

It is developed with two audiences in mind: as a working substrate for research in universal algebra, and as a high-quality, vetted training corpus of Agda proofs for machine learning on formal mathematics. Every page is rendered directly from a literate .lagda.md source the type-checker reads β€” the proof you read is the proof that compiles.

Reading the code

In code blocks, every Agda token is coloured by its role and links to its definition β€” click a function, a Record, a constructor to jump to where it is defined. Press / to search any module; use the edit pencil to view a page's source on GitHub.