diff --git a/library/theories/topology/basic.lean b/library/theories/topology/basic.lean
index f4f9ce7f9..bce954e2a 100644
--- a/library/theories/topology/basic.lean
+++ b/library/theories/topology/basic.lean
@@ -14,6 +14,14 @@ structure topology [class] (X : Type) :=
   (sUnion_mem_opens : ∀ {S : set (set X)}, S ⊆ opens → ⋃₀ S ∈ opens)
   (inter_mem_opens : ∀₀ s ∈ opens, ∀₀ t ∈ opens, s ∩ t ∈ opens)
 
+-- the bundled version
+structure TopologicalSpace : Type :=
+(carrier : Type) (struct : topology carrier)
+
+attribute TopologicalSpace.carrier [coercion]
+attribute TopologicalSpace.struct [instance]
+
+
 namespace topology
 
 variables {X : Type} [topology X]
diff --git a/library/theories/topology/continuous.lean b/library/theories/topology/continuous.lean
new file mode 100644
index 000000000..fc906010d
--- /dev/null
+++ b/library/theories/topology/continuous.lean
@@ -0,0 +1,314 @@
+/-
+Copyright (c) 2016 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jacob Gross, Jeremy Avigad
+
+Continuous functions.
+-/
+import theories.topology.basic algebra.category ..move
+open algebra eq.ops set topology function category sigma.ops
+
+namespace topology
+
+/- continuity on a set -/
+
+variables {X Y Z : Type} [topology X] [topology Y] [topology Z]
+
+definition continuous_on (f : X → Y) (s : set X) : Prop :=
+  ∀ ⦃t : set Y⦄, Open t → (∃ u : set X, Open u ∧ u ∩ s = f '- t ∩ s)
+
+theorem exists_Open_of_continous_on {f : X → Y} {s : set X} {t : set Y} (Ot : Open t)
+    (H : continuous_on f s) :
+  ∃ u : set X, Open u ∧ u ∩ s = f '- t ∩ s := H Ot
+
+theorem Open_preimage_inter_of_continuous_on {f : X → Y} {s : set X} (Os : Open s)
+    (Hcont : continuous_on f s) {t : set Y} (Ot : Open t) :
+  Open (f '- t ∩ s) :=
+obtain u [Ou Hu], from Hcont Ot,
+by rewrite[-Hu]; exact Open_inter Ou Os
+
+theorem continuous_on_of_forall_open {f : X → Y} {s : set X}
+    (H : ∀ t, Open t → Open (f '- t ∩ s)) :
+  continuous_on f s :=
+take t, assume Ot,
+have f '- t ∩ s ∩ s = f '- t ∩ s, by rewrite [inter_assoc, inter_self],
+exists.intro (f '- t ∩ s) (and.intro (H t Ot) this)
+
+theorem Open_preimage_of_continuous_on {f : X → Y} {s : set X} (Opens : Open s)
+    (contfs : continuous_on f s) {t : set Y} (Ot : Open t) (Hpre : f '- t ⊆ s) :
+  Open (f '- t) :=
+have f '- t ∩ s = f '- t, from inter_eq_self_of_subset Hpre,
+show Open (f '- t),
+  by rewrite -this; apply Open_preimage_inter_of_continuous_on Opens contfs Ot
+
+theorem exists_closed_of_continuous_on {f : X → Y} {s : set X}
+    (contfs : continuous_on f s) {t : set Y} (clt : closed t) :
+  ∃ u, closed u ∧ u ∩ s = f '- t ∩ s :=
+obtain v [Ov (Hv  : v ∩ s = f '- -t ∩ s)], from contfs clt,
+have -v ∩ s = f '- t ∩ s,
+  from inter_eq_inter_of_compl_inter_eq_compl_inter (by rewrite [compl_compl, Hv]),
+show ∃ u, closed u ∧ u ∩ s = f '- t ∩ s,
+  from exists.intro (-v) (and.intro (closed_compl Ov) this)
+
+theorem continuous_on_of_forall_closed' {f : X → Y} {s : set X}
+    (H : ∀ t, closed t → ∃ u, closed u ∧ u ∩ s = f '- t ∩ s) :
+  continuous_on f s :=
+take t : set Y, assume Ot : Open t,
+obtain (v : set X) [(clv : closed v) (Hv : v ∩ s = f '- (-t) ∩ s)], from H (-t) (closed_compl Ot),
+have (-v) ∩ s = f '- t ∩ s,
+  from inter_eq_inter_of_compl_inter_eq_compl_inter (by rewrite [compl_compl, Hv]),
+show ∃ u, Open u ∧ u ∩ s = f '- t ∩ s,
+  from exists.intro (-v) (and.intro clv this)
+
+theorem continuous_on_of_forall_closed {f : X → Y} {s : set X} (closeds : closed s)
+  (H : ∀ B, closed B → closed (f '- B ∩ s)) : continuous_on f s :=
+continuous_on_of_forall_closed'
+  (λ B HB, exists.intro _ (and.intro (H B HB) (by rewrite [inter_assoc, inter_self])))
+
+theorem closed_preimage_inter_of_continuous_on {f : X → Y} {s : set Y} (cls : closed s)
+    {t : set X} (clt : closed t) (contft : continuous_on f t) :
+  closed (f '- s ∩ t) :=
+obtain u [clu Hu], from exists_closed_of_continuous_on contft cls,
+by rewrite [-Hu]; exact (closed_inter clu clt)
+
+theorem continuous_on_subset {s t : set X} {f : X → Y} (Hs : continuous_on f s) (ts : t ⊆ s) :
+  continuous_on f t :=
+take u, assume Ou,
+obtain v [Ov Hv], from Hs Ou,
+have v ∩ t = f '- u ∩ t, by rewrite [-inter_eq_self_of_subset_right ts, -*inter_assoc, Hv],
+show ∃ v, Open v ∧ v ∩ t = f '- u ∩ t, from exists.intro v (and.intro Ov this)
+
+theorem continous_on_union_of_closed {f : X → Y} {s t : set X} (cls : closed s) (clt : closed t)
+    (contsf : continuous_on f s) (conttf : continuous_on f t) :
+  continuous_on f (s ∪ t) :=
+have ∀ u, closed u → closed (f '- u ∩ (s ∪ t)), from
+  begin
+    intro u clu,
+    rewrite [inter_distrib_left],
+    exact closed_union (closed_preimage_inter_of_continuous_on clu cls contsf)
+      (closed_preimage_inter_of_continuous_on clu clt conttf)
+  end,
+show continuous_on f (s ∪ t),
+  from continuous_on_of_forall_closed (closed_union cls clt) this
+
+theorem continuous_on_empty (f : X → Y) : continuous_on f ∅ :=
+continuous_on_of_forall_open
+  (take B, assume OpenB, by rewrite[inter_empty]; apply Open_empty)
+
+theorem continuous_on_union {f : X → Y} {s t : set X}
+    (Opens : Open s) (Opent : Open t) (contsf : continuous_on f s) (conttf : continuous_on f t) :
+  continuous_on f (s ∪ t) :=
+continuous_on_of_forall_open
+  (take B, assume OpenB,
+    have Open (f '- B ∩ s), from Open_preimage_inter_of_continuous_on Opens contsf OpenB,
+    have Open (f '- B ∩ t), from Open_preimage_inter_of_continuous_on Opent conttf OpenB,
+    show Open (f '- B ∩ (s ∪ t)),
+      by rewrite [inter_distrib_left]; apply Open_union; assumption; assumption)
+
+theorem continuous_on_id (s : set X) :  continuous_on (@id X) s :=
+λ B OpB, exists.intro B (and.intro OpB (by rewrite preimage_id))
+
+theorem continuous_on_comp {s : set X} {f : X → Y} {g : Y → Z}
+  (Hf : continuous_on f s) (Hg : continuous_on g (f ' s)) : continuous_on (g ∘ f) s :=
+take t, assume Ot,
+obtain (u : set Y) [(Ou : Open u) (Hu : u ∩ f ' s = g '- t ∩ f ' s)], from Hg Ot,
+obtain (v : set X) [(Ov : Open v) (Hv : v ∩ s = f '- u ∩ s)], from Hf Ou,
+have s ⊆ f '- (f ' s), from subset_preimage_image s f,
+have f '- (u ∩ f ' s) ∩ s = f '- (g '- t ∩ f ' s) ∩ s, by rewrite Hu,
+have f '- u ∩ s = f '- (g '- t) ∩ s,
+  begin
+    revert this,
+    rewrite [*preimage_inter, *inter_assoc, *inter_eq_self_of_subset_right `s  ⊆ f '- (f ' s)`],
+    intro H, exact H
+  end,
+show ∃ v, Open v ∧ v ∩ s = (g ∘ f) '- t ∩ s,
+  from exists.intro v (and.intro Ov (eq.trans Hv this))
+
+theorem continuous_on_comp' {s : set X} {t : set Y} {f : X → Y} {g : Y → Z}
+  (Hf : continuous_on f s) (Hg : continuous_on g t) (H : f ' s ⊆ t) : continuous_on (g ∘ f) s :=
+continuous_on_comp Hf (continuous_on_subset Hg H)
+
+section
+  open classical
+
+  theorem continuous_on_singleton (f : X → Y) (x : X) :
+    continuous_on f '{x} :=
+  take s, assume Ops,
+  if Hx : x ∈ f '- s then
+    have '{x} ⊆ f '- s, from singleton_subset_of_mem Hx,
+    exists.intro univ (and.intro Open_univ
+      (by rewrite [univ_inter, inter_eq_self_of_subset_right this]))
+  else
+    have f '- s ∩ '{x} = ∅,
+      from eq_empty_of_forall_not_mem
+        (take y, assume ymem,
+          obtain (Hy : y ∈ f '- s) (Hy' : y ∈ '{x}), from ymem,
+          have y = x, from eq_of_mem_singleton Hy',
+          show false, from Hx (by rewrite -this; apply Hy)),
+    exists.intro ∅ (and.intro Open_empty (by rewrite [this, empty_inter]))
+
+  theorem continuous_on_const (c : Y) (s : set X) :
+    continuous_on (λ x : X, c) s :=
+  take s, assume Ops,
+  if cs : c ∈ s then
+    have (λx, c) '- s = @univ X, from eq_univ_of_forall (take x, mem_preimage cs),
+    exists.intro univ (and.intro Open_univ (by rewrite this))
+  else
+    have (λx, c) '- s = (∅ : set X),
+      from eq_empty_of_forall_not_mem (take x, assume H, cs (mem_of_mem_preimage H)),
+    exists.intro ∅ (and.intro Open_empty (by rewrite this))
+end
+
+
+/- pointwise continuity on a set -/
+
+definition continuous_at_on (f : X → Y) (x : X) (s : set X) : Prop :=
+∀ ⦃t : set Y⦄, Open t → f x ∈ t → ∃ u, Open u ∧ x ∈ u ∧ u ∩ s ⊆ f '- t
+
+theorem continuous_at_on_of_continuous_on {f : X → Y} {s : set X}
+    (H : continuous_on f s) ⦃x : X⦄ (xs : x ∈ s) :
+  continuous_at_on f x s :=
+take u, assume (Ou : Open u) (fxu : f x ∈ u),
+obtain (t : set X) [(Ot : Open t) (Ht : t ∩ s = f '- u ∩ s)], from H Ou,
+have x ∈ f '- u ∩ s, from and.intro fxu xs,
+have x ∈ t, by rewrite [-Ht at this]; exact and.left this,
+exists.intro t (and.intro Ot (and.intro this (by rewrite Ht; apply inter_subset_left)))
+
+section
+open classical
+
+theorem continuous_on_of_forall_continuous_at_on {f : X → Y} {s : set X}
+    (H : ∀ x, continuous_at_on f x s) :
+  continuous_on f s :=
+take t, assume Ot : Open t,
+have H₁ : ∀₀ x ∈ f '- t, ∃ u', Open u' ∧ x ∈ u' ∧ u' ∩ s ⊆ f '- t,
+  from λ x xmem, H x Ot (mem_of_mem_preimage xmem),
+let u := ⋃₀ {u' | ∃ x (Hx : x ∈ f '- t), u' = some (H₁ Hx) } in
+have Open u, from Open_sUnion
+  (take u', assume Hu',
+    obtain x (Hx : x ∈ f '- t) (u'eq : u' = some (H₁ Hx)), from Hu',
+    show Open u', by rewrite u'eq; apply and.left (some_spec (H₁ Hx))),
+have Hu₁ : u ∩ s ⊆ f '- t, from
+  take x, assume Hx,
+  obtain xu xs, from Hx,
+  obtain u' [[x' (Hx' : x' ∈ f '- t) (u'eq : u' = some (H₁ Hx'))] (xu' : x ∈ u')], from xu,
+  have u' ∩ s ⊆ f '- t, by rewrite u'eq; exact and.right (and.right (some_spec (H₁ Hx'))),
+  show x ∈ f '- t, from this (and.intro xu' xs),
+have Hu₂ : f '- t ∩ s ⊆ u, from
+  take x, assume Hx : x ∈ f '- t ∩ s,
+  obtain xft xs, from Hx,
+  let u' := some (H₁ xft) in
+  have x ∈ u', from and.left (and.right (some_spec (H₁ xft))),
+  show x ∈ u, from exists.intro u' (and.intro (exists.intro x (exists.intro xft rfl)) this),
+show ∃ u, Open u ∧ u ∩ s = f '- t ∩ s,
+  from exists.intro u (and.intro `Open u` (inter_eq_inter_right Hu₁ Hu₂))
+
+end
+
+
+/- continuity -/
+
+definition continuous (f : X → Y) : Prop := ∀ ⦃s : set Y⦄, Open s → Open (f '- s)
+
+theorem continuous_of_continuous_on_univ {f : X → Y} (H : continuous_on f univ) : continuous f :=
+λ s Os, by rewrite [-inter_univ]; exact Open_preimage_inter_of_continuous_on Open_univ H Os
+
+theorem continuous_on_of_continuous {f : X → Y} (s : set X) (H : continuous f) :
+  continuous_on f s :=
+take t, assume Ot, exists.intro (f '- t) (and.intro (H Ot) rfl)
+
+theorem continuous_on_univ_of_continuous {f : X → Y} (H : continuous f) : continuous_on f univ :=
+continuous_on_of_continuous univ H
+
+theorem continuous_iff (f : X → Y) : continuous f ↔ continuous_on f univ :=
+iff.intro continuous_on_univ_of_continuous continuous_of_continuous_on_univ
+
+theorem Open_preimage_of_continuous {f : X → Y} (H : continuous f) ⦃s : set Y⦄ (Os : Open s) :
+  Open (f '- s) := H Os
+
+theorem closed_preimage_of_continuous {f : X → Y} (H : continuous f) {s : set Y} (cls : closed s) :
+  closed (f '- s) :=
+by rewrite [↑closed, -preimage_compl]; exact H cls
+
+theorem continuous_id : continuous (@id X) :=
+λ s Os, Os
+
+theorem continuous_comp {f : X → Y} {g : Y → Z}
+  (Hf : continuous f) (Hg : continuous g) : continuous (g ∘ f) :=
+λ s Os, Hf (Hg Os)
+
+theorem continuous_const (c : Y) : continuous (λ x : X, c) :=
+continuous_of_continuous_on_univ (continuous_on_const c univ)
+
+
+/- continuity at a point -/
+
+definition continuous_at' (f : X → Y) (x : X) : Prop :=
+∀ ⦃t : set Y⦄, Open t → f x ∈ t → ∃ u, Open u ∧ x ∈ u ∧ u ⊆ f '- t
+
+theorem continuous_at_of_continuous_at_on {f : X → Y} {x : X} {s : set X}
+    (Os : Open s) (xs : x ∈ s) (H : continuous_at_on f x s) :
+  continuous_at' f x :=
+take t, assume Ot fxt,
+obtain u Ou xu xssub, from H Ot fxt,
+exists.intro (u ∩ s) (and.intro (Open_inter Ou Os)
+  (and.intro (and.intro xu xs) xssub))
+
+theorem continuous_at_of_continuous_at_on_univ {f : X → Y} {x : X}
+    (H : continuous_at_on f x univ) :
+  continuous_at' f x :=
+continuous_at_of_continuous_at_on Open_univ !mem_univ H
+
+theorem continuous_at_on_univ_of_continuous_at {f : X → Y} {x : X}
+    (H : continuous_at' f x) :
+  continuous_at_on f x univ :=
+take t, assume Ot fxt,
+obtain u Ou xu usub, from H Ot fxt,
+have u ∩ univ ⊆ f '- t, by rewrite inter_univ; apply usub,
+exists.intro u (and.intro Ou (and.intro xu this))
+
+theorem continuous_at_iff_continuous_at_on_univ (f : X → Y) (x : X) :
+  continuous_at' f x ↔ continuous_at_on f x univ :=
+iff.intro continuous_at_on_univ_of_continuous_at continuous_at_of_continuous_at_on_univ
+
+
+/- The Category TOP -/
+
+section TOP
+open subtype
+
+private definition TOP_hom (A B : TopologicalSpace) : Type :=
+{f : A → B | continuous f}
+
+private definition TOP_ID {A : TopologicalSpace} : TOP_hom A A :=
+subtype.tag (@id A) continuous_id
+
+private definition TOP_comp ⦃ A B C : TopologicalSpace ⦄ (g : TOP_hom B C) (f : TOP_hom A B) :
+  TOP_hom A C :=
+subtype.tag (elt_of g ∘ elt_of f)
+  (continuous_comp (subtype.has_property f) (subtype.has_property g))
+
+private theorem TOP_assoc ⦃A B C D : TopologicalSpace⦄
+    (h : TOP_hom C D) (g : TOP_hom B C) (f : TOP_hom A B) :
+  TOP_comp h (TOP_comp g f) = TOP_comp (TOP_comp h g) f :=
+subtype.eq rfl
+
+private theorem id_left ⦃A B : TopologicalSpace ⦄ (f : TOP_hom A B) : TOP_comp TOP_ID f = f :=
+subtype.eq rfl
+
+private theorem id_right ⦃A B : TopologicalSpace ⦄ (f : TOP_hom A B) : TOP_comp f TOP_ID = f :=
+subtype.eq rfl
+
+definition TOP [reducible] [trans_instance] : category TopologicalSpace :=
+⦃ category,
+  hom := TOP_hom,
+  comp := TOP_comp,
+  ID := @TOP_ID,
+  assoc := TOP_assoc,
+  id_left := id_left,
+  id_right := id_right
+⦄
+
+end TOP
+
+end topology
diff --git a/library/theories/topology/topology.md b/library/theories/topology/topology.md
index 52b993697..e5f960e2b 100644
--- a/library/theories/topology/topology.md
+++ b/library/theories/topology/topology.md
@@ -3,4 +3,5 @@ theories.topology
 
 * [filterlim](filterlim.lean) : a general theory of limits, based on filters
 * [basic](basic.lean) : open and closed sets, separation axioms, and generated topologies
-* [order_topology](order_topology.lean)
\ No newline at end of file
+* [order_topology](order_topology.lean)
+* [continuous](continuous.lean) : continuous functions
\ No newline at end of file