diff --git a/category/fold.lean b/category/fold.lean
index 9e7737e09b067..972f7db85ab96 100644
--- a/category/fold.lean
+++ b/category/fold.lean
@@ -1,141 +1,145 @@
 /-
 Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Simon Hudon
+Authors: Simon Hudon, Sean Leather
 
-`foldl` and `foldr` generalized to any `traversable` collection.
+List folds generalized to `traversable`.
 -/
 
 import data.list.basic
 import category.traversable.instances
 import category.traversable.lemmas
 
-universes u v w
+universes u v
+
+open ulift
 
 namespace functor
 
-def foldl (α : Type u) (β : Type v) := α → α
-def foldr (α : Type u) (β : Type v) := α → α
+/- to_list -/
 
-def mfoldl (m : Type u → Type u) (α : Type u) (β : Type v) := α → m α
-def mfoldr (m : Type u → Type u) (α : Type u) (β : Type v) := α → m α
+def to_list (α : Type u) (β : Type v) : Type u := list α
 
-def to_list (α : Type u) (β : Type v) := list α
+namespace to_list
+variables {α : Type u} {β : Type v}
 
-def foldr.eval {α β} (x : foldr α β) : α → α := x
+def mk (x : α) : to_list α punit := [x]
 
-def foldl.eval {α β} (x : foldl α β) : α → α := x
+instance : applicative (to_list α) :=
+{ pure := λ _ _, [], seq := λ _ _ x y, (x ++ y : list α) }
 
-def fold.cons {α} (x : α) : to_list α punit :=
-[x]
+instance : is_lawful_applicative (to_list α) :=
+by refine {..}; intros; simp
 
-def foldl.cons {α β} (x : α) : foldl (list α) β :=
-list.cons x
+end to_list
 
-def foldr.cons {α β} (x : α) : foldr (list α) β :=
-list.cons x
+/- foldl -/
 
-def foldl.cons' {α} (x : α) : foldl (list α) punit :=
-list.cons x
+def foldl (α : Type u) (β : Type v) : Type u := α → α
 
-def foldr.cons' {α} (x : α) : foldr (list α) punit :=
-list.cons x
+namespace foldl
+variables {α : Type u} {β : Type v}
 
-def foldl.lift {α} (x : α → α) : foldl α punit := x
-def foldr.lift {α} (x : α → α) : foldr α punit := x
+def mk (x : α → α) : foldl α punit := x
 
-def mfoldl.lift {m : Type u → Type u} {α} (x : α → m α) : mfoldl m α punit := x
-def mfoldr.lift {m : Type u → Type u} {α} (x : α → m α) : mfoldr m α punit := x
+instance applicative : applicative (foldl α) :=
+{ pure := λ _ _, id, seq := λ _ _ f x, x ∘ f }
 
-end functor
+instance is_lawful_applicative : is_lawful_applicative (foldl α) :=
+by refine {..}; intros; refl
 
-instance {α} : applicative (functor.to_list α) :=
-{ pure := λ _ _, [],
-  seq := λ _ _ f x, (f ++ x : list α) }
+end foldl
 
-instance {α} : applicative (functor.foldr α) :=
-{ pure := λ _ _, id,
-  seq  := λ _ _ f x, f ∘ x }
+/- foldr -/
 
-instance {α} : applicative (functor.foldl α) :=
-{ pure := λ _ _, id,
-  seq  := λ _ _ f x, x ∘ f }
+def foldr (α : Type u) (β : Type v) : Type u := α → α
 
-variables {m : Type u → Type u} [monad m]
+namespace foldr
+variables {α : Type u} {β : Type v}
 
-instance {α} : applicative (functor.mfoldr m α) :=
-{ pure := λ _ _, pure,
-  seq  := λ _ _ f x i, x i >>= f }
+def mk (x : α → α) : foldr α punit := x
 
-instance {α} : applicative (functor.mfoldl m α) :=
-{ pure := λ _ _, pure,
-  seq  := λ _ _ f x i, f i >>= x }
+instance : applicative (foldr α) :=
+{ pure := λ _ _, id, seq := λ _ _ f x, f ∘ x }
 
-instance {α} : is_lawful_applicative (functor.to_list α) :=
-by { refine { .. }; dsimp; intros; simp }
+instance : is_lawful_applicative (foldr α) :=
+by refine {..}; intros; refl
 
-instance {α} : is_lawful_applicative (functor.foldr α) :=
-by refine { .. }; intros; refl
+end foldr
 
