Credits

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

The agda-algebras development team

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.

Escardo, Introduction to Univalent Foundations of Mathematics with Agda
Wadler, Programming Languages Foundations in Agda
Bove and Dybjer, Dependent Types at Work
Gunther, Gadea, Pagano, Formalization of Universal Algebra in Agda
Norell and Chapman, Dependently Typed Programming in Agda

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

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

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.