Skip to content

ualib/agda-algebras

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 entire library
make html            # (optional) build clickable HTML under ./html/

The first nix develop downloads and builds the pinned Agda and standard library; 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.

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/ (planned, M3) 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.
  • 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/Demos/ holds self-contained pedagogical presentations of marquee results. src/Demos/HSP is a single-file rendition of Birkhoff's variety theorem suitable for teaching; the canonical proof lives in src/Setoid/Varieties/HSP.agda (canonicality to be formalized in M2-4).

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 dual-licensed to match the dual nature 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.

If you are redistributing or building on agda-algebras, please respect both 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/Demos/HSP.agda}{https://github.com/ualib/agda-algebras/blob/master/src/Demos/HSP.agda}}
}

The current canonical setoid-based formalization of Birkhoff's theorem is in the Setoid.Varieties.HSP module, with the proof anchor in the rendered HTML at https://ualib.org/Setoid.Varieties.HSP.html#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)

ualib.github.io/agda-algebras/

Topics

dependent-types logic type-theory agda foundations model-theory agda-library universal-algebra

Resources

Readme

License

Apache-2.0, Unknown licenses found

Licenses found

Apache-2.0
LICENSE
Unknown
LICENSE-docs

Code of conduct

Code of conduct

Contributing

Contributing
Activity
Custom properties

Stars

45 stars

Watchers

4 watching

Forks

8 forks
Report repository

Releases 3

v.2.0.1 Latest
Dec 8, 2021
+ 2 releases

Sponsor this project

Packages

 
 
 

Contributors

Languages