diff --git a/colimit/README.md b/colimit/README.md
index 02e1d55..0dce244 100644
--- a/colimit/README.md
+++ b/colimit/README.md
@@ -1 +1,5 @@
-This folder contains various properties about colimits, from a paper to appear by Egbert Rijke, Floris van Doorn and Kristina Sojakova.
\ No newline at end of file
+This folder contains a formalization of various properties about sequential colimits. Most importantly, we prove that sigma-types commute with colimits. It accompanies a submitted paper by Kristina Sojakova, Floris van Doorn and Egbert Rijke.
+
+This repository contains some unproven results, marked by `sorry`. No unproven results are used for any theorems discussed in the paper. You can write `print axioms theoremname` in a file to verify that `sorry` is not used in the proofs.
+
+You will need a working version of Lean 2 to compile this repository. Installation instructions for Lean 2 can be found [here](https://github.com/leanprover/lean2). After that, you can run `linja` (or `path/to/lean2/bin/linja`) from the command-line in the main directory to compile this repository.