cat
cat copied to clipboard
fredefox
A formalization of category theory in cubical Agda
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.2[^1]
- Agda Standard Library version v1.3-9f454e23
- Agda Cubical Library version v0.1-acabbd9
[^1]: Revisions 02cb18a and 61ea3a3.
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.
fredefox