-instance {α} : is_lawful_applicative (functor.foldl α) :=
-by refine { .. }; intros; refl
+/- mfoldl -/
 
-variables [is_lawful_monad m]
+def mfoldl (m : Type u → Type u) (α : Type u) (β : Type v) : Type u := α → m α
 
-instance {α} : is_lawful_applicative (functor.mfoldr m α) :=
-by { refine { .. }; intros; ext; simp only with functor_norm }
+namespace mfoldl
+variables {α : Type u} {m : Type u → Type u}
 
-instance {α} : is_lawful_applicative (functor.mfoldl m α) :=
-by { refine { .. }; intros; ext; simp only with functor_norm }
+def mk (x : α → m α) : mfoldl m α punit := x
 
-namespace traversable
+variable [monad m]
 
-open functor
+instance : applicative (mfoldl m α) :=
+{ pure := λ _ _, pure, seq  := λ _ _ f g i, f i >>= g }
 
-variables {t : Type u → Type u} [traversable t]
-open list (hiding mfoldl mfoldr)
+instance [is_lawful_monad m] : is_lawful_applicative (mfoldl m α) :=
+by refine {..}; intros; ext; simp only with functor_norm
 
-def foldl {α β} (f : α → β → α) (x : α) (xs : t β) : α :=
-foldl.eval (traverse (foldl.lift ∘ flip f) xs) x
+end mfoldl
 
-def foldr {α β} (f : α → β → β) (x : β) (xs : t α) : β :=
-foldr.eval (traverse (foldr.lift ∘ f) xs) x
+/- mfoldr -/
 
-def mfoldl {α β} (f : α → β → m α) (x : α) (xs : t β) : m α :=
-(traverse (mfoldl.lift ∘ flip f) xs) x
+def mfoldr (m : Type u → Type u) (α : Type u) (β : Type v) : Type u := α → m α
 
-def mfoldr {α β} (f : α → β → m β) (x : β) (xs : t α) : m β :=
-(traverse (mfoldr.lift ∘ f) xs) x
+namespace mfoldr
+variables {α : Type u} {m : Type u → Type u}
 
-def foldl' {α β : Type u} (f : α → β → α) (x : α) (xs : t β) : α :=
-list.foldl f x (traverse fold.cons xs)
+def mk (x : α → m α) : mfoldr m α punit := x
 
-def foldr' {α β : Type u} (f : β → α → α) (x : α) (xs : t β) : α :=
-list.foldr f x (traverse fold.cons xs)
+variable [monad m]
 
-def mfoldl' {α β : Type u} (f : α → β → m α) (x : α) (xs : t β) : m α :=
-list.mfoldl f x (traverse fold.cons xs)
+instance : applicative (mfoldr m α) :=
+{ pure := λ _ _, pure, seq  := λ _ _ f g i, g i >>= f }
 
-def mfoldr' {α β : Type u} (f : β → α → m α) (x : α) (xs : t β) : m α :=
-list.mfoldr f x (traverse fold.cons xs)
+instance [is_lawful_monad m] : is_lawful_applicative (mfoldr m α) :=
+by refine {..}; intros; ext; simp only with functor_norm
 
-def to_list {α} (x : t α) : list α :=
-(foldl (flip cons) [] x).reverse
+end mfoldr
 
-def to_list' {α} (xs : t α) : list α :=
-traverse fold.cons xs
+end functor
 
-open ulift
+namespace traversable
+open functor
+
+section defs
+variables {α β : Type u} {t : Type u → Type u} [traversable t]
 
-def length {α} (xs : t α) : ℕ :=
-down $ foldl (λ l _, up $ 1+down l) (up 0) xs
+def foldl (f : α → β → α) (x : α) (xs : t β) : α :=
+traverse (foldl.mk ∘ flip f) xs x
+
+def foldr (f : α → β → β) (x : β) (xs : t α) : β :=
+traverse (foldr.mk ∘ f) xs x
+
+def to_list : t α → list α :=
+traverse to_list.mk
+
+def length (xs : t α) : ℕ :=
+down $ foldl (λ l _, up $ l.down + 1) (up 0) xs
+
+variables {m : Type u → Type u} [monad m]
+
+def mfoldl (f : α → β → m α) (x : α) (xs : t β) : m α :=
+traverse (mfoldl.mk ∘ flip f) xs x
+
+def mfoldr (f : α → β → m β) (x : β) (xs : t α) : m β :=
+traverse (mfoldr.mk ∘ f) xs x
+
+end defs
 
 section applicative_transformation
