diff --git a/README.md b/README.md
new file mode 100644
index 0000000..17d6cc8
--- /dev/null
+++ b/README.md
@@ -0,0 +1,20 @@
+# agdaproofs
+Mathematical proofs in Agda
+
+## What is it?
+This is an ongoing project for me to formalise my lecture notes from the Cambridge Mathematical Tripos.
+I started in about June 2018 and have been going at least through January 2019.
+I'm starting at the very beginning (a very good place to start), and proving as much as I can from the lecture notes and the example sheets.
+
+## Status
+
+I make no promises about the quality of this code.
+It's proofs, not prose.
+
+Similarly, I'm using this to try and discover the right ways to do programming in a dependently-typed language, finding idioms and features as I go.
+Some of this was done really early, and the code is accordingly bad.
+
+Some of the code might not compile; I'll try and make sure that it does compile as I commit to it, but I just wanted to get it up here first.
+
+## Previous history
+The code used to be versioned with [Pijul](https://nest.pijul.com/Smaug/agda).