A formalization of category theory in cubical Agda
This project aims to formalize some parts of category theory using Cubical Agda — an extension to agda permitting univalence. To learn more about Cubical Agda read the docs.
This project draws a lot of inspiration from the HoTT-book.
If you want more information about this project, then you're in luck. This is my masters thesis. It can be accessed here or build like so:
cd doc/
make
You can browse a syntax-highlighted version of the formalization here.
To successfully compile the following is needed:
Has been tested with:
[^1]: Revisions 02cb18a
and 61ea3a3
.
You can build the library with
git submodule update --init
make
The library file .agda-lib
takes care of using the right
dependencies, which are cloned as "submodules" into the libs
directory by the first command line.