This is the source code for my Univalent-Agda project. It is mostly following the HoTT Book, but I will hopefully add in more results about classical mathematics and algebra. It is on GitHub and is written in literate Agda, using Emacs' org-mode.
This is still a work in progress. To browse the code here, currently, the best thing to do is start here. It should link to every (non-experimental) file in the repository.