diff --git a/category/applicative.lean b/category/applicative.lean
new file mode 100644
index 0000000000000..b8fa963f28dd4
--- /dev/null
+++ b/category/applicative.lean
@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2017 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Simon Hudon
+
+Instances for identity and composition functors
+-/
+
+import category.functor
+
+universe variables u v w
+
+section lemmas
+
+open function
+
+variables {f : Type u → Type v}
+variables [applicative f] [is_lawful_applicative f]
+variables {α β γ σ : Type u}
+
+attribute [functor_norm] seq_assoc pure_seq_eq_map map_pure seq_map_assoc map_seq
+
+lemma applicative.map_seq_map (g : α → β → γ) (h : σ → β) (x : f α) (y : f σ) :
+  (g <$> x) <*> (h <$> y) = (flip (∘) h ∘ g) <$> x <*> y :=
+by simp [flip] with functor_norm
+
+lemma applicative.pure_seq_eq_map' (g : α → β) :
+  (<*>) (pure g : f (α → β)) = (<$>) g :=
+by ext; simp with functor_norm
+
+end lemmas
+
+namespace comp
+
+open function (hiding comp)
+open functor
+
+variables {f : Type u → Type w} {g : Type v → Type u}
+
+variables [applicative f] [applicative g]
+
+protected def seq  {α β : Type v} : comp f g (α → β) → comp f g α → comp f g β
+| ⟨h⟩ ⟨x⟩ := ⟨has_seq.seq <$> h <*> x⟩
+
+instance : has_pure (comp f g) :=
+⟨λ _ x, ⟨pure $ pure x⟩⟩
+
+instance : has_seq (comp f g) :=
+⟨λ _ _ f x, comp.seq f x⟩
+
+@[simp]
+protected lemma run_pure {α : Type v} :
+  ∀ x : α, (pure x : comp f g α).run = pure (pure x)
+| _ := rfl
+
+@[simp]
+protected lemma run_seq {α β : Type v} :
+  ∀ (h : comp f g (α → β)) (x : comp f g α),
+  (h <*> x).run = (<*>) <$> h.run <*> x.run
+| ⟨_⟩ ⟨_⟩ := rfl
+
+variables [is_lawful_applicative f] [is_lawful_applicative g]
+variables {α β γ : Type v}
+
+lemma map_pure (h : α → β) (x : α) : (h <$> pure x : comp f g β) = pure (h x) :=
+by ext; simp
+
+lemma seq_pure (h : comp f g (α → β)) (x : α) :
+  h <*> pure x = (λ g : α → β, g x) <$> h :=
+by ext; simp [(∘)] with functor_norm
+
+lemma seq_assoc (x : comp f g α) (h₀ : comp f g (α → β)) (h₁ : comp f g (β → γ)) :
+   h₁ <*> (h₀ <*> x) = (@function.comp α β γ <$> h₁) <*> h₀ <*> x :=
+by ext; simp [(∘)] with functor_norm
+
+lemma pure_seq_eq_map (h : α → β)  (x : comp f g α) :
+  pure h <*> x = h <$> x :=
+by ext; simp [applicative.pure_seq_eq_map'] with functor_norm
+
+instance {f : Type u → Type w} {g : Type v → Type u}
+  [applicative f] [applicative g] :
+  applicative (comp f g) :=
+{ map := @comp.map f g _ _,
+  seq := @comp.seq f g _ _,
+  ..comp.has_pure }
+
+instance {f : Type u → Type w} {g : Type v → Type u}
+  [applicative f] [applicative g]
+  [is_lawful_applicative f] [is_lawful_applicative g] :
+  is_lawful_applicative (comp f g) :=
+{ pure_seq_eq_map := @comp.pure_seq_eq_map f g _ _ _ _,
+  map_pure := @comp.map_pure f g _ _ _ _,
+  seq_pure := @comp.seq_pure f g _ _ _ _,
+  seq_assoc := @comp.seq_assoc f g _ _ _ _ }
+
+end comp
+open functor
+
+@[functor_norm]
+lemma comp.seq_mk {α β : Type w}
+  {f : Type u → Type v} {g : Type w → Type u}
+  [applicative f] [applicative g]
+  (h : f (g (α → β))) (x : f (g α)) :
+  comp.mk h <*> comp.mk x = comp.mk (has_seq.seq <$> h <*> x) := rfl
diff --git a/category/basic.lean b/category/basic.lean
index 07c3fe2e130e6..4e057c19685d8 100644
--- a/category/basic.lean
+++ b/category/basic.lean
@@ -6,7 +6,7 @@ Authors: Johannes Hölzl
 Extends the theory on functors, applicatives and monads.
 -/
 
-universes u v w x y
+universes u v
 variables {α β γ : Type u}
 
 notation a ` $< `:1 f:1 := f a
@@ -16,7 +16,7 @@ variables {f : Type u → Type v} [functor f] [is_lawful_functor f]
 
 run_cmd mk_simp_attr `functor_norm
 
-@[functor_norm] theorem map_map (m : α → β) (g : β → γ) (x : f α) :
+@[functor_norm] protected theorem map_map (m : α → β) (g : β → γ) (x : f α) :
   g <$> (m <$> x) = (g ∘ m) <$> x :=
 (comp_map _ _ _).symm
 
@@ -25,13 +25,31 @@ run_cmd mk_simp_attr `functor_norm
 end functor
 
 section applicative
-variables {f : Type u → Type v} [applicative f] [is_lawful_applicative f]
+variables {f : Type u → Type v} [applicative f]
+
+def mzip_with
+  {α₁ α₂ φ : Type u}
+  (g : α₁ → α₂ → f φ) :
+  Π (ma₁ : list α₁) (ma₂: list α₂), f (list φ)
+| (x :: xs) (y :: ys) := (::) <$> g x y <*> mzip_with xs ys
+| _ _ := pure []
+
+def mzip_with'  (g : α → β → f γ) : list α → list β → f punit
+| (x :: xs) (y :: ys) := g x y *> mzip_with' xs ys
+| [] _ := pure punit.star
+| _ [] := pure punit.star
+
+variables [is_lawful_applicative f]
 
 attribute [functor_norm] seq_assoc pure_seq_eq_map
 
 @[simp] theorem pure_id'_seq (x : f α) : pure (λx, x) <*> x = x :=
 pure_id_seq x
 
+variables  [is_lawful_applicative f]
+
+attribute [functor_norm] seq_assoc pure_seq_eq_map
+
 @[functor_norm] theorem seq_map_assoc (x : f (α → β)) (g : γ → α) (y : f γ) :
   (x <*> (g <$> y)) = (λ(m:α→β), m ∘ g) <$> x <*> y :=
 begin
@@ -51,7 +69,7 @@ section monad
 variables {m : Type u → Type v} [monad m] [is_lawful_monad m]
 
 lemma map_bind (x : m α) {g : α → m β} {f : β → γ} : f <$> (x >>= g) = (x >>= λa, f <$> g a) :=
-by simp [bind_assoc, (∘), (bind_pure_comp_eq_map _ _ _).symm]
+by rw [← bind_pure_comp_eq_map,bind_assoc]; simp [bind_pure_comp_eq_map]
 
 lemma seq_bind_eq (x : m α) {g : β → m γ} {f : α → β} : (f <$> x) >>= g = (x >>= g ∘ f) :=
 show bind (f <$> x) g = bind x (g ∘ f),
@@ -85,10 +103,3 @@ calc f <$> a <*> b = (λp:α×β, f p.1 p.2) <$> (prod.mk <$> a <*> b) :
   ... = (λb a, f a b) <$> b <*> a :
     by rw [is_comm_applicative.commutative_prod];
         simp [seq_map_assoc, map_seq, seq_assoc, seq_pure, map_map]
-
-def mmap₂
-  {α₁ α₂ φ : Type u} {m : Type u → Type*} [applicative m]
-  (f : α₁ → α₂ → m φ)
-: Π (ma₁ : list α₁) (ma₂: list α₂), m (list φ)
- | (x :: xs) (y :: ys) := (::) <$> f x y <*> mmap₂ xs ys
- | _ _ := pure []
diff --git a/category/functor.lean b/category/functor.lean
new file mode 100644
index 0000000000000..fc6e05c17763a
--- /dev/null
+++ b/category/functor.lean
@@ -0,0 +1,114 @@
+/-
+Copyright (c) 2017 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Simon Hudon
+
+Standard identity and composition functors
+-/
+import tactic.ext
+import category.basic
+
+universe variables u v w
+
+section functor
+
+variables {F : Type u → Type v}
+variables {α β γ : Type u}
+variables [functor F] [is_lawful_functor F]
+
+lemma functor.map_id : (<$>) id = (id : F α → F α) :=
+by apply funext; apply id_map
+
+lemma functor.map_comp_map (f : α → β) (g : β → γ) :
+  ((<$>) g ∘ (<$>) f : F α → F γ) = (<$>) (g ∘ f) :=
+by apply funext; intro; rw comp_map
+
+end functor
+
+def id.mk {α : Sort u} : α → id α := id
+
+namespace functor
+
+/-- `functor.comp` is a wrapper around `function.comp` for types.
+    It prevents Lean's type class resolution mechanism from trying
+    a `functor (comp f id)` when `functor f` would do. -/
+structure comp (f : Type u → Type w) (g : Type v → Type u) (α : Type v) : Type w :=
+(run : f $ g α)
+
+@[extensionality]
+protected lemma comp.ext {f : Type u → Type w} {g : Type v → Type u} {α : Type v} :
+  ∀ {x y : comp f g α}, x.run = y.run → x = y
+| ⟨x⟩ ⟨._⟩ rfl := rfl
+
+namespace comp
+
+variables {f : Type u → Type w} {g : Type v → Type u}
+
+variables [functor f] [functor g]
+
+protected def map {α β : Type v} (h : α → β) : comp f g α → comp f g β
+| ⟨x⟩ := ⟨(<$>) h <$> x⟩
+
+variables [is_lawful_functor f] [is_lawful_functor g]
+variables {α β γ : Type v}
+
+protected lemma id_map : ∀ (x : comp f g α), comp.map id x = x
+| ⟨x⟩ :=
+by simp [comp.map,functor.map_id]
+
+protected lemma comp_map (g_1 : α → β) (h : β → γ) : ∀ (x : comp f g α),
+           comp.map (h ∘ g_1) x = comp.map h (comp.map g_1 x)
+| ⟨x⟩ :=
+by simp [comp.map,functor.map_comp_map g_1 h] with functor_norm
+
+instance {f : Type u → Type w} {g : Type v → Type u}
+  [functor f] [functor g] :
+  functor (comp f g) :=
+{ map := @comp.map f g _ _ }
+
+@[simp]
+protected lemma run_map {α β : Type v} (h : α → β) :
+  ∀ x : comp f g α, (h <$> x).run = (<$>) h <$> x.run
+| ⟨_⟩ := rfl
+
+instance {f : Type u → Type w} {g : Type v → Type u}
+  [functor f] [functor g]
+  [is_lawful_functor f] [is_lawful_functor g] :
+  is_lawful_functor (comp f g) :=
+{ id_map := @comp.id_map f g _ _ _ _,
+  comp_map := @comp.comp_map f g _ _ _ _ }
+
+end comp
+
+@[functor_norm]
+lemma comp.map_mk {α β : Type w}
+  {f : Type u → Type v} {g : Type w → Type u}
+  [functor f] [functor g]
+  (h : α → β) (x : f (g α)) :
+  h <$> comp.mk x = comp.mk ((<$>) h <$> x) := rfl
+
+end functor
+
+namespace ulift
+
+instance : functor ulift :=
+{ map := λ α β f, up ∘ f ∘ down }
+
+end ulift
+
+namespace sum
+
+variables {γ α β : Type v}
+
+protected def mapr (f : α → β) : γ ⊕ α → γ ⊕ β
+| (inl x) := inl x
+| (inr x) := inr (f x)
+
+instance : functor (sum γ) :=
+{ map := @sum.mapr γ }
+
+instance : is_lawful_functor.{v} (sum γ) :=
+{ id_map := by intros; casesm _ ⊕ _; refl,
+  comp_map := by intros; casesm _ ⊕ _; refl }
+
+end sum
diff --git a/data/prod.lean b/data/prod.lean
index 7b3e402d2f6fc..a17933cefe298 100644
--- a/data/prod.lean
+++ b/data/prod.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 
 Extends theory on products
 -/
+import tactic.ext
 
 universes u v
 variables {α : Type u} {β : Type v}
@@ -23,6 +24,7 @@ namespace prod
 lemma ext_iff {p q : α × β} : p = q ↔ p.1 = q.1 ∧ p.2 = q.2 :=
 by rw [← @mk.eta _ _ p, ← @mk.eta _ _ q, mk.inj_iff]
 
+@[extensionality]
 lemma ext {α β} {p q : α × β} : p.1 = q.1 → p.2 = q.2 → p = q :=
 by rw [ext_iff] ; intros ; split ; assumption
 
@@ -60,4 +62,3 @@ theorem lex_def (r : α → α → Prop) (s : β → β → Prop)
  end⟩
 
 end prod
-
diff --git a/data/set/basic.lean b/data/set/basic.lean
index e772c8268cdde..4765bf4fe2cda 100644
--- a/data/set/basic.lean
+++ b/data/set/basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad, Leonardo de Moura
 -/
-import tactic tactic.finish data.subtype
+import tactic.ext tactic.finish data.subtype
 open function
 
 namespace set
diff --git a/tactic/ext.lean b/tactic/ext.lean
new file mode 100644
index 0000000000000..b43dd6c3ed9b8
--- /dev/null
+++ b/tactic/ext.lean
@@ -0,0 +1,75 @@
+
+import tactic.basic
+
+/--
+ Tag lemmas of the form:
+
+ ```
+ lemma my_collection.ext (a b : my_collection)
+   (h : ∀ x, a.lookup x = b.lookup y) :
+   a = b := ...
+ ```
+ -/
+@[user_attribute]
+meta def extensional_attribute : user_attribute :=
+{ name := `extensionality,
+  descr := "lemmas usable by `ext` tactic" }
+
+attribute [extensionality] _root_.funext array.ext
+
+namespace tactic
+open interactive interactive.types
+open lean.parser nat
+
+local postfix `?`:9001 := optional
+local postfix *:9001 := many
+
+/--
+  `ext1 id` selects and apply one extensionality lemma (with attribute
+  `extensionality`), using `id`, if provided, to name a local constant
+  introduced by the lemma. If `id` is omitted, the local constant is
+  named automatically, as per `intro`.
+ -/
+meta def interactive.ext1 (x : parse ident_ ?) : tactic unit :=
+do ls ← attribute.get_instances `extensionality,
+   ls.any_of (λ l, applyc l) <|> fail "no applicable extensionality rule found",
+   try ( interactive.intro x )
+
+meta def ext_arg :=
+prod.mk <$> (some <$> small_nat)
+        <*> (tk "with" *> ident_* <|> pure [])
+<|> prod.mk none <$> (ident_*)
+
+/--
+  - `ext` applies as many extensionality lemmas as possible;
+  - `ext ids`, with `ids` a list of identifiers, finds extentionality and applies them
+    until it runs out of identifiers in `ids` to name the local constants.
+
+  When trying to prove:
+
+  ```
+  α β : Type,
+  f g : α → set β
+  ⊢ f = g
+  ```
+
+  applying `ext x y` yields:
+
+  ```
+  α β : Type,
+  f g : α → set β,
+  x : α,
+  y : β
+  ⊢ y ∈ f x ↔ y ∈ f x
+  ```
+
+  by applying functional extensionality and set extensionality.
+
+  A maximum depth can be provided with `ext 3 with x y z`.
+  -/
+meta def interactive.ext : parse ext_arg → tactic unit
+ | (some n, []) := interactive.ext1 none >> iterate_at_most (pred n) (interactive.ext1 none)
+ | (none,   []) := interactive.ext1 none >> repeat (interactive.ext1 none)
+ | (n, xs) := tactic.ext xs n
+
+end tactic
diff --git a/tactic/interactive.lean b/tactic/interactive.lean
index fa70e3ee76785..0242807be36f8 100644
--- a/tactic/interactive.lean
+++ b/tactic/interactive.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 import data.dlist data.dlist.basic data.prod category.basic
   tactic.basic tactic.rcases tactic.generalize_proofs
   tactic.split_ifs meta.expr logic.basic
+  tactic.ext
 
 open lean
 open lean.parser
@@ -289,70 +290,6 @@ done
 /-- Shorter name for the tactic `tautology`. -/
 meta def tauto := tautology
 
-/--
- Tag lemmas of the form:
-
- ```
- lemma my_collection.ext (a b : my_collection)
-   (h : ∀ x, a.lookup x = b.lookup y) :
-   a = b := ...
- ```
- -/
-@[user_attribute]
-meta def extensional_attribute : user_attribute :=
-{ name := `extensionality,
-  descr := "lemmas usable by `ext` tactic" }
-
-attribute [extensionality] _root_.funext array.ext prod.ext
-
-/--
-  `ext1 id` selects and apply one extensionality lemma (with attribute
-  `extensionality`), using `id`, if provided, to name a local constant
-  introduced by the lemma. If `id` is omitted, the local constant is
-  named automatically, as per `intro`.
- -/
-meta def ext1 (x : parse ident_ ?) : tactic unit :=
-do ls ← attribute.get_instances `extensionality,
-   ls.any_of (λ l, applyc l) <|> fail "no applicable extensionality rule found",
-   try ( interactive.intro x )
-
-meta def ext_arg :=
-prod.mk <$> (some <$> small_nat)
-        <*> (tk "with" *> ident_* <|> pure [])
-<|> prod.mk none <$> (ident_*)
-
-/--
-  - `ext` applies as many extensionality lemmas as possible;
-  - `ext ids`, with `ids` a list of identifiers, finds extentionality and applies them
-    until it runs out of identifiers in `ids` to name the local constants.
-
-  When trying to prove:
-
-  ```
-  α β : Type,
-  f g : α → set β
-  ⊢ f = g
-  ```
-
-  applying `ext x y` yields:
-
-  ```
-  α β : Type,
-  f g : α → set β,
-  x : α,
-  y : β
-  ⊢ y ∈ f x ↔ y ∈ f x
-  ```
-
-  by applying functional extensionality and set extensionality.
-
-  A maximum depth can be provided with `ext 3 with x y z`.
-  -/
-meta def ext : parse ext_arg → tactic unit
- | (some n, []) := ext1 none >> iterate_at_most (pred n) (ext1 none)
- | (none,   []) := ext1 none >> repeat (ext1 none)
- | (n, xs) := tactic.ext xs n
-
 private meta def generalize_arg_p_aux : pexpr → parser (pexpr × name)
 | (app (app (macro _ [const `eq _ ]) h) (local_const x _ _ _)) := pure (h, x)
 | _ := fail "parse error"
@@ -458,7 +395,7 @@ do    tgt ← target,
           , field_values := field_values ++ vs.map to_pexpr         ++ src_field_vals },
       tactic.exact e',
       gs ← with_enable_tags (
-        mmap₂ (λ (n : name × name) v, do
+        mzip_with (λ (n : name × name) v, do
            set_goals [v],
            try (interactive.unfold (provided.map $ λ ⟨s,f⟩, f.update_prefix s) (loc.ns [none])),
            apply_auto_param
diff --git a/tests/tactics.lean b/tests/tactics.lean
index 65d3eeafcb8ec..0337aefc90b99 100644
--- a/tests/tactics.lean
+++ b/tests/tactics.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
-import tactic data.set.lattice
+import tactic data.set.lattice data.prod
 
 section solve_by_elim
 example {a b : Prop} (h₀ : a → b) (h₁ : a) : b :=