Skip to content
BranchesTags

Repository files navigation

agda-algebras

CI License: Apache 2.0 Docs License: CC BY 4.0 Agda 2.8.0 stdlib 2.3

A formalization of universal algebra in Agda, built on the Agda standard library. The library defines algebras, homomorphisms, congruences, terms, varieties, and the equational logic that underlies them, with a fully constructive proof of Birkhoff's HSP theorem at the centre. It is being developed both as a working substrate for research in universal algebra and as a high-quality training corpus of Agda proofs for machine learning on formal mathematics.

Status. Version 3.0 is under active reconstruction on master. The library currently targets Agda 2.8.0 and standard-library 2.3. Expect breaking changes until 3.0 is released; see docs/GITHUB_PROJECT.md for the milestone plan and CHANGELOG.md for what has landed so far.

The previous version (called UALib, built against TypeTopology) is no longer maintained but remains available:

Quickstart

From a clean checkout to a green build, assuming Nix with flakes enabled (see INSTALL.md for installation and flake-activation instructions):

git clone https://github.com/ualib/agda-algebras.git
cd agda-algebras
nix develop          # pins Agda 2.8.0 + standard-library 2.3 automatically
make check           # type-check the library and the frozen Legacy tree
make check-all       # (optional) the above plus the FLRP certificate census
make site            # (optional) build the documentation site under ./site

