Author. William DeMeo
Affiliation. Department of Algebra, Charles University in Prague
PDF documentation. ualib-part1.pdf, ualib-part2.pdf
(ualib-part3.pdf coming soon!)
Abstract. The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) that formalizes the foundations of universal algebra in dependent type theory using the Agda proof assistant language.
This is the main repository for the Agda UALib. Below are instructions for getting the UALib installed on your machine. I hope that these steps work for you; they work on my Ubuntu 18.04 machine, but I haven't tested them on a fresh distro, or any other OS, so...
...in any case, please email me if you have trouble.
This repository contains the source code, as well as files that generate documentation, for the Agda Universal Algebra Library, aka Agda UALib.
The docs are served at ualib.org, and are automatically generated from the .lagda files using the script generate-md. See the section on Generating the documentation below.
Agda (version 2.6.1 or greater) is required.
If you don't have it, follow the official Agda installation instructions or these instructions by Martin Escardo.
Be sure you have Agda, Emacs (or Spacemacs), and agda2-mode for Emacs (Spacemacs) installed.
Clone the repository to your local machine using ONE of the following alternative commands:
git clone https://gitlab.com/ualib/ualib.gitlab.io.gitOR, if you have a gitlab account and have configured ssh keys,
git clone [email protected]:ualib/ualib.gitlab.io.gitThis creates a directory on your local machine called ualib.gitlab.io. The UALib source code files reside in subdirectories of ualib.gitlab.io/UALib and have the .lagda extension.
Having installed Agda and cloned the ualib.gitlab.io repository, you should now be able to work with the source code contained in the .lagda files, such as UALib.lagda or any of it submodules. For example, you might start by loading the file UALib/Prelude/Preliminaries.lagda into Emacs and check that Agda can type-check that file using the command C-c C-l.
Other Emacs keybindings are described in the emacs-mode.html#keybindings section of the Agda docs.
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, but below we list the five simple steps required.
(A "pull request" is also known as a "merge request" on gitlab and its documentation.)
The following assumes you already have a gitlab or github account. If you don't, sign up for one. It's free. The instructions below are for gitlab, but they should work for github as well.
-
Fork the ualib.gitlab.io repository. This makes a complete copy of the repository in your own gitlab account that you now control, so, for example, you can commit and push changes to the source code in your forked copy of the repo.
-
Clone your fork to make a copy of it on your local machine.
-
Make some improvements to the source files or documentation in your local copy of the repository.
-
Commit your changes to your local repository and then Push your changes to your remote fork residing in your gitlab account.
-
Submit a merge request to alert the UALib team members that you would like your proposed changes to be reviewed and integrated into the official Agda UALib repository.
When improvements are made to the "upstream" ualib/ualib.gitlab.io repository, you will want to update your fork to incorporate these changes.
Below is a list of the commands that accomplish this, but see this page and this page for more details.
New Gitlab has a "mirroring" feature to keep your fork synced with the upstream repo. See this page for details.
-
Change to the working directory of your local copy of the repository and specify the upstream repository.
cd $HOME/git/ualib.gitlab.io # (for example) git remote add upstream [email protected]:ualib/ualib.gitlab.io.git
-
Verify that it worked.
git remote -v
The output should look something like this:
origin [email protected]:your-user-name/ualib.gitlab.io.git (fetch) origin [email protected]:your-user-name/ualib.gitlab.io.git (push) upstream [email protected]:ualib/ualib.gitlab.io.git (fetch) upstream [email protected]:ualib/ualib.gitlab.io.git (push)
If the foregoing fails, try
git remote add upstream https://gitlab.com/ualib/ualib.gitlab.io.git
-
In the working directory of your local project, fetch the branches and their commits from the upstream repository and merge upstream/master into your local master branch.
git fetch upstream git checkout master git merge upstream/master
This brings your fork's master branch into sync with the upstream repository, without losing your local changes.
-
Finally, commit the changes and push to your remote fork.
git commit -m "merged changes from upstream" git push origin master
Now when you now visit the Gitlab page of your personal fork of the repo, you should see a message like, "This branch is even with ualib:master."
The html pages at ualib.org were generated from the literate Agda (.lagda) files in this repository. These files contain formal, verified, mathematical theorems and proofs inside code environments (i.e., inside \begin{code}...\end{code} blocks) as well as some mathematical discussions outside those blocks written in markdown.
The html documentation is available at ualib.org, so there is usually no need for end-users to generate the documentation pages locally. However, if you want to fix something or help develop improved versions of the docs or code, you may want to update and render the documentation html pages on your local machine. In that case, the instructions in this section may be helpful.
To generate the html documentation pages and serve them locally you will need bundler and jekyll. If you're using Ubuntu 18.04 or something similar, the INSTALL_JEKYLL.md file gives instructions for installing these two programs.
The html pages are generated by Agda with the following command:
agda --html --html-highlight=code UALib.lagda
This generates a set of markdown files that are then converted to html by jekyll with the command
bundle exec jekyll buildIn practice, we use the script generate-md, inside the UALib directory, to process the .lagda files and put the resulting markdown output in the right place, and then using the script jekyll-serve to invoke the following commands
cp html/UALib.md index.md
cp html/*.html html/*.md .
bundle install --path vendor
bundle exec jekyll serve --watch --incremental
This causes jekyll to serve the web pages locally so we can inspect them by pointing a browser to the local server at http://127.0.0.1:4000.
Please email William if you have any questions or problems using the UALib.
Comments, questions, or suggestions may also be submitted by creating a new issue.
A great source of information and inspiration for the Agda UALib is Marin Escardo's lecture notes on HoTT/UF in Agda.
See also Martin's HoTT/UF github repository and Type Topology github repository.
The author wishes to thank Siva Somayyajula, who contributed to this project during its first year and helped get it off the ground.
Thanks also to Andreas Abel, Andrej Bauer, Clifford Bergman, Venanzio Capretta, Martin Escardo, Ralph Freese, Bill Lampe, Miklós Maróti, JB Nation, and Hyeyoung Shin for helpful discussions, corrections, advice, inspiration and encouragement.
Most of the mathematical results that formalized in the UAlib are already well known.
Regarding the Agda source code in the Agda UALib, this is mainly due to the author with one major caveat: we benefited greatly from, and the library depends upon, the lecture notes on Univalent Foundations and Homotopy Type Theory and the Type Topology Agda Library by Martin Hötzel Escardo. The author is indebted to Martin for making his library and notes available and for teaching a course on type theory in Agda at the Midlands Graduate School in the Foundations of Computing Science in Birmingham in 2019.
The Agda Universal Algebra Library by William DeMeo is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.
Based on a work at https://gitlab.com/ualib/ualib.gitlab.io.
If you use the Agda UALib or wish to refer to it or its documentation in a publication or on a web page, please use the following BibTeX data:
@article{DeMeo:2021,
author = {William DeMeo},
title = {The {A}gda {U}niversal {A}lgebra {L}ibrary and
{B}irkhoff's {T}heorem in {D}ependent {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: \url{https://gitlab.com/ualib/ualib.gitlab.io}},
biburl = {https://dblp.org/rec/journals/corr/abs-2101-10166.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}