Go to file
2018-05-31 02:12:45 +02:00
doc Fixup some missing files 2018-05-31 01:07:05 +02:00
libs Makefile uses included libraries 2018-05-26 01:15:57 +02:00
src Test with master Agda version 2.6.0-d3efe64 2018-05-31 01:56:44 +02:00
.gitignore Various changes proposed by Andreas 2018-05-15 16:08:29 +02:00
.gitmodules Add new submodules 2017-11-10 16:56:52 +01:00
BACKLOG.md Update CHANGELOG and remove --allow-unsolved-metas pragma 2018-05-08 18:35:22 +02:00
cat.agda-lib Add comment to agda-lib 2018-01-31 14:47:20 +01:00
CHANGELOG.md Update change log 2018-05-29 15:24:18 +02:00
libraries Add libraries file 2017-11-26 14:57:07 +01:00
Makefile Update makefile 2018-05-29 15:35:20 +02:00
README.md Update RAEDME 2018-05-31 02:12:45 +02:00

Description

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

Dependencies

To successfully compile the following is needed:

Has been tested with:

  • Agda version 2.6.0-d3efe64

Building

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.agda-lib
EOF

Or you could symlink them as well if you want.