diff --git a/library/data/unit/basic.lean b/library/data/unit/basic.lean
new file mode 100644
index 000000000..df303f48e
--- /dev/null
+++ b/library/data/unit/basic.lean
@@ -0,0 +1,5 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+inductive unit.{l} : Type.{l} :=
+  star : unit
diff --git a/library/data/unit/decl.lean b/library/data/unit/decl.lean
new file mode 100644
index 000000000..2860fbec1
--- /dev/null
+++ b/library/data/unit/decl.lean
@@ -0,0 +1,9 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+inductive unit.{l} : Type.{l} :=
+  star : unit
+
+namespace unit
+  notation `⋆` := star
+end unit
diff --git a/library/data/unit/default.lean b/library/data/unit/default.lean
new file mode 100644
index 000000000..7b2dbca50
--- /dev/null
+++ b/library/data/unit/default.lean
@@ -0,0 +1,4 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+import data.unit.decl data.unit.thms data.unit.insts
diff --git a/library/data/unit.lean b/library/data/unit/insts.lean
similarity index 65%
rename from library/data/unit.lean
rename to library/data/unit/insts.lean
index 0694735df..6f7cf442e 100644
--- a/library/data/unit.lean
+++ b/library/data/unit/insts.lean
@@ -1,24 +1,13 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic.decidable logic.inhabited
+import data.unit.decl data.unit.thms logic.decidable logic.inhabited
 open decidable
 
-inductive unit.{l} : Type.{l} :=
-  star : unit
 namespace unit
-  notation `⋆` := star
-
-  -- remove duplication?
-  protected theorem equal (a b : unit) : a = b :=
-  rec_on a (rec_on b rfl)
-
   protected theorem subsingleton [instance] : subsingleton unit :=
   subsingleton.intro (λ a b, equal a b)
 
-  theorem eq_star (a : unit) : a = star :=
-  equal a star
-
   protected definition is_inhabited [instance] : inhabited unit :=
   inhabited.mk ⋆