This repository hosts my Agda code for homotopy type theory. Homotopy type theory is a new type theory seeking the connections between (abstract) homotopy theory, type theory and category theory. For more information about this theory I recommend this blog.
Lots of code is copied from Nil's repository (with my significant refactoring). We both released our code under BSD 3. Please consider using open-source licenses in your derived work to maximize the availability and usefulness, thanks.
For an overview of the code, please take a look at