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:

• Agda
• Agda Standard Library
• Agda Cubical Library

Has been tested with:

• Agda versions 2.6.1 and 2.6.2¹
• Agda Standard Library version v1.3-9f454e23
• Agda Cubical Library version v0.1-acabbd9

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.