Skip to content
/ cat Public
forked from fredefox/cat

Formalizing Category Theory in Agda using Cubical Type Theory

Notifications You must be signed in to change notification settings

Saizan/cat

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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-472fc6b

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

Or you could symlink them as well if you want.

About

Formalizing Category Theory in Agda using Cubical Type Theory

Resources

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Agda 99.9%
  • Makefile 0.1%