2017-11-10 16:08:38 +00:00
|
|
|
Description
|
|
|
|
|
===========
|
2018-02-21 12:52:51 +00:00
|
|
|
This project aims to formalize some parts of category theory using cubical agda
|
|
|
|
|
— an extension to agda permitting univalence. To learn more about this
|
|
|
|
|
[readthedocs](https://agda.readthedocs.io/en/latest/language/cubical.html).
|
|
|
|
|
|
|
|
|
|
This project draws a lot of inspiration from [the
|
|
|
|
|
HoTT-book](https://homotopytypetheory.org/book/).
|
2017-11-10 16:08:38 +00:00
|
|
|
|
|
|
|
|
Installation
|
|
|
|
|
============
|
|
|
|
|
|
|
|
|
|
Dependencies
|
|
|
|
|
------------
|
2018-02-20 13:08:47 +00:00
|
|
|
To succesfully compile the following is needed:
|
|
|
|
|
|
2018-03-07 14:40:52 +00:00
|
|
|
* The Agda release candidate 2.5.4[^1]
|
2018-05-08 16:45:36 +00:00
|
|
|
* [Agda Standard Library](https://github.com/agda/agda-stdlib)
|
2018-02-21 12:52:51 +00:00
|
|
|
* [Cubical](https://github.com/Saizan/cubical-demo/)
|
|
|
|
|
|
2018-03-07 14:40:52 +00:00
|
|
|
[^1]: At least version >= [`707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43`](https://github.com/agda/agda/commit/707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43)
|
|
|
|
|
|
2018-05-08 16:45:36 +00:00
|
|
|
The version of the libraries that this depends on can be shown by
|
|
|
|
|
executing the following command in the root directory of the project:
|
|
|
|
|
|
|
|
|
|
git submodule foreach git rev-parse HEAD
|
|
|
|
|
|
|
|
|
|
Unfortunately Agda's module system does not allow us to automatically
|
|
|
|
|
add these dependencies. So you'll have to make sure you're using
|
|
|
|
|
versions of these libraries that are compatible with this
|
|
|
|
|
project. Since this information is only provided as documentation it
|
|
|
|
|
may also noot be up-to-date so beware.
|
|
|
|
|
|
2018-02-21 12:52:51 +00:00
|
|
|
It's important to have the right version of these - but which one is the right
|
|
|
|
|
is in constant flux. It's most likely the newest one.
|
2018-02-20 13:08:47 +00:00
|
|
|
|
2017-11-10 16:08:38 +00:00
|
|
|
I've used git submodules to manage dependencies. Unfortunately Agda does not
|
2018-02-21 12:52:51 +00:00
|
|
|
allow specifying libraries to be used only as local dependencies. So the
|
|
|
|
|
submodules are mostly used for documentation.
|
2017-11-10 16:08:38 +00:00
|
|
|
|
|
|
|
|
You can let Agda know about these libraries by appending them to your global
|
|
|
|
|
libraries file like so: (NB!: There is a good reason this is not in a
|
|
|
|
|
makefile. So please verify that you know what you are doing, you probably
|
|
|
|
|
already have standard-library in you libraries)
|
|
|
|
|
|
|
|
|
|
AGDA_LIB=~/.agda
|
|
|
|
|
readlink -f libs/*/*.agda-lib | tee -a $AGDA_LIB/libraries
|
|
|
|
|
|
|
|
|
|
Anyways, assuming you have this set up you should be good to go.
|
