diff --git a/src/plfa/Lists.lagda b/src/plfa/Lists.lagda
index 8c702ada..f7b03a2b 100644
--- a/src/plfa/Lists.lagda
+++ b/src/plfa/Lists.lagda
@@ -28,7 +28,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
 open import Function using (_∘_)
 open import Level using (Level)
-open import plfa.Isomorphism using (_≃_)
+open import plfa.Isomorphism using (_≃_; _⇔_)
 \end{code}
 
 
@@ -344,7 +344,7 @@ reversed, append takes time linear in the length of the first
 list, and the sum of the numbers up to `n - 1` is `n * (n - 1) / 2`.
 (We will validate that last fact in an exercise later in this chapter.)
 
-#### Exercise `reverse-++-commute`
+#### Exercise `reverse-++-commute` (recommended)
 
 Show that the reverse of one list appended to another is the
 reverse of the second appended to the reverse of the first.
@@ -354,7 +354,7 @@ postulate
     → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
 \end{code}
 
-#### Exercise `reverse-involutive`
+#### Exercise `reverse-involutive` (recommended)
 
 A function is an _involution_ if when applied twice it acts
 as the identity function.  Show that reverse is an involution.
@@ -766,6 +766,21 @@ foldr-monoid-++ _⊗_ e monoid-⊗ xs ys =
   ∎
 \end{code}
 
+#### Exercise `foldl`
+
+Define a function `foldl` which is analogous to `foldr`, but where
+operations associate to the left rather than the right.  For example,
+
+    foldr _⊗_ e [ x , y , z ]  =  x ⊗ (y ⊗ (z ⊗ e))
+    foldl _⊗_ e [ x , y , z ]  =  ((e ⊗ x) ⊗ y) ⊗ z
+
+
+#### Exercise `foldr-monoid-foldl`
+
+Show that if `_⊕_` and `e` form a monoid, then `foldr _⊗_ e` and
+`foldl _⊗_ e` always compute the same result.
+
+
 ## All {#All}
 
 We can also define predicates over lists. Two of the most important
@@ -843,19 +858,15 @@ possible evidence for `3 ≡ 0`, `3 ≡ 1`, `3 ≡ 0`, `3 ≡ 2`, and
 ## All and append
 
 A predicate holds for every element of one list appended to another if and
-only if it holds for every element of each list.  Indeed, an even stronger
-result is true, as we can show that the two types are isomorphic.
+only if it holds for every element of each list.
 \begin{code}
-All-++ : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
-  All P (xs ++ ys) ≃ (All P xs × All P ys)
-All-++ xs ys =
+All-++-⇔ : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
+  All P (xs ++ ys) ⇔ (All P xs × All P ys)
+All-++-⇔ xs ys =
   record
     { to       =  to xs ys
     ; from     =  from xs ys
-    ; from∘to  =  from∘to xs ys
-    ; to∘from  =  to∘from xs ys
     }
-
   where
 
   to : ∀ {A : Set} {P : A → Set} (xs ys : List A) →
@@ -868,24 +879,18 @@ All-++ xs ys =
     All P xs × All P ys → All P (xs ++ ys)
   from [] ys ⟨ [] , Pys ⟩ = Pys
   from (x ∷ xs) ys ⟨ Px ∷ Pxs , Pys ⟩ =  Px ∷ from xs ys ⟨ Pxs , Pys ⟩
-
-  from∘to : ∀ { A : Set} {P : A → Set} (xs ys : List A) →
-    ∀ (u : All P (xs ++ ys)) → from xs ys (to xs ys u) ≡ u
-  from∘to [] ys Pys = refl
-  from∘to (x ∷ xs) ys (Px ∷ Pxs++ys) = cong (Px ∷_) (from∘to xs ys Pxs++ys)
-
-  to∘from : ∀ { A : Set} {P : A → Set} (xs ys : List A) →
-    ∀ (v : All P xs × All P ys) → to xs ys (from xs ys v) ≡ v
-  to∘from [] ys ⟨ [] , Pys ⟩ = refl
-  to∘from (x ∷ xs) ys ⟨ Px ∷ Pxs , Pys ⟩ rewrite to∘from xs ys ⟨ Pxs , Pys ⟩ = refl
 \end{code}
 
