diff --git a/library/init/collection.lean b/library/init/collection.lean
new file mode 100644
index 0000000000..f30359a59f
--- /dev/null
+++ b/library/init/collection.lean
@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.logic
+universe variables u v
+
+/- Type class used to implement polymorphic notation for collections.
+   Example: {a, b, c}. -/
+structure [class] insertable (A : Type u) (C : Type u → Type v) :=
+(empty : C A) (insert : A → C A → C A)
+
+section
+variables {A : Type u} {C : Type u → Type v}
+variable [insertable A C]
+
+definition insert : A → C A → C A :=
+insertable.insert
+
+/- The empty collection -/
+definition empty_col : C A :=
+insertable.empty A C
+
+notation `∅` := empty_col
+
+definition singleton (a : A) : C A :=
+insert a ∅
+end
+
+/- Type class use to implement the notation [ a ∈ c | p a ] -/
+structure [class] decidable_separable (A : Type u) (C : Type u → Type v) :=
+(sep : ∀ (p : A → Prop) [decidable_pred p], C A → C A)
+
+section
+variables {A : Type u} {C : Type u → Type v}
+variable [decidable_separable A C]
+
+definition dec_sep (p : A → Prop) [decidable_pred p] : C A → C A :=
+decidable_separable.sep p
+end
+
+/- Type class use to implement the notation { a ∈ c | p a } -/
+structure [class] separable (A : Type u) (C : Type u → Type v) :=
+(sep : (A → Prop) → C A → C A)
+
+section
+variables {A : Type u} {C : Type u → Type v}
+variable [separable A C]
+
+definition sep : (A → Prop) → C A → C A :=
+separable.sep
+end
diff --git a/library/init/set.lean b/library/init/set.lean
new file mode 100644
index 0000000000..dd1114467b
--- /dev/null
+++ b/library/init/set.lean
@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.logic init.collection
+
+universe variables u v
+
+definition set (A : Type u) := A → Prop
+
+namespace set
+variables {A : Type u} {B : Type v}
+
+definition mem (a : A) (s : set A) :=
+s a
+
+infix ∈ := mem
+notation a ∉ s := ¬ mem a s
+
+definition subset (s₁ s₂ : set A) : Prop :=
+∀ ⦃a⦄, a ∈ s₁ → a ∈ s₂
+infix ⊆ := subset
+
+definition superset (s₁ s₂ : set A) : Prop :=
+s₂ ⊆ s₁
+infix ⊇ := superset
+
+definition set_of (p : A → Prop) : set A :=
+p
+
+private definition sep (p : A → Prop) (s : set A) : set A :=
+λ a, a ∈ s ∧ p a
+
+attribute [instance]
+definition set_is_separable : separable A set :=
+⟨sep⟩
+
+private definition empty : set A :=
+λ a, false
+
+private definition insert (a : A) (s : set A) : set A :=
+λ b, b = a ∨ b ∈ s
+
+attribute [instance]
+definition set_is_insertable : insertable A set :=
+⟨empty, insert⟩
+
+definition union (s₁ s₂ : set A) : set A :=
+λ a, a ∈ s₁ ∨ a ∈ s₂
+notation s₁ ∪ s₂ := union s₁ s₂
+
+definition inter (s₁ s₂ : set A) : set A :=
+λ a, a ∈ s₁ ∧ a ∈ s₂
+notation s₁ ∩ s₂ := inter s₁ s₂
+
+definition compl (s : set A) : set A :=
+λ a, a ∉ s
+
+attribute [instance]
+definition set_has_neg : has_neg (set A) :=
+⟨compl⟩
+
+definition diff (s t : set A) : set A :=
+λ a, a ∈ s ∧ a ∉ t
+infix `\`:70 := diff
+
+definition powerset (s : set A) : set (set A) :=
+λ t : set A, t ⊆ s
+prefix `𝒫`:100 := powerset
+
+definition image (f : A → B) (s : set A) : set B :=
+λ b, ∃ a, a ∈ s ∧ f a = b
+infix ` ' ` := image
+end set