diff --git a/README.md b/README.md
index d4989da..2d9737f 100644
--- a/README.md
+++ b/README.md
@@ -24,3 +24,18 @@ So far the contributions are:
 
 ## TODO
 TODOs are found inside the literate agda files!
+
+## Usage
+The project requires a new version of agda-categories (newer than some package managers ship), so the easiest way to use this project is via the provided nix flake, which fetches my fork of agda-categories that is guaranteed to work with this project.
+
+To use the project you just have to open a development shell:
+```sh
+nix develop .
+```
+(this will take 20 - 30 minutes the first time, because it has to typecheck the agda-categories library)
+
+There is also a Makefile for compiling every module and generating the html documentation.
+
+```
+make
+```