Description
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.
Dependencies
To successfully compile the following is needed:
Has been tested with:
- Agda versions 2.6.1 and 2.6.21
- Agda Standard Library version v1.3-9f454e23
- Agda Cubical Library version v0.1-acabbd9
Building
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.
Footnotes
-
Revisions
02cb18aand61ea3a3.↩