+variables {α β γ : Type u}
 
 open function
 
-variables {α α' β γ : Type u}
-
 def map_fold (f : α → β) :
   applicative_transformation (functor.to_list α) (functor.to_list β) :=
 { app := λ x h, (f <$> h : list _),
@@ -145,27 +149,27 @@ def map_fold (f : α → β) :
 def fold_foldl (f : β → α → β) :
   applicative_transformation (functor.to_list α) (functor.foldl β) :=
 { app := λ a h x, list.foldl f x h,
-  preserves_seq'  := by { intros, simp only [foldl_append] },
+  preserves_seq'  := by { intros, simp only [list.foldl_append] },
   preserves_pure' := by { intros, ext, refl } }
 
 def fold_foldr (f : α → β → β) :
   applicative_transformation (functor.to_list α) (functor.foldr β) :=
 { app := λ a h x, list.foldr f x h,
-  preserves_seq'  := by { intros, simp only [foldr_append] },
+  preserves_seq'  := by { intros, simp only [list.foldr_append] },
   preserves_pure' := by { intros, ext, refl } }
 
-variable m
+variables (m : Type u → Type u) [monad m] [is_lawful_monad m]
 
 def fold_mfoldl (f : β → α → m β) :
   applicative_transformation (functor.to_list α) (functor.mfoldl m β) :=
 { app := λ a h x, list.mfoldl f x h,
-  preserves_seq'  := by { intros, simp only [mfoldl_append] with functor_norm },
+  preserves_seq'  := by { intros, simp only [list.mfoldl_append] with functor_norm },
   preserves_pure' := by { intros, ext, refl } }
 
 def fold_mfoldr (f : α → β → m β) :
   applicative_transformation (functor.to_list α) (functor.mfoldr m β) :=
 { app := λ a h x, list.mfoldr f x h,
-  preserves_seq'  := by { intros, simp only [mfoldr_append] with functor_norm },
+  preserves_seq'  := by { intros, simp only [list.mfoldr_append] with functor_norm },
   preserves_pure' := by { intros, ext, refl } }
 
 lemma foldl_to_natural {i} (f : α → β → α) (x : functor.to_list β i) (a : α) :
@@ -183,117 +187,82 @@ lemma mfoldr_to_natural {i} (f : β → α → m α) (x : functor.to_list β i)
   list.mfoldr f a x = fold_mfoldr m f x a := rfl
 
 lemma fold_mfoldl_cons (f : α → β → m α) (x : β) :
-  (fold_mfoldl m f) (fold.cons x) = flip f x :=
-by unfold_coes; ext; simp [fold_mfoldl,fold.cons,list.mfoldl,flip]
+  (fold_mfoldl m f) (to_list.mk x) = flip f x :=
+by unfold_coes; ext; simp [fold_mfoldl, to_list.mk, list.mfoldl, flip]
 
 lemma fold_mfoldr_cons (f : β → α → m α) (x : β) :
-  (fold_mfoldr m f) (fold.cons x) = f x :=
-by unfold_coes; ext; simp [fold_mfoldr,fold.cons,list.mfoldr,flip]
+  (fold_mfoldr m f) (to_list.mk x) = f x :=
+by unfold_coes; ext; simp [fold_mfoldr, to_list.mk, list.mfoldr, flip]
 
 lemma map_to_natural (x : functor.to_list α γ) (f : α → β) :
   list.map f x = map_fold f x := rfl
 
-open is_lawful_traversable
-variables [is_lawful_traversable t]
-
 end applicative_transformation
 
+section equalities
 open is_lawful_traversable
+variables {α β γ : Type u}
+variables {t : Type u → Type u} [traversable t] [is_lawful_traversable t]
 
-variables [is_lawful_traversable t]
+lemma foldl_to_list (f : α → β → α) (xs : t β) (x : α) :
+  foldl f x xs = list.foldl f x (to_list xs) :=
+by simp only [foldl, to_list, naturality, foldl_to_natural]; refl
 
-lemma foldl_eq_foldl' {α β} (f : α → β → α) (xs : t β) (x : α) :
-  foldl f x xs = foldl' f x xs :=
-by { simp only [foldl,foldl',naturality,foldl_to_natural], refl }
+lemma foldr_to_list (f : α → β → β) (xs : t α) (x : β) :
+  foldr f x xs = list.foldr f x (to_list xs) :=
+by simp only [foldr, to_list, naturality, foldr_to_natural]; refl
 
-lemma to_list'_map {α β} (f : α → β) (xs : t α) :
-  to_list' (f <$> xs) = f <$> to_list' xs :=
-by simp [to_list',traverse_map,map_to_natural,naturality]; refl
+lemma to_list_map (f : α → β) (xs : t α) :
+  to_list (f <$> xs) = f <$> to_list xs :=
+by simp [to_list, traverse_map, map_to_natural, naturality]; refl
 
-@[simp] theorem foldl_map {α β γ} (g : β → γ) (f : α → γ → α) (a : α) (l : t β) :
+@[simp] theorem foldl_map (g : β → γ) (f : α → γ → α) (a : α) (l : t β) :
   foldl f a (g <$> l) = foldl (λ x y, f x (g y)) a l :=
-by simp only [foldl,traverse_map]; refl
+by simp only [foldl, traverse_map]; refl
 
-@[simp] theorem foldr_map {α β γ} (g : β → γ) (f : γ → α → α) (a : α) (l : t β) :
+@[simp] theorem foldr_map (g : β → γ) (f : γ → α → α) (a : α) (l : t β) :
   foldr f a (g <$> l) = foldr (f ∘ g) a l :=
-by simp only [foldr,traverse_map]
-
-@[simp] theorem mfoldl_map {α β γ} (g : β → γ) (f : α → γ → m α) (a : α) (l : t β) :
-  mfoldl f a (g <$> l) = mfoldl (λ x y, f x (g y)) a l :=
-by simp only [mfoldl,traverse_map]; refl
-
-@[simp] theorem mfoldr_map {α β γ} (g : β → γ) (f : γ → α → m α) (a : α) (l : t β) :
-  mfoldr f a (g <$> l) = mfoldr (f ∘ g) a l :=
-by simp only [mfoldr,traverse_map]
+by simp only [foldr, traverse_map]
 
-lemma to_list_eq_to_list'  {α} (xs : t α) :
-   to_list xs = to_list' xs :=
+@[simp] theorem to_list_eq_self {xs : list α} : to_list xs = xs :=
 begin
-  transitivity reverse (list.foldl (flip list.cons) [] (traverse fold.cons xs : list α)),
-  { rw [foldl_to_natural,naturality], refl,},
-  { apply reverse_inj.1,
-    simp only [to_list'],
-    generalize : (traverse fold.cons xs) = ys, clear xs,
-    suffices : list.foldl (flip cons) nil ys = (reverse ys ++ [] : list α),
-    { simpa },
-    generalize : nil = zs,
-    induction ys generalizing zs, simp, simp, rw ys_ih, refl },
+  unfold to_list traverse,
+  induction xs,
+  case list.nil { refl },
+  case list.cons : _ _ ih { unfold list.traverse to_list.mk, rw ih, refl }
 end
 
-@[simp] theorem to_list_map {α β} (f : α → β) (l : t α) : to_list (f <$> l) = f <$> to_list l :=
-by simp only [to_list_eq_to_list',to_list'_map]
-
-lemma list_foldl_eq {α β} (f : α → β → α) (x : α) (xs : t β) :
-  foldl f x xs = list.foldl f x (to_list xs) :=
-by simp only [to_list_eq_to_list',to_list',foldl_to_natural,naturality]; refl
+theorem length_to_list {xs : t α} : length xs = list.length (to_list xs) :=
+begin
+  unfold length,
+  rw foldl_to_list,
+  generalize : to_list xs = ys,
+  transitivity list.foldl (λ n _, n + 1) 0 ys,
+  { generalize : 0 = n, induction ys with _ _ ih generalizing n, simp, simp only [list.foldl, ih (n+1)] },
+  { induction ys with _ tl ih, { simp }, { simp only [list.foldl, list.length],
+    transitivity list.foldl (λ n _, n + 1) 0 tl + 1,
+    { exact eq.symm (list.foldl_hom (λ n, n + 1) (λ n _, n + 1) (λ n _, n + 1) 0 (λ _ _, rfl) _) },
+    { rw ih } } }
+end
 
-lemma list_foldr_eq {α β} (f : α → β → β) (x : β) (xs : t α) :
-  foldr f x xs = list.foldr f x (to_list xs) :=
-by simp only [to_list_eq_to_list',to_list',foldr_to_natural,naturality]; refl
+variables {m : Type u → Type u} [monad m] [is_lawful_monad m]
 
-lemma list_mfoldl_eq {α β} (f : α → β → m α) (x : α) (xs : t β) :
+lemma mfoldl_to_list {f : α → β → m α} {x : α} {xs : t β} :
   mfoldl f x xs = list.mfoldl f x (to_list xs) :=
-by simp only [to_list_eq_to_list',to_list',mfoldl_to_natural,naturality,(∘),fold_mfoldl_cons] with functor_norm; refl
+by simp only [mfoldl, to_list, naturality, mfoldl_to_natural, (∘), fold_mfoldl_cons]; refl
 
-lemma list_mfoldr_eq {α β} (f : α → β → m β) (x : β) (xs : t α) :
+lemma mfoldr_to_list (f : α → β → m β) (x : β) (xs : t α) :
   mfoldr f x xs = list.mfoldr f x (to_list xs) :=
-by simp only [to_list_eq_to_list',to_list',mfoldr_to_natural,naturality,(∘),fold_mfoldr_cons] with functor_norm; refl
+by simp only [mfoldr, to_list, naturality, mfoldr_to_natural, (∘), fold_mfoldr_cons]; refl
 
-lemma length_to_list {α} (xs : t α) :
-  (to_list xs).length = length xs :=
-by { simp only [length,list_foldl_eq,flip],
-     rw [← list.foldr_reverse,← list.length_reverse],
-     generalize : list.reverse (to_list xs) = l,
-     induction l; simp [*], }
-
-end traversable
-
-open traversable
-
-open functor (hiding foldl foldr)
-
-lemma list.to_list_eq_self {α} (xs : list α) :
-  to_list xs = xs :=
-begin
-  simp only [traversable.to_list,traverse,foldl,foldl.eval,flip],
-  suffices : ∀ s, (list.traverse (foldl.lift ∘ list.cons) xs s).reverse = s.reverse ++ xs,
-  { rw [this], simp },
-  induction xs; intros s;
-  simp [list.traverse,pure,(<*>),(<$>),*,foldl.lift],
-end
-
-lemma list.list_foldl_eq {α β} (f : α → β → α) (x : α) (xs : list β) :
-  foldl f x xs = list.foldl f x xs :=
-by simp only [list_foldl_eq,list.to_list_eq_self]
+@[simp] theorem mfoldl_map (g : β → γ) (f : α → γ → m α) (a : α) (l : t β) :
+  mfoldl f a (g <$> l) = mfoldl (λ x y, f x (g y)) a l :=
+by simp only [mfoldl, traverse_map]; refl
 
-lemma list.list_foldr_eq {α β} (f : α → β → β) (x : β) (xs : list α) :
-  foldr f x xs = list.foldr f x xs :=
-by simp only [list_foldr_eq,list.to_list_eq_self]
+@[simp] theorem mfoldr_map (g : β → γ) (f : γ → α → m α) (a : α) (l : t β) :
+  mfoldr f a (g <$> l) = mfoldr (f ∘ g) a l :=
+by simp only [mfoldr, traverse_map]
 
-lemma list.list_mfoldl_eq {α β} (f : α → β → m α) (x : α) (xs : list β) :
-  traversable.mfoldl f x xs = list.mfoldl f x xs :=
-by simp only [list_mfoldl_eq,list.to_list_eq_self]
+end equalities
 
-lemma list.list_mfoldr_eq {α β} (f : α → β → m β) (x : β) (xs : list α) :
-  traversable.mfoldr f x xs = list.mfoldr f x xs :=
-by simp only [list_mfoldr_eq,list.to_list_eq_self]
+end traversable
diff --git a/data/list/basic.lean b/data/list/basic.lean
index 4be36cb747dc4..aa7477880a31a 100644
--- a/data/list/basic.lean
+++ b/data/list/basic.lean
@@ -1079,6 +1079,9 @@ by rw reverse_reverse l at t; rwa t
 | []     := rfl
 | (x::l) := by simp [foldr_eta l]
 
+@[simp] theorem reverse_foldl (l : list α) : reverse (foldl (λ t h, h :: t) [] l) = l :=
+by rw ←foldr_reverse; simp
+
 /-- Fold a function `f` over the list from the left, returning the list
   of partial results. `scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]` -/
 def scanl (f : α → β → α) : α → list β → list α