fredefox
/
cat
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Update readme

This commit is contained in:
Frederik Hanghøj Iversen 2018-02-21 13:52:51 +01:00
parent 8f620e0dbe
commit 7398210a2b
1 changed files with 13 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
README.md
View File

@ -1,7 +1,11 @@
Description
===========
This project includes code as well as my masters thesis (currently just
consisting of the proposal for the thesis).
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/).
Installation
============
@ -11,10 +15,15 @@ Dependencies
To succesfully compile the following is needed:
* Agda version >= `707ce6042b6a3bdb26521f3fe8dfe5d8a8470a43`.
* Agda Standard Library >= `87d28d7d753f73abd20665d7bbb88f9d72ed88aa`.
* [Agda Standard Library](https://github.com/agda/agda-stdlib)
* [Cubical](https://github.com/Saizan/cubical-demo/)
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.
I've used git submodules to manage dependencies. Unfortunately Agda does not
allow specifying libraries to be used only as local dependencies.
allow specifying libraries to be used only as local dependencies. So the
submodules are mostly used for documentation.
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