diff --git a/src/Lists.lagda b/src/Lists.lagda
index 5f3eb229..330049a9 100644
--- a/src/Lists.lagda
+++ b/src/Lists.lagda
@@ -14,6 +14,7 @@ import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)
 open Eq.≡-Reasoning
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Data.Nat.Properties.Simple using (distribʳ-*-+)
 \end{code}
 
 ## Lists
@@ -139,7 +140,8 @@ _++_ : ∀ {A : Set} → List A → List A → List A
 [] ++ ys = ys
 (x ∷ xs) ++ ys = x ∷ (xs ++ ys)
 \end{code}
-The type `A` is an implicit argument to append.
+The type `A` is an implicit argument to append, making it
+a *polymorphic* function (one that can be used at many types).
 The empty list appended to a list `ys` is the same as `ys`.
 A list with head `x` and tail `xs` appended to a list `ys`
 yields a list with head `x` and with tail consisting of
@@ -162,8 +164,12 @@ ex₂ =
     0 ∷ 1 ∷ 2 ∷ ([] ++ 3 ∷ 4 ∷ [])
   ≡⟨⟩
     0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ []
+  ≡⟨⟩
+    [ 0 , 1 , 2 , 3 , 4 ]
   ∎
 \end{code}
+Appending two lists requires time proportional to the
+number of elements in the first list.
 
 
 ## Reasoning about append
@@ -206,43 +212,90 @@ to the equivalence needed in the proof
     x ∷ (xs ++ (ys ++ zs)) ≡ x ∷ ((xs ++ ys) ++ zs)
 
 The section notation `(x ∷)` makes it convenient to invoke the congruence.
+Else we would need to write `cong (_∷_ x)` or `cong (λ xs → x ∷ xs)`, each
+of which is longer and less pleasing to read.
+
+It is also easy to show that `[]` is a left and right identity for `_++_`.
+That it is a left identity is immediate from the definition.
+\begin{code}
+++-identityˡ : ∀ {A : Set} (xs : List A) → [] ++ xs ≡ xs
+++-identityˡ xs =
+  begin
+    [] ++ xs
+  ≡⟨⟩
+    xs
+  ∎
+\end{code}
+That it is a right identity follows by simple induction.
+\begin{code}
+++-identityʳ : ∀ {A : Set} (xs : List A) → xs ++ [] ≡ xs
+++-identityʳ [] =
+  begin
+    [] ++ []
+  ≡⟨⟩
+    []
+  ∎
+++-identityʳ (x ∷ xs) =
+  begin
+    (x ∷ xs) ++ []
+  ≡⟨⟩
+    x ∷ (xs ++ [])
+  ≡⟨ cong (x ∷) (++-identityʳ xs) ⟩
+    x ∷ xs
+  ∎
+\end{code}
+These three properties establish that `_++_` and `[]` form
+a *monoid* over lists.
 
 ## Length
 
+Our next function finds the length of a list.
 \begin{code}
 length : ∀ {A : Set} → List A → ℕ
 length [] = zero
 length (x ∷ xs) = suc (length xs)
 \end{code}
+Again, it takes an implicit parameter `A`.
+The length of the empty list is zero.
+The length of the list with head `x` and tail `xs`
+is one greater than the length of its tail.
 
-## Reverse
-
-## Map
-
-## Fold
-
+Here is an example showing how to compute the length
+of `[ 0 , 1 , 2 ]`.
 \begin{code}
-map : ∀ {A B : Set} → (A → B) → List A → List B
-map f []       = []
-map f (x ∷ xs) = f x ∷ map f xs
-
-foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B
-foldr c n []       = n
-foldr c n (x ∷ xs) = c x (foldr c n xs)
-
-ex₃ : length ([ 1 , 2 , 3 ]) ≡ 3
-ex₃ = refl
-
-ex₄ : map (λ x → x * x) ([ 1 , 2 , 3 ]) ≡ [ 1 , 4 , 9 ]
-ex₄ = refl
-
-ex₅ : foldr _+_ 0 ([ 1 , 2 , 3 ]) ≡ 6
-ex₅ = refl
-
-ex₆ : length {ℕ} [] ≡ zero
-ex₆ = refl
+ex₃ : length ([ 0 , 1 , 2 ]) ≡ 3
+ex₃ =
+  begin
+    length ([ 0 , 1 , 2 ])
+  ≡⟨⟩
+    length (0 ∷ 1 ∷ 2 ∷ [])
+  ≡⟨⟩
+    suc (length (1 ∷ 2 ∷ []))
+  ≡⟨⟩
+    suc (suc (length (2 ∷ [])))
+  ≡⟨⟩
+    suc (suc (suc (length {ℕ} [])))
+  ≡⟨⟩
+    suc (suc (suc zero))
+  ≡⟨⟩
+    3
+  ∎
 \end{code}
+Computing the length of a list requires time
+proportional to the number of elements in the list.
 
+In the second-to-last line, we cannot write
+simply `length []`  but must instead write
+`length {ℕ} []`.  This is because Agda has
+insufficient information to infer the implicit
+parameter; after all, `[]` could just as well
+be an empty list with elements of any type.
+
+
+## Reasoning about length
+
+The length of one list appended to another is the
+sum of the lengths of the lists.
 \begin{code}
 length-++ : ∀ {A : Set} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
 length-++ {A} [] ys = 