-#### Exercise `Any-++`
+#### Exercise `Any-++-⇔` (recommended)
 
-Prove a result similar to `All-++`, but with `Any` in place of `All`, and a suitable
-replacement for `_×_`.  As a consequence, demonstrate an isomorphism relating
+Prove a result similar to `All-++-↔`, but with `Any` in place of `All`, and a suitable
+replacement for `_×_`.  As a consequence, demonstrate an equivalence relating
 `_∈_` and `_++_`.
 
+#### Exercise `All-++-≃` (stetch)
+
+Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
+
 #### Exercise `¬Any≃All¬` (stretch)
 
 First generalise composition to arbitrary levels, using
diff --git a/src/plfa/Properties.lagda b/src/plfa/Properties.lagda
index 6494d652..dd7dca88 100644
--- a/src/plfa/Properties.lagda
+++ b/src/plfa/Properties.lagda
@@ -342,7 +342,7 @@ Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`.
 Write out the proof of `progress′` in full, and compare it to the
 proof of `progress` above.
 
-#### Exercise `value?`
+#### Exercise `value?` (recommended)
 
 Combine `progress` and `—→¬V` to write a program that decides
 whether a well-typed term is a value.
@@ -1249,11 +1249,29 @@ _ = refl
 And again, the example in the previous section was derived by editing the
 above.
 
-#### Exercise `mul-example`
+#### Exercise `mul-example` (recommended)
 
 Using the evaluator, confirm that two times two is four.
 
 
+#### Exercise: `progress-preservation` (recommended)
+
+Without peeking at their statements above, write down the progress
+and preservation theorems for the simply typed lambda-calculus.
+
+
+#### Exercise `subject_expansion`
+
+We say that `M` _reduces_ to `N` if `M —→ N`,
+but we can also describe the same situation by saying
+that `N` _expands_ to `M`.
+The preservation property is sometimes called _subject reduction_.
+Its opposite is _subject expansion_, which holds if
+`M —→ N` and `∅ ⊢ N ⦂ A` imply `∅ ⊢ M ⦂ A`.
+Find two counter-examples to subject expansion, one
+with case expressions and one not involving case expressions.
+
+
 ## Well-typed terms don't get stuck
 
 A term is _normal_ if it cannot reduce.
@@ -1398,23 +1416,6 @@ checker complains, because the arguments have merely switched order
 and neither is smaller.
 
 
-#### Exercise: `progress-preservation`
-
-Without peeking at their statements above, write down the progress
-and preservation theorems for the simply typed lambda-calculus.
-
-
-#### Exercise `subject_expansion`
-
-We say that `M` _reduces_ to `N` if `M —→ N`,
-and conversely that `M` _expands_ to `N` if `N —→ M`.
-The preservation property is sometimes called _subject reduction_.
-Its opposite is _subject expansion_, which holds if
-`M —→ N` and `∅ ⊢ N ⦂ A` imply `∅ ⊢ M ⦂ A`.
-Find two counter-examples to subject expansion, one
-with case expressions and one not involving case expressions.
-
-
 #### Quiz
 
 Suppose we add a new term `zap` with the following reduction rule
diff --git a/tspl/Assignment3.lagda b/tspl/Assignment3.lagda
new file mode 100644
index 00000000..83eabb8f
--- /dev/null
+++ b/tspl/Assignment3.lagda
@@ -0,0 +1,373 @@
+---
+title     : "Assignment3: TSPL Assignment 3"
+layout    : page
+permalink : /Assignment3/
+---
+
+\begin{code}
+module Assignment3 where
+\end{code}
+
+## YOUR NAME AND EMAIL GOES HERE
+
+## Introduction
+
+This assignment is due **4pm Thursday 1 November** (Week 7).
+
+You must do _all_ the exercises labelled "(recommended)".
+
+Exercises labelled "(stretch)" are there to provide an extra challenge.
+You don't need to do all of these, but should attempt at least a few.
+
+Exercises without a label are optional, and may be done if you want
+some extra practice.
+
+Submit your homework using the "submit" command.
+Please ensure your files execute correctly under Agda!
+
+## Imports
+
+\begin{code}
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; cong; sym)
+open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
+open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
+open import Data.Nat.Properties using
+  (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Function using (_∘_)
+open import Level using (Level)
+open import plfa.Relations using (_<_; z<s; s<s)
+open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open plfa.Isomorphism.≃-Reasoning
+open import plfa.Lists using (List; []; _∷_; [_]; [_,_]; [_,_,_]; [_,_,_,_];
+  _++_; reverse; map; foldr; sum; Any; All; _∈_)
+open import plfa.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
+open import plfa.Properties hiding (value?)
+\end{code}
+
+#### Exercise `reverse-++-commute` (recommended)
+
+
+
+
+
+
+
+Show that the reverse of one list appended to another is the
+reverse of the second appended to the reverse of the first.
+\begin{code}
+postulate
+  reverse-++-commute : ∀ {A : Set} {xs ys : List A}
+    → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
+\end{code}
+
+#### Exercise `reverse-involutive` (recommended)
+
+A function is an _involution_ if when applied twice it acts
+as the identity function.  Show that reverse is an involution.
+\begin{code}
+postulate
+  reverse-involutive : ∀ {A : Set} {xs : List A}
+    → reverse (reverse xs) ≡ xs
+\end{code}
+
+#### Exercise `map-compose`
+
+Prove that the map of a composition is equal to the composition of two maps.
+\begin{code}
+postulate
+  map-compose : ∀ {A B C : Set} {f : A → B} {g : B → C}
+    → map (g ∘ f) ≡ map g ∘ map f
+\end{code}
+The last step of the proof requires extensionality.
+
+#### Exercise `map-++-commute`
+
+Prove the following relationship between map and append.
+\begin{code}
+postulate
+  map-++-commute : ∀ {A B : Set} {f : A → B} {xs ys : List A}
+   →  map f (xs ++ ys) ≡ map f xs ++ map f ys
+\end{code}
+
+#### Exercise `map-Tree`
+
+Define a type of trees with leaves of type `A` and internal
+nodes of type `B`.
+\begin{code}
+data Tree (A B : Set) : Set where
+  leaf : A → Tree A B
+  node : Tree A B → B → Tree A B → Tree A B
+\end{code}
+Define a suitabve map operator over trees.
+\begin{code}
+postulate
+  map-Tree : ∀ {A B C D : Set}
+    → (A → C) → (B → D) → Tree A B → Tree C D
+\end{code}
+
+#### Exercise `product` (recommended)
+
+Use fold to define a function to find the product of a list of numbers.
+For example,
+
+    product [ 1 , 2 , 3 , 4 ] ≡ 24
+
+#### Exercise `foldr-++` (recommended)
+
+Show that fold and append are related as follows.
+\begin{code}
+postulate
+  foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) (e : B) (xs ys : List A) →
+    foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ (foldr _⊗_ e ys) xs
+\end{code}
+
+
+#### Exercise `map-is-foldr`
+
+Show that map can be defined using fold.
+\begin{code}
+postulate
+  map-is-foldr : ∀ {A B : Set} {f : A → B} →
+    map f ≡ foldr (λ x xs → f x ∷ xs) []
+\end{code}
+This requires extensionality.
+
+#### Exercise `fold-Tree`
+
+Define a suitable fold function for the type of trees given earlier.
+\begin{code}
+postulate
+  fold-Tree : ∀ {A B C : Set}
+    → (A → C) → (C → B → C → C) → Tree A B → C
+\end{code}
+
+#### Exercise `map-is-fold-Tree`
+
+Demonstrate an anologue of `map-is-foldr` for the type of trees.
+
+#### Exercise `sum-downFrom` (stretch)
+
+Define a function that counts down as follows.
+\begin{code}
+downFrom : ℕ → List ℕ
+downFrom zero     =  []
+downFrom (suc n)  =  n ∷ downFrom n
+\end{code}
+For example,
+\begin{code}
+_ : downFrom 3 ≡ [ 2 , 1 , 0 ]
+_ = refl
+\end{code}
+Prove that the sum of the numbers `(n - 1) + ⋯ + 0` is
+equal to `n * (n ∸ 1) / 2`.
+\begin{code}
+postulate
+  sum-downFrom : ∀ (n : ℕ)
+    → sum (downFrom n) * 2 ≡ n * (n ∸ 1)
+\end{code}
+
+
+#### Exercise `foldl`
+
+Define a function `foldl` which is analogous to `foldr`, but where
+operations associate to the left rather than the right.  For example,
+
+    foldr _⊗_ e [ x , y , z ]  =  x ⊗ (y ⊗ (z ⊗ e))
+    foldl _⊗_ e [ x , y , z ]  =  ((e ⊗ x) ⊗ y) ⊗ z
+
+
+#### Exercise `foldr-monoid-foldl`
+
+Show that if `_⊕_` and `e` form a monoid, then `foldr _⊗_ e` and
+`foldl _⊗_ e` always compute the same result.
+
+
+#### Exercise `Any-++-⇔` (recommended)
+
+Prove a result similar to `All-++-↔`, but with `Any` in place of `All`, and a suitable
+replacement for `_×_`.  As a consequence, demonstrate an equivalence relating
+`_∈_` and `_++_`.
+
+
+#### Exercise `All-++-≃` (stetch)
+
+Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
+
+
+#### Exercise `¬Any≃All¬` (stretch)
+
+First generalise composition to arbitrary levels, using
+[universe polymorphism][plfa.Equality#unipoly].
+\begin{code}
+_∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
+  → (B → C) → (A → B) → A → C
+(g ∘′ f) x  =  g (f x)
+\end{code}
+
+Show that `Any` and `All` satisfy a version of De Morgan's Law.
+\begin{code}
+postulate
+  ¬Any≃All¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
+    → (¬_ ∘′ Any P) xs ≃ All (¬_ ∘′ P) xs
+\end{code}
+
+Do we also have the following?
+\begin{code}
+postulate
+  ¬All≃Any¬ : ∀ {A : Set} (P : A → Set) (xs : List A)
+    → (¬_ ∘′ All P) xs ≃ Any (¬_ ∘′ P) xs
+\end{code}
+If so, prove; if not, explain why.
+
+
+#### Exercise `any?`
+
+Just as `All` has analogues `all` and `all?` which determine whether a
+predicate holds for every element of a list, so does `Any` have
+analogues `any` and `any?` which determine whether a predicates holds
+for some element of a list.  Give their definitions.
+
+## Lambda
+
+#### Exercise `mul` (recommended)
+
+Write out the definition of a lambda term that multiplies
+two natural numbers.
+
+
+#### Exercise `primed` (stretch)
+
+We can make examples with lambda terms slighly easier to write
+by adding the following definitions.
+\begin{code}
+ƛ′_⇒_ : Term → Term → Term
+ƛ′ (` x) ⇒ N  =  ƛ x ⇒ N
+ƛ′ _ ⇒ _      =  ⊥-elim impossible
+  where postulate impossible : ⊥
+
+case′_[zero⇒_|suc_⇒_] : Term → Term → Term → Term → Term
+case′ L [zero⇒ M |suc (` x) ⇒ N ]  =  case L [zero⇒ M |suc x ⇒ N ]
+case′ _ [zero⇒ _ |suc _ ⇒ _ ]      =  ⊥-elim impossible
+  where postulate impossible : ⊥
+
+μ′_⇒_ : Term → Term → Term
+μ′ (` x) ⇒ N  =  μ x ⇒ N
+μ′ _ ⇒ _      =  ⊥-elim impossible
+  where postulate impossible : ⊥
+\end{code}
+The definition of `plus` can now be written as follows.
+\begin{code}
+plus′ : Term
+plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
+          case′ m
+            [zero⇒ n
+            |suc m ⇒ `suc (+ · m · n) ]
+  where
+  +  =  ` "+"
+  m  =  ` "m"
+  n  =  ` "n"
+\end{code}
+Write out the definition of multiplication in the same style.
+
+#### Exercise `_[_:=_]′` (stretch)
+
+The definition of substitution above has three clauses (`ƛ`, `case`,
+and `μ`) that invoke a with clause to deal with bound variables.
+Rewrite the definition to factor the common part of these three
+clauses into a single function, defined by mutual recursion with
+substitution.
+
+
+#### Exercise `—↠≃—↠′`
+
+Show that the two notions of reflexive and transitive closure
+above are isomorphic.
+
+
+#### Exercise `plus-example`
+
+Write out the reduction sequence demonstrating that one plus one is two.
+
+
+#### Exercise `mul-type`
+
+Using the term `mul` you defined earlier, write out the derivation
+showing that it is well-typed.
+
+
+## Properties
+
+
+#### Exercise `Progress-iso`
+
+Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M —→ N)`.
+
+
+#### Exercise `progress′`
+
+Write out the proof of `progress′` in full, and compare it to the
+proof of `progress` above.
+
+
+#### Exercise `value?`
+
+Combine `progress` and `—→¬V` to write a program that decides
+whether a well-typed term is a value.
+\begin{code}
+postulate
+  value? : ∀ {A M} → ∅ ⊢ M ⦂ A → Dec (Value M)
+\end{code}
+
+
+#### Exercise `subst′` (stretch)
+
+Rewrite `subst` to work with the modified definition `_[_:=_]′`
+from the exercise in the previous chapter.  As before, this
+should factor dealing with bound variables into a single function,
+defined by mutual recursion with the proof that substitution
+preserves types.
+
+
+#### Exercise `mul-example` (recommended)
+
+Using the evaluator, confirm that two times two is four.
+
+
+#### Exercise: `progress-preservation` (recommended)
+
+Without peeking at their statements above, write down the progress
+and preservation theorems for the simply typed lambda-calculus.
+
+
+#### Exercise `subject_expansion`
+
+We say that `M` _reduces_ to `N` if `M —→ N`,
+and conversely that `M` _expands_ to `N` if `N —→ M`.
+The preservation property is sometimes called _subject reduction_.
+Its opposite is _subject expansion_, which holds if
+`M —→ N` and `∅ ⊢ N ⦂ A` imply `∅ ⊢ M ⦂ A`.
+Find two counter-examples to subject expansion, one
+with case expressions and one not involving case expressions.
+
+
+#### Exercise `stuck` (recommended)
+
+Give an example of an ill-typed term that does get stuck.
+
+
+#### Exercise `unstuck` (recommended)
+
+Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` above.
+
+
+
+
+
+
+
+
diff --git a/tspl/TSPL.lagda b/tspl/TSPL.lagda
index 028b667c..4b2caeb6 100644
--- a/tspl/TSPL.lagda
+++ b/tspl/TSPL.lagda
@@ -99,7 +99,7 @@ For instructions on how to set up Agda for PLFA see [Getting Started](/GettingSt
 
 * [Assignment 1][Assignment1] cw1 due 4pm Thursday 4 October (Week 3)
 * [Assignment 2][Assignment2] cw2 due 4pm Thursday 18 October (Week 5)
-* Assignment 3 cw3 due 4pm Thursday 1 November (Week 7)
+* [Assignment 3][Assignment3] cw3 due 4pm Thursday 1 November (Week 7)
 * Assignment 4 cw4 due 4pm Thursday 15 November (Week 9)
 * Assignment 5 cw5 due 4pm Thursday 22 November (Week 10)