NEWS! (2021 Mar 7) The long paper on arXiv describing the library is already outdated. However, the complete and always-up-to-date html documentation of the Agda UALib is available on the main ualib.org website.
Pdf documentation will appear in a series of three papers, the first of which is now available as ualib-part1.pdf. Parts 2 and 3 are in the works. Stay tuned.
(2021 Jan 20) I am very pleased to announce that on 12 January 2021 I achieved my goal of constructing a formal, machine-checked proof of Birkhoff's variety theorem in dependent type theory using the Agda programming language.