The first nix develop downloads and builds the pinned Agda and standard library (and the MkDocs toolchain); subsequent entries into the shell are essentially instantaneous. Non-Nix installation paths (Agda's PyPI package, prebuilt binaries, cabal from source) are documented in INSTALL.md.

The build has three tiers. make check covers the library and the frozen Legacy/ tree; make check-certificates covers the machine-checked small-lattice representation certificates of the FLRP research track (src/FLRP/Certificates/SmallLatticeReps/), which no library module imports and which cost as much to type-check as the rest of the library put together; make check-all is everything. CI runs all three, the certificates in their own parallel job.

Documentation

Library structure

The 3.0 reconstruction organizes the source tree around a canonical foundation with optional layers built on top of it.

  • src/Setoid/ is the canonical development tree for 3.0. Algebras are sets-with-equivalence (setoids) carrying a signature interpretation that respects the equivalence; homomorphisms preserve both the operations and the equivalence. Definitions are stated in terms of the Algebra.Domain equivalence rather than propositional equality, which makes the eventual port to Cubical Agda largely mechanical.
  • src/Classical/ builds specific algebraic theories — semigroups, monoids, groups, lattices, rings — on the universal-algebra foundation. Core structures are Σ-typed for mathematical elegance, with parallel record-typed bundle views in Classical/Bundles/ for stdlib interop. The scaffold landed under M3-1; concrete structures arrive issue-by-issue under M3-2 onward. See ADR-002 for the design.
  • src/Cubical/ (planned, v4.0, tracked in M5) is the long-term canonical target: cubical-Agda counterparts of the Setoid/ and Classical/ developments, using the structure identity principle in place of setoid equivalence.
  • src/Base/ holds the pre-reconstruction development and shared foundations still in use during the 3.0 transition. M2-1 will move the frozen portions to src/Legacy/Base/; new contributions do not land in Base/ (or later in Legacy/Base/).
  • src/Overture/ holds the small set of definitions shared across Setoid/, Classical/, and (eventually) Cubical/.
  • src/Examples/Demos/ holds self-contained pedagogical presentations of marquee results. src/Examples/Demos/HSP is a single-file rendition of Birkhoff's variety theorem suitable for teaching; the canonical proof lives in src/Setoid/Varieties/HSP, designated canonical under M2-4 (#259).

The contributor's guide gives more detail on which tree a new piece of work belongs in; when in doubt, please open an issue with the design-discussion label.

Installation

The recommended development environment is Nix (Option 1 in INSTALL.md):

nix develop

inside a clone of the repository. This pins Agda 2.8.0 and standard-library 2.3 automatically, writes a project-local Agda library configuration under .agda/, and bypasses any Agda or standard-library versions registered elsewhere on the host machine.

For contributors who cannot or prefer not to use Nix, INSTALL.md walks through three alternative paths: Agda's official Python installer (pipx install agda==2.8.0), a prebuilt binary from the Agda 2.8.0 release page, and a cabal build from source. All three require manually installing standard-library 2.3 and registering it in ~/.config/agda/libraries.

Requirements

Older versions of either component are not supported on the master branch. To work against the v2.0.1 archival release (which targets Agda 2.6.2 / stdlib 1.7), check out the v2.0.1 tag.

Contributing

Contributions are welcome — bug reports, design discussions, pull requests, and documentation improvements alike. Before contributing code, please read

  • CONTRIBUTING.md — development workflow, branching, and review expectations;
  • docs/STYLE_GUIDE.md — file format, naming, notation, proof style, and the library-as-training-corpus considerations that shape how we write proofs;
  • docs/GITHUB_PROJECT.md — the 3.0 milestone roadmap (check whether your contribution fits an existing track before opening a fresh issue);
  • CODE_OF_CONDUCT.md — community standards.

For questions about mathematical content or larger design changes, please open a GitHub issue with the design-discussion label before writing code.

Licensing

agda-algebras is licensed to match the several natures of the project.

  • Source code (under src/) is licensed under the Apache License 2.0, a permissive industry-standard software license compatible with essentially all other open-source licenses and with commercial use.
  • Documentation, papers, and tutorials (under docs/) are licensed under the Creative Commons Attribution 4.0 International License, the standard license for academic-style written material; it permits sharing and adaptation with attribution.
  • Machine-extracted representations of the library — type signatures, proof terms as Agda renders them, names, dependency metadata, structural encodings, statistics, and corpora built from these — carry an additional permission: they may be used under Apache-2.0 or under CC0-1.0, at the recipient's option. This is a grant, not a restriction; it exists so that using this library as machine-learning training or retrieval data does not require per-row attribution bookkeeping. Citation is requested rather than required in that case — see Citing.

If you are redistributing or building on agda-algebras, please respect these licenses for their respective parts of the repository.

Citing

DOI

The archival reference is the v2.0.1 Zenodo deposit, made for the TYPES 2021 submission:

@misc{ualib_v2.0.1,
  author       = {De{M}eo, William and Carette, Jacques},
  title        = {{T}he {A}gda {U}niversal {A}lgebra {L}ibrary (agda-algebras)},
  year         = 2021,
  note         = {{D}ocumentation available at https://ualib.org},
  version      = {2.0.1},
  doi          = {10.5281/zenodo.5765793},
  howpublished = {{G}it{H}ub.com},
  note         = {{V}er.~2.0.1; source code: \href{https://zenodo.org/record/5765793/files/ualib/agda-algebras-v.2.0.1.zip?download=1}{agda-algebras-v.2.0.1.zip}, {G}it{H}ub repo: \href{https://github.com/ualib/agda-algebras}{github.com/ualib/agda-algebras}},
}

While the 3.0 reconstruction is in development, please cite the GitHub repository directly and pin a commit hash for reproducibility. A new Zenodo DOI will be minted at the v3.0 release.

To cite the formalization of Birkhoff's HSP theorem:

@article{DeMeo:2021,
  author        = {De{M}eo, William and Carette, Jacques},
  title         = {A {M}achine-checked {P}roof of {B}irkhoff's {V}ariety {T}heorem
                   in {M}artin-{L}\"of {T}ype {T}heory},
  journal       = {CoRR},
  volume        = {abs/2101.10166},
  year          = {2021},
  eprint        = {2101.10166},
  archivePrefix = {arXiv},
  primaryClass  = {cs.LO},
  url           = {https://arxiv.org/abs/2101.10166},
  note          = {Source code: \href{https://github.com/ualib/agda-algebras/blob/master/src/Examples/Demos/HSP.lagda.md}{https://github.com/ualib/agda-algebras/blob/master/src/Examples/Demos/HSP.lagda.md}}
}

The current canonical setoid-based formalization of Birkhoff's theorem is in the Setoid.Varieties.HSP module, with the proof anchor in the rendered site at https://agda-algebras.universalalgebra.org/Setoid/Varieties/HSP/#proof-of-the-hsp-theorem.

Credits

The agda-algebras library is developed and maintained by the agda-algebras development team:

Acknowledgements

We thank Andreas Abel, Jeremy Avigad, Andrej Bauer, Clifford Bergman, Venanzio Capretta, Martín Escardó, Ralph Freese, Hyeyoung Shin, and Siva Somayyajula for helpful discussions, corrections, advice, inspiration, and encouragement. Most of the mathematical results formalized in agda-algebras are well known; the novelty is in the formalization itself, which is mainly due to the contributors and acknowledgees listed above.

References

The following Agda documentation and tutorials informed the development of agda-algebras:

The official Agda Wiki, Agda User's Manual, Agda Language Reference, and the open-source Agda Standard Library source code are also indispensable.

About

The Agda Universal Algebra Library (html docs available at the url below)

agda-algebras.universalalgebra.org

Topics

agdaagda-librarydependent-typesfoundationslogicmodel-theorytype-theoryuniversal-algebra

Resources

Readme

Code of conduct

Code of conduct

Contributing

Contributing
Activity
Custom properties

Stars

49 stars

Watchers

3 watching

Forks

8 forks
Report repository

Releases

Sponsor this project

Packages

Used by

Contributors

Languages