@@ -264,6 +317,120 @@ length-++ (x ∷ xs) ys =
     length (x ∷ xs) + length ys
   ∎
 \end{code}
+The proof is by induction. The base case instantiates the
+first argument to `[]`, and follows by straightforward computation.
+As before, Agda cannot infer the implicit type parameter to `length`,
+and it must be given explicitly.
+The inductive case instantiates the first argument to `x ∷ xs`,
+and follows by straightforward computation combined with the
+inductive hypothesis.  As usual, the inductive hypothesis is indicated by a recursive
+invocation of the proof, in this case `length-++ xs ys`, and it is promoted
+by the congruence `cong suc`.
+
+
+## Reverse
+
+Using append, it is easy to formulate a function to reverse a list.
+\begin{code}
+reverse : ∀ {A : Set} → List A → List A
+reverse [] = []
+reverse (x ∷ xs) = reverse xs ++ [ x ]
+\end{code}
+The reverse of the empty list is the empty list.
+The reverse of the list with head `x` and tail `xs`
+is the reverse of its tail appended to a unit list
+containing its head.
+
+Here is an example showing how to reverse the list `[ 0 , 1 , 2 ]`.
+\begin{code}
+ex₄ : reverse ([ 0 , 1 , 2 ]) ≡ [ 2 , 1 , 0 ]
+ex₄ =
+  begin
+    reverse ([ 0 , 1 , 2 ])
+  ≡⟨⟩
+    reverse (0 ∷ 1 ∷ 2 ∷ [])
+  ≡⟨⟩
+    reverse (1 ∷ 2 ∷ []) ++ [ 0 ]
+  ≡⟨⟩
+    (reverse (2 ∷ []) ++ [ 1 ]) ++ [ 0 ]
+  ≡⟨⟩
+    ((reverse [] ++ [ 2 ]) ++ [ 1 ]) ++ [ 0 ]
+  ≡⟨⟩
+    (([] ++ [ 2 ]) ++ [ 1 ]) ++ [ 0 ]
+  ≡⟨⟩
+    (([] ++ 2 ∷ []) ++ 1 ∷ []) ++ 0 ∷ []
+  ≡⟨⟩
+    (2 ∷ [] ++ 1 ∷ []) ++ 0 ∷ []
+  ≡⟨⟩
+    2 ∷ ([] ++ 1 ∷ []) ++ 0 ∷ []
+  ≡⟨⟩
+    (2 ∷ 1 ∷ []) ++ 0 ∷ []
+  ≡⟨⟩
+    2 ∷ (1 ∷ [] ++ 0 ∷ [])
+  ≡⟨⟩
+    2 ∷ 1 ∷ ([] ++ 0 ∷ [])
+  ≡⟨⟩
+    2 ∷ 1 ∷ 0 ∷ []
+  ≡⟨⟩
+    [ 2 , 1 , 0 ]
+  ∎
+\end{code}
+Because append takes time proportional to the length
+of the first list, reversing a list in this way takes
+time proportional to the *square* of the length of the
+list, since `1 + ⋯ + n ≡ n * (n + 1) / 2`.
+
+\begin{code}
+upto : ℕ → List ℕ
+upto zero = []
+upto (suc n) = suc n ∷ upto n
+
+sum : List ℕ → ℕ
+sum [] = zero
+sum (x ∷ xs) = x + sum xs
+
+sum-upto : ∀ (n : ℕ) → 2 * sum (upto n) ≡ n * suc n
+sum-upto zero = refl
+sum-upto (suc n) = {!!}
+{-
+  begin
+    2 * sum (upto (suc n))
+  ≡⟨⟩
+    2 * sum (suc n ∷ upto n)
+  ≡⟨⟩
+    2 * (suc n + sum (upto n))
+  ≡⟨ +-dist-* 2 (suc n) (sum (upto n)) ⟩
+    (2 * suc n) + (2 * sum (upto n))
+  ≡⟨ cong (_+_ (2 * suc n)) (sup-upto n) ⟩
+    (2 * suc n) + (n * suc n)
+  ≡⟨ sym (+-dist-* 
+-}
+\end{code}
+
+
+
+## Reverse
+
+## Map
+
+## Fold
+
+\begin{code}
+map : ∀ {A B : Set} → (A → B) → List A → List B
+map f []       = []
+map f (x ∷ xs) = f x ∷ map f xs
+
+foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B
+foldr c n []       = n
+foldr c n (x ∷ xs) = c x (foldr c n xs)
+
+ex₅ : map (λ x → x * x) ([ 1 , 2 , 3 ]) ≡ [ 1 , 4 , 9 ]
+ex₅ = refl
+
+ex₆ : foldr _+_ 0 ([ 1 , 2 , 3 ]) ≡ 6
+ex₆ = refl
+\end{code}
+
 
 \begin{code}
 data _∈_ {A : Set} (x : A) : List A → Set where
diff --git a/src/extra/Dummy.agda b/src/extra/Dummy.agda
new file mode 100644
index 00000000..2a0095ac
--- /dev/null
+++ b/src/extra/Dummy.agda
@@ -0,0 +1,3 @@
+import Data.List.Properties
+import Data.Nat.Properties
+