From 2b441fe0ec0409450184e88129f19b72d3ccabea Mon Sep 17 00:00:00 2001
From: depsterr <depsterr@protonmail.com>
Date: Wed, 20 Jul 2022 21:22:35 +0200
Subject: [PATCH] updated plan

---
 README.md | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/README.md b/README.md
index 3ae90e2..261d7b4 100644
--- a/README.md
+++ b/README.md
@@ -3,15 +3,16 @@ A dependently typed system
 
 # TODO
 
-* Inductively defined datatypes
+* Some fun types
+  * ⊤
+  * ⊥
+  * ℕ
+  * Σ
+  * Id
 
-* Implicit arguments, Metavariables, and Unification
+* Implicit arguments
 
-* Universe hierarchy
-
-  * Universe Polymorphism
-
-  * Cumulative Universes(?)
+* Universes
 
 # References