This project aims to formalize some parts of category theory using cubical agda — an extension to agda permitting univalence. To learn more about this 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. Go ahead and read it here or alternative like so:
cd doc/
make
To successfully compile the following is needed:
- The master branch of Agda.
- Agda Standard Library
- Cubical Demo
Has been tested with:
- Agda version 2.6.0-472fc6b
You can build the library with
git submodule update --init
make
The Makefile takes care of using the right dependencies.
Unfortunately I have not found a way to automatically inform
agda-mode that it should use these dependencies. So what you can do
in stead is to copy these libraries to a global location and then add
them system wide:
mkdir -p ~/.agda/libs
cd ~/.agda/libs
git clone $CAT/libs/std-lib
git clone $CAT/libs/cubical
echo << EOF | tee -a ~/.agda/libraries
$HOME/.agda/libs/agda-stdlib/standard-library.agda-lib
$HOME/.agda/libs/cubical/cubical-demo.agda-lib
EOF
Or you could symlink them as well if you want.