diff --git a/README.md b/README.md
index 15cfcee..7748eaa 100644
--- a/README.md
+++ b/README.md
@@ -32,7 +32,6 @@ ghci> run "Eaxmple.shitt"
 - [x] Coverage checking
 - [x] Without K
 - [x] [Syntax Highlight](https://github.com/KonjacSource/shitt-highlight)
-- [x] Higher Inductive Types(No boundary check yet)
 - [x] REPL
 - [x] Module system (very naive)
 
@@ -176,7 +175,9 @@ fun invf {A B : U} (f : A -> B) (y : B) (_ : Imf f y) : A where
 
 Here `y` is restricted by `imf x`.
 
-### HIT
+### (TODO) HIT
+
+For now, we can only do this.
 
 ```haskell
 higher inductive Int : U where