Univalent-Agda

Univalent-Agda

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.

Author: James Leslie

Created: 2021-03-24 Wed 10:01