diff --git a/README.md b/README.md
index 2b43008..fae0104 100644
--- a/README.md
+++ b/README.md
@@ -20,19 +20,26 @@ A dependently typed system
 
 * Σ Types
 
-# TODO
+* Martin-Löf Identity types
 
-* Performence optimisation
-  * Parsing !!! (this is like 90% of the time currently lmao)
-  * Memoize normalisation and conversion somehow?
+# TODO
 
 * Universes
 
-* Implicit arguments
+* Elaboration
+  * Implicit arguments
+  * Universe family application
 
-* (indexed) inductive datatypes
+* Inductives
+  * Indexed inductives
 
-* Write down the rules (I'll not get this far)
+## Things that could be fun to do sometime eventually
+
+* Pattern matching in elaborator
+
+* Write down the rules
+
+* Performence optimisation?
 
 * Compile to scheme