diff --git a/README.org b/README.org
new file mode 100644
index 0000000..552124b
--- /dev/null
+++ b/README.org
@@ -0,0 +1,5 @@
+* Type Theory and Formal Proofs
+This is a partial formalization of the first few chapters of /Type Theory and Formal Proof: An Introduction/ by Nederpelt and Geuvers in Coq. As it stands, the formalization covers up to approximately chapter 3.
+
+I differ in a few places from their formalization. In particular, I use de Bruijn indices, simply because they are so much more convenient than worrying about \alpha-conversion everywhere. I also include proofs of several exercises from the book.
+