diff --git a/README.md b/README.md
new file mode 100644
index 0000000..3218f84
--- /dev/null
+++ b/README.md
@@ -0,0 +1,4 @@
+# justified-type-inference
+An implementation of Compositional type inference in Idris with a complete proof
+
+I am now working on a [Coq version of this](https://github.com/joonazan/verified-type-inference) because of a code generation bug in Idris and because typechecking was so slow.