diff --git a/TODO.md b/TODO.md
index 03a188e..e1129b2 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,3 +1,8 @@
 # Inductives
 
  * Add support for them in type checking, conversion, etc
+ * Positivity check, etc
+
+# Generally
+
+ * Create a syntax and parser
diff --git a/pi.ipkg b/pi.ipkg
index 17b9e02..8e7f458 100644
--- a/pi.ipkg
+++ b/pi.ipkg
@@ -9,6 +9,8 @@ modules = Term
         , Tests
         , Parsing.Parse
         , Parsing.Lex
+        , Inductive
+        , Inductive.Check
 
 options = "-p contrib --warnpartial"
 
diff --git a/src/Inductive.idr b/src/Inductive.idr
index 69d2fc0..6f5eea9 100644
--- a/src/Inductive.idr
+++ b/src/Inductive.idr
@@ -3,15 +3,13 @@ module Inductive
 import Data.Vect
 
 import Term
+import Misc
 
 {-
   The type of a constructor, indexed like terms
 -}
-public export
-data Constructor : (ctx : Index) -> (tags : Vect n Nat) -> Type where
-  Tr   : Term n v      -> Constructor n v                          -- a term
-  Sum  : Constructor n v -> Constructor (S n) v -> Constructor n v -- Σ _ : #0 , #1
-
+Constructor : (ctx : Index) -> (tags : Vect n Nat) -> Type
+Constructor = Term ctx tags
 
 {-
   The type of an inductive definition. It is a vector of constructors.
@@ -20,4 +18,3 @@ data Constructor : (ctx : Index) -> (tags : Vect n Nat) -> Type where
 public export
 Inductive : Nat -> Index -> Vect n Nat -> Type
 Inductive cons ctx tags = Vect cons (Constructor ctx (cons :: tags))
-
diff --git a/src/Inductive/Check.idr b/src/Inductive/Check.idr
new file mode 100644
index 0000000..834a921
--- /dev/null
+++ b/src/Inductive/Check.idr
@@ -0,0 +1,7 @@
+module Inductive.Check
+
+import Inductive
+import Term
+import Value
+import Convert
+import Check