diff --git a/README.md b/README.md index 2869967..fd29dad 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ 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 -[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 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 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 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