diff --git a/courses/TSPL/2024/Assignment1.lagda.md b/courses/TSPL/2024/Assignment1.lagda.md
index 5c2c75827..2dab11aac 100644
--- a/courses/TSPL/2024/Assignment1.lagda.md
+++ b/courses/TSPL/2024/Assignment1.lagda.md
@@ -37,6 +37,15 @@ any such work on a public repository then you must set access
 permissions appropriately (generally permitting access only to
 yourself). Do not publish solutions to the coursework.
 
+## Deadline and late policy
+
+The deadline and late policy for this assignment are specified on
+Learn in the "Coursework Planner". There are no extensions and
+no ETAs. Coursework is marked best three out of four. Guidance
+on late submissions is at
+
+> [https://web.inf.ed.ac.uk/node/4533](https://web.inf.ed.ac.uk/node/4533)
+
 
 ## Naturals
 
diff --git a/courses/TSPL/2024/Assignment2.lagda.md b/courses/TSPL/2024/Assignment2.lagda.md
new file mode 100644
index 000000000..f40bb062c
--- /dev/null
+++ b/courses/TSPL/2024/Assignment2.lagda.md
@@ -0,0 +1,504 @@
+---
+title     : "Assignment2: TSPL Assignment 2"
+permalink : /TSPL/2024/Assignment2/
+---
+
+```
+module Assignment2 where
+```
+
+## YOUR NAME AND EMAIL GOES HERE
+
+## Introduction
+
+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 labelled "(practice)" are included for those who want extra practice.
+
+Submit your homework using Gradescope. Go to the course page under Learn.
+Select `Assessment`, then select `Assignment Submission`.
+Please ensure your files execute correctly under Agda!
+
+
+## Good Scholarly Practice.
+
+Please remember the University requirement as
+regards all assessed work. Details about this can be found at:
+
+> [https://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct](https://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct)
+
+You are required to take reasonable measures to protect
+your assessed work from unauthorised access. For example, if you put
+any such work on a public repository then you must set access
+permissions appropriately (generally permitting access only to
+yourself). Do not publish solutions to the coursework.
+
+## Deadline and late policy
+
+The deadline and late policy for this assignment are specified on
+Learn in the "Coursework Planner". There are no extensions and
+no ETAs. Coursework is marked best three out of four. Guidance
+on late submissions is at
+
+> [https://web.inf.ed.ac.uk/node/4533](https://web.inf.ed.ac.uk/node/4533)
+
+
+## Connectives
+
+```
+module Connectives where
+```
+
+## Imports
+
+```agda
+  import Relation.Binary.PropositionalEquality as Eq
+  open Eq using (_≡_; refl)
+  open Eq.≡-Reasoning
+  open import Data.Nat using (ℕ)
+  open import Function using (_∘_)
+  open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality; _⇔_)
+  open plfa.part1.Isomorphism.≃-Reasoning
+  open import plfa.part1.Connectives
+    hiding (⊎-weak-×; ⊎×-implies-×⊎)
+```
+
+#### Exercise `⇔≃×` (practice)
+
+Show that `A ⇔ B` as defined [earlier](/Isomorphism/#iff)
+is isomorphic to `(A → B) × (B → A)`.
+
+```agda
+  -- Your code goes here
+```
+
+
+#### Exercise `⊎-comm` (recommended)
+
+Show sum is commutative up to isomorphism.
+
+```agda
+  -- Your code goes here
+```
+
+#### Exercise `⊎-assoc` (practice)
+
+Show sum is associative up to isomorphism.
+
+```agda
+  -- Your code goes here
+```
+
+#### Exercise `⊥-identityˡ` (recommended)
+
+Show empty is the left identity of sums up to isomorphism.
+
+```agda
+  -- Your code goes here
+```
+
+#### Exercise `⊥-identityʳ` (practice)
+
+Show empty is the right identity of sums up to isomorphism.
+
+```agda
+  -- Your code goes here
+```
+
+#### Exercise `⊎-weak-×` (recommended)
+
+Show that the following property holds:
+```agda
+  postulate
+    ⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
+```
+This is called a _weak distributive law_. Give the corresponding
+distributive law, and explain how it relates to the weak version.
+
+```agda
+  -- Your code goes here
+```
+
+
+#### Exercise `⊎×-implies-×⊎` (practice)
+
+Show that a disjunct of conjuncts implies a conjunct of disjuncts:
+```agda
+  postulate
+    ⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
+```
+Does the converse hold? If so, prove; if not, give a counterexample.
+
+```agda
+  -- Your code goes here
+```
+
+
+
+## Negation
+
+```
+module Negation where
+```
+
+## Imports
+
+```agda
+  open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+  open import Data.Nat using (ℕ; zero; suc)
+  open import plfa.part1.Isomorphism using (_≃_; extensionality)
+  open import plfa.part1.Connectives
+  open import plfa.part1.Negation
+    hiding (Stable)
+```
+
+#### Exercise `<-irreflexive` (recommended)
+
+Using negation, show that
+[strict inequality](/Relations/#strict-inequality)
+is irreflexive, that is, `n < n` holds for no `n`.
+
+```agda
+  -- Your code goes here
+```
+
+
+#### Exercise `trichotomy` (practice)
+
+Show that strict inequality satisfies
+[trichotomy](/Relations/#trichotomy),
+that is, for any naturals `m` and `n` exactly one of the following holds:
+
+* `m < n`
+* `m ≡ n`
+* `m > n`
+
+Here "exactly one" means that not only one of the three must hold,
+but that when one holds the negation of the other two must also hold.
+
+```agda
+  -- Your code goes here
+```
+
+#### Exercise `⊎-dual-×` (recommended)
+
+Show that conjunction, disjunction, and negation are related by a
+version of De Morgan's Law.
+
+    ¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
+
+This result is an easy consequence of something we've proved previously.
+
+```agda
+  -- Your code goes here
+```
+
+
+Do we also have the following?
+
+    ¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
+
+If so, prove; if not, can you give a relation weaker than
+isomorphism that relates the two sides?
+
+
+#### Exercise `Classical` (stretch)
+
+Consider the following principles:
+
+  * Excluded Middle: `A ⊎ ¬ A`, for all `A`
+  * Double Negation Elimination: `¬ ¬ A → A`, for all `A`
+  * Peirce's Law: `((A → B) → A) → A`, for all `A` and `B`.
+  * Implication as disjunction: `(A → B) → ¬ A ⊎ B`, for all `A` and `B`.
+  * De Morgan: `¬ (¬ A × ¬ B) → A ⊎ B`, for all `A` and `B`.
+
+Show that each of these implies all the others.
+
+```agda
+  -- Your code goes here
+```
+
+
+#### Exercise `Stable` (stretch)
+
+Say that a formula is _stable_ if double negation elimination holds for it:
+```agda
+  Stable : Set → Set
+  Stable A = ¬ ¬ A → A
+```
+Show that any negated formula is stable, and that the conjunction
+of two stable formulas is stable.
+
+```agda
+  -- Your code goes here
+```
+
+
+## Quantifiers
+
+```
+module Quantifiers where
+```
+
+## Imports
+
+```agda
+  import Relation.Binary.PropositionalEquality as Eq
+  open Eq using (_≡_; refl)
+  open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+  open import Relation.Nullary using (¬_)
+  open import Function using (_∘_)
+  open import plfa.part1.Isomorphism using (_≃_; extensionality; ∀-extensionality)
+  open import plfa.part1.Connectives
+    hiding (Tri)
+  open import plfa.part1.Quantifiers
+    hiding (∀-distrib-×; ⊎∀-implies-∀⊎; ∃-distrib-⊎; ∃×-implies-×∃; ∃¬-implies-¬∀; Tri)
+```
+
+#### Exercise `∀-distrib-×` (recommended)
+
+Show that universals distribute over conjunction:
+```agda
+  postulate
+    ∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
+      (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
+```
+Compare this with the result (`→-distrib-×`) in
+Chapter [Connectives](/Connectives/).
+
+Hint: you will need to use [`∀-extensionality`](/Isomorphism/#extensionality).
+
+#### Exercise `⊎∀-implies-∀⊎` (practice)
+
+Show that a disjunction of universals implies a universal of disjunctions:
+```agda
+  postulate
+    ⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} →
+      (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
+```
+Does the converse hold? If so, prove; if not, explain why.
+
+
+#### Exercise `∀-×` (practice)
+
+Consider the following type.
+```agda
+  data Tri : Set where
+    aa : Tri
+    bb : Tri
+    cc : Tri
+```
+Let `B` be a type indexed by `Tri`, that is `B : Tri → Set`.
+Show that `∀ (x : Tri) → B x` is isomorphic to `B aa × B bb × B cc`.
+
+Hint: you will need to use [`∀-extensionality`](/Isomorphism/#extensionality).
+
+
+#### Exercise `∃-distrib-⊎` (recommended)
+
+Show that existentials distribute over disjunction:
+```agda
+  postulate
+    ∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} →
+      ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
+```
+
+#### Exercise `∃×-implies-×∃` (practice)
+
+Show that an existential of conjunctions implies a conjunction of existentials:
+```agda
+  postulate
+    ∃×-implies-×∃ : ∀ {A : Set} {B C : A → Set} →
+      ∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
+```
+Does the converse hold? If so, prove; if not, explain why.
+
+#### Exercise `∃-⊎` (practice)
+
+Let `Tri` and `B` be as in Exercise `∀-×`.
+Show that `∃[ x ] B x` is isomorphic to `B aa ⊎ B bb ⊎ B cc`.
+
+
+#### Exercise `∃-even-odd` (practice)
+
+How do the proofs become more difficult if we replace `m * 2` and `1 + m * 2`
+by `2 * m` and `2 * m + 1`?  Rewrite the proofs of `∃-even` and `∃-odd` when
+restated in this way.
+
+```agda
+  -- Your code goes here
+```
+
+#### Exercise `∃-+-≤` (practice)
+
+Show that `y ≤ z` holds if and only if there exists a `x` such that
+`x + y ≡ z`.
+
+```agda
+  -- Your code goes here
+```
+
+
+#### Exercise `∃¬-implies-¬∀` (recommended)
+
+Show that existential of a negation implies negation of a universal:
+```agda
+  postulate
+    ∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set}
+      → ∃[ x ] (¬ B x)
+        --------------
+      → ¬ (∀ x → B x)
+```
+Does the converse hold? If so, prove; if not, explain why.
+
+
+#### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism}
+
+Recall that Exercises
+[Bin](/Naturals/#Bin),
+[Bin-laws](/Induction/#Bin-laws), and
+[Bin-predicates](/Relations/#Bin-predicates)
+define a datatype `Bin` of bitstrings representing natural numbers,
+and asks you to define the following functions and predicates:
+
+    to   : ℕ → Bin
+    from : Bin → ℕ
+    Can  : Bin → Set
+
+And to establish the following properties:
+
+    from (to n) ≡ n
+
+    ----------
+    Can (to n)
+
+    Can b
+    ---------------
+    to (from b) ≡ b
+
+Using the above, establish that there is an isomorphism between `ℕ` and
+`∃[ b ] Can b`.
+
+We recommend proving the following lemmas which show that, for a given
+binary number `b`, there is only one proof of `One b` and similarly
+for `Can b`.
+
+    ≡One : ∀ {b : Bin} (o o′ : One b) → o ≡ o′
+
+    ≡Can : ∀ {b : Bin} (cb cb′ : Can b) → cb ≡ cb′
+
+Many of the alternatives for proving `to∘from` turn out to be tricky.
+However, the proof can be straightforward if you use the following lemma,
+which is a corollary of `≡Can`.
+
+    proj₁≡→Can≡ : {cb cb′ : ∃[ b ] Can b} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′
+
+```agda
+  -- Your code goes here
+```
+
+
+
+## Decidable
+
+```
+module Decidable where
+```
+
+## Imports
+
+```agda
+  import Relation.Binary.PropositionalEquality as Eq
+  open Eq using (_≡_; refl)
+  open Eq.≡-Reasoning
+  open import Data.Nat using (ℕ; zero; suc)
+  open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
+  open import Data.Sum using (_⊎_; inj₁; inj₂)
+  open import Relation.Nullary using (¬_)
+  open import Relation.Nullary.Negation using ()
+    renaming (contradiction to ¬¬-intro)
+  open import Data.Unit using (⊤; tt)
+  open import Data.Empty using (⊥; ⊥-elim)
+  open import plfa.part1.Relations using (_<_; z<s; s<s)
+  open import plfa.part1.Isomorphism using (_⇔_)
+  open import plfa.part1.Decidable
+    hiding (_<?_; _≡ℕ?_; ∧-×; ∨-⊎; not-¬; _iff_; _⇔-dec_; iff-⇔)
+```
+
+#### Exercise `_<?_` (recommended)
+
+Analogous to the function above, define a function to decide strict inequality:
+```agda
+  postulate
+    _<?_ : ∀ (m n : ℕ) → Dec (m < n)
+```
+
+```agda
+  -- Your code goes here
+```
+
+#### Exercise `_≡ℕ?_` (practice)
+
+Define a function to decide whether two naturals are equal:
+```agda
+  postulate
+    _≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
+```
+
+```agda
+  -- Your code goes here
+```
+
+
+#### Exercise `erasure` (practice)
+
+Show that erasure relates corresponding boolean and decidable operations:
+```agda
+  postulate
+    ∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
+    ∨-⊎ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
+    not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
+```
+
+#### Exercise `iff-erasure` (recommended)
+
+Give analogues of the `_⇔_` operation from
+Chapter [Isomorphism](/Isomorphism/#iff),
+operation on booleans and decidables, and also show the corresponding erasure:
+```agda
+  postulate
+    _iff_ : Bool → Bool → Bool
+    _⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
+    iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
+```
+
+```agda
+  -- Your code goes here
+```
+
+#### Exercise `False` (practice)
+
+Give analogues of `True`, `toWitness`, and `fromWitness` which work
+with *negated* properties. Call these `False`, `toWitnessFalse`, and
+`fromWitnessFalse`.
+
+
+#### Exercise `Bin-decidable` (stretch)
+
+Recall that Exercises
+[Bin](/Naturals/#Bin),
+[Bin-laws](/Induction/#Bin-laws), and
+[Bin-predicates](/Relations/#Bin-predicates)
+define a datatype `Bin` of bitstrings representing natural numbers,
+and asks you to define the following predicates:
+
+    One  : Bin → Set
+    Can  : Bin → Set
+
+Show that both of the above are decidable.
+
+    One? : ∀ (b : Bin) → Dec (One b)
+    Can? : ∀ (b : Bin) → Dec (Can b)
diff --git a/courses/TSPL/2024/tspl.md b/courses/TSPL/2024/tspl.md
index 55d2a99c0..e6e26faf9 100644
--- a/courses/TSPL/2024/tspl.md
+++ b/courses/TSPL/2024/tspl.md
@@ -103,7 +103,7 @@ Lectures on Tuesday and Thursday are immediately followed by a tutorial.
 Assessment for the course is as follows.
 
 * four courseworks, marked best three out of four, **80%**
-* project, take a research paper and formalise its development, **20%**
+* essay, take a research paper and formalise its development, **20%**
 
 Because there is no final, we need to be able to check that students
 can explain their work during tutorials.  For this reason, _you can
@@ -112,9 +112,9 @@ the four tutorial sessions in the week before it is due_.
 
 In order to conform with the University's Common Marking Scheme,
 students may typically get only 10 points or less (out of 20) on the
-project.  _Attempting the project may not be a good use of time
+essay.  _Attempting the essay may not be a good use of time
 compared to other courses where there are easier marks to be had._
-Not all students are expected to attempt the project.
+Not all students are expected to attempt the essay.
 
 
 ## Coursework
@@ -122,7 +122,7 @@ Not all students are expected to attempt the project.
 For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/).
 
 * [Assignment 1](/TSPL/2024/Assignment1/) cw1 due 12 noon Friday 18 October (Week 5)
-* Assignment 2 cw2 due 12 noon Friday 1 November (Week 7)
+* [Assignment 2](/TSPL/2024/Assignment2/) cw2 due 12 noon Friday 1 November (Week 7)
 * Assignment 3 cw3 due 12 noon Friday 15 November (Week 9)
 * Assignment 4 cw4 due 12 noon Friday 29 November (Week 11)
 * Essay cw5 due 12 noon Thursday 23 January 2025 (Week 2, Semester 2)
@@ -155,12 +155,12 @@ submit tspl cwN AssignmentN.lagda.md
 where N is the number of the assignment. -->
 
 
-## Project
+## Essay
 
-The optional project is to take a research paper and formalise all or
-part of it in Agda.  In the past, some students have submitted superb optional
-projects that contributed to ongoing research.
-Talk to me about what you would like to submit.
+The essay is to take a research paper and formalise all or
+part of it in Agda.  In the past, some students have submitted superb
+essays that contributed to ongoing research.
+Talk to Prof Wadler about what you would like to submit.
 
 <!--
 ## Mock exam