diff --git a/README.md b/README.md
new file mode 100644
index 0000000..4fce48b
--- /dev/null
+++ b/README.md
@@ -0,0 +1,6 @@
+Cumulative hierarchy in Coq
+---------------------------
+
+Aczel's model of CZF done in Coq.
+
+Uses [std++](https://gitlab.mpi-sws.org/iris/stdpp).