Skip to content

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

License

Notifications You must be signed in to change notification settings

TypeFunc/agda-algebras

 
 

Repository files navigation

agda-algebras

This is a copy of the Agda Universal Algebra Library which depends the Standard Library of the Agda proof assistant language. It is currently under active reconstruction, and should be regarded as alpha software. (The previous version of the Agda Universal Algebra Library, which was called UALib, was based on the Type Topology library of Martín Escardó.

If problems arise when attempting to follow these steps, please email the development team or create new issue on the git repo for this library.


Introduction

This repository contains the source code, as well as the files used to generate the documentation, for (this version of) the Agda Universal Algebra Library. (Documentation for the previous version is available at ualib.org.)


Documentation

Agda was used to generate html pages for each module. These pages are now served at

https://ualib.github.io/agda-algebras/

(The previous version of the agda-algebras library, called UALib, is documented at ualib.org.)


Install Agda

Agda (version 2.6.1 or greater) is required.

If you don't have it, follow the official Agda installation instructions.

For reference, the following is a list of commands that should Agda version 2.6.2 on a Ubuntu 18.04 distro. Please submit an issue or pull request if these commands don't work for you.

cabal update
git clone git@github.com:agda/agda.git
cd agda
git checkout release-2.6.2
cabal install Agda-2.6.2 --program-suffix=-2.6.2  # (takes a very long time)
cd ~/.cabal/bin/
touch ~/.emacs
cp ~/.emacs ~/.emacs.backup
./agda-mode-2.6.2 setup
./agda-mode-2.6.2 compile
mkdir -p ~/bin
cp ~/.emacs ~/bin
cp ~/.emacs.backup ~/.emacs
cd ~/bin
echo '#!/bin/bash' > agdamacs
echo 'PATH=~/.cabal/bin:$PATH emacs --no-init-file --load ~/bin/.emacs \$@' >> agdamacs
chmod +x agdamacs
echo 'export PATH=~/bin:~/.cabal/bin:$PATH' >> ~/.profile

Now invoking the command agdamacs will launch emacs with Agda 2.6.2 and agda-mode installed.)


Contributing to this repository

If you wish to contribute to this repository, the best way is to use the standard fork-clone-pull-request workflow. This is described nicely on this page. More extensive instructions, that still apply, can be found on the original project's page.


Credits

The agda-algebras library is developed and maintained by the ualib/agda-algebras development team.

The agda-algebras development team

Jacques Carette
William DeMeo

Acknowledgements and attributions

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 the agda-algebras are well known. Regarding the source code in the agda-algebras library, this is mainly due to the contributors listed above.

References

The following Agda documentation and tutorials helped inform and improve the agda-algebras library, especially the first one in the list.

Finally, the official Agda Wiki, Agda User's Manual, Agda Language Reference, and the (open source) Agda Standard Library source code are also quite useful.

How to cite the Agda Universal Algebra Library

DOI

To cite the agda-algebras software library in a publication or on a web page, please use the following BibTeX entry:

@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}},
}                  

To cite the agda-algebras documentation, please use the following BibTeX entry:

@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.2101.10166},
 archivePrefix = {arXiv},
 primaryClass  = {cs.LO},
 note          = {Source code: \href{https://github.com/ualib/agda-algebras/blob/master/src/Demos/HSP.lagda}{https://github.com/ualib/agda-algebras/blob/master/src/Demos/HSP.lagda}}
}

License

Creative Commons License
The Agda Universal Algebra Library by William DeMeo and the Agda Algebras Development Team is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.
Based on a work at https://gitlab.com/ualib/ualib.gitlab.io.

About

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

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Agda 81.6%
  • Emacs Lisp 11.4%
  • TeX 6.5%
  • Other 0.5%