chore(library/init): remove punit micro module

library/init/core.lean

@@ -1633,7 +1633,7 @@ end subtype
 section
 variables {α : Type u} {β : Type v}
 
-@[simp] lemma prod.mk.eta : ∀{p : α × β}, (p.1, p.2) = p
+@[simp] theorem prod.mk.eta : ∀{p : α × β}, (p.1, p.2) = p
 | (a, b) := rfl
 
 instance [inhabited α] [inhabited β] : inhabited (prod α β) :=
@@ -1660,10 +1660,27 @@ instance prod_has_decidable_lt
          [decidable_rel ((<) : β → β → Prop)] : Π s t : α × β, decidable (s < t) :=
 λ t s, or.decidable
 
-lemma prod.lt_def [has_lt α] [has_lt β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
+theorem prod.lt_def [has_lt α] [has_lt β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
 rfl
 end
 
 def {u₁ u₂ v₁ v₂} prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
   (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
 | (a, b) := (f a, g b)
+
+/- Universe polymorphic unit -/
+
+theorem punit_eq (a b : punit) : a = b :=
+punit.rec_on a (punit.rec_on b rfl)
+
+theorem punit_eq_punit (a : punit) : a = () :=
+punit_eq a ()
+
+instance : subsingleton punit :=
+subsingleton.intro punit_eq
+
+instance : inhabited punit :=
+⟨()⟩
+
+instance : decidable_eq punit :=
+λ a b, is_true (punit_eq a b)

library/init/data/basic.lean

@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.setoid init.data.quot init.data.punit
-import init.data.nat.basic init.data.sum.basic
+import init.data.setoid init.data.quot init.data.nat.basic init.data.sum.basic
 import init.data.sigma.basic init.data.fin.basic init.data.list.basic init.data.char.basic
 import init.data.string.basic init.data.option.basic init.data.set
 import init.data.uint init.data.ordering.basic init.data.repr

library/init/data/punit.lean

@@ -1,22 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-prelude
-import init.core
-
-lemma punit_eq (a b : punit) : a = b :=
-punit.rec_on a (punit.rec_on b rfl)
-
-lemma punit_eq_punit (a : punit) : a = () :=
-punit_eq a ()
-
-instance : subsingleton punit :=
-subsingleton.intro punit_eq
-
-instance : inhabited punit :=
-⟨()⟩
-
-instance : decidable_eq punit :=
-λ a b, is_true (punit_eq a b)