Remove obsolete comment
This commit is contained in:
parent
a5571de191
commit
655c12720a
|
@ -2,7 +2,7 @@ Description
|
||||||
===========
|
===========
|
||||||
This project aims to formalize some parts of category theory using cubical agda
|
This project aims to formalize some parts of category theory using cubical agda
|
||||||
— an extension to agda permitting univalence. To learn more about this
|
— an extension to agda permitting univalence. To learn more about this
|
||||||
[readthedocs](https://agda.readthedocs.io/en/latest/language/cubical.html).
|
[read the docs](https://agda.readthedocs.io/en/latest/language/cubical.html).
|
||||||
|
|
||||||
This project draws a lot of inspiration from [the
|
This project draws a lot of inspiration from [the
|
||||||
HoTT-book](https://homotopytypetheory.org/book/).
|
HoTT-book](https://homotopytypetheory.org/book/).
|
||||||
|
@ -31,13 +31,6 @@ versions of these libraries that are compatible with this
|
||||||
project. Since this information is only provided as documentation it
|
project. Since this information is only provided as documentation it
|
||||||
may also noot be up-to-date so beware.
|
may also noot be up-to-date so beware.
|
||||||
|
|
||||||
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. So the
|
|
||||||
submodules are mostly used for documentation.
|
|
||||||
|
|
||||||
You can let Agda know about these libraries by appending them to your global
|
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
|
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
|
makefile. So please verify that you know what you are doing, you probably
|
||||||
|
|
Loading…
Reference in a new issue