diff --git a/Makefile b/Makefile
index cce8e012..d9c99a35 100644
--- a/Makefile
+++ b/Makefile
@@ -1,6 +1,6 @@
-agda := $(shell find src -type f -name '*.lagda')
-agdai := $(shell find src -type f -name '*.agdai')
-markdown := $(subst src/,out/,$(subst .lagda,.md,$(agda)))
+agda := $(shell find src tspl -type f -name '*.lagda')
+agdai := $(shell find src tspl -type f -name '*.agdai')
+markdown := $(subst tspl/,out/,$(subst src/,out/,$(subst .lagda,.md,$(agda))))
 PLFA_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
 AGDA2HTML_FLAGS := --verbose --link-to-local-agda-names --use-jekyll=out/
 
@@ -21,6 +21,12 @@ out/%.md: src/%.lagda | out/
 		| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
 	@sed -i '1 s|---|---\nsrc       : $(<)|' $@
 
+# should fix this -- it's the same as above
+out/%.md: tspl/%.lagda | out/
+	agda2html $(AGDA2HTML_FLAGS) -i $< -o $@ 2>&1 \
+		| sed '/^Generating.*/d; /^Warning\: HTML.*/d; /^reached from the.*/d; /^\s*$$/d'
+	@sed -i '1 s|---|---\nsrc       : $(<)|' $@
+
 serve:
 	ruby -S bundle exec jekyll serve --incremental
 
diff --git a/tspl/Assignment1.lagda b/tspl/Assignment1.lagda
new file mode 100644
index 00000000..674e0092
--- /dev/null
+++ b/tspl/Assignment1.lagda
@@ -0,0 +1,319 @@
+---
+title     : "Assignment1: TSPL Assignment 1"
+layout    : page
+permalink : /Assignment1/
+---
+
+\begin{code}
+module Assignment1 where
+\end{code}
+
+## YOUR NAME AND EMAIL GOES HERE
+
+## Introduction
+
+This assignment is due **4pm Thursday 4 October** (Week 3).
+
+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.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
+open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
+  ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
+open import plfa.Relations using (_<_; z<s; s<s; zero; suc; even; odd)
+\end{code}
+
+## Naturals
+
+#### Exercise `seven` {#seven}
+
+Write out `7` in longhand.
+
+
+#### Exercise `+-example` {#plus-example}
+
+Compute `3 + 4`, writing out your reasoning as a chain of equations.
+
+
+#### Exercise `*-example` {#times-example}
+
+Compute `3 * 4`, writing out your reasoning as a chain of equations.
+
+
+#### Exercise `_^_` (recommended) {#power}
+
+Define exponentiation, which is given by the following equations.
+
+    n ^ 0        =  1
+    n ^ (1 + m)  =  n * (n ^ m)
+
+Check that `3 ^ 4` is `81`.
+
+
+#### Exercise `∸-examples` (recommended) {#monus-examples}
+
+Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations.
+
+
+#### Exercise `Bin` (stretch) {#Bin}
+
+A more efficient representation of natural numbers uses a binary
+rather than a unary system.  We represent a number as a bitstring.
+\begin{code}
+data Bin : Set where
+  nil : Bin
+  x0_ : Bin → Bin
+  x1_ : Bin → Bin
+\end{code}
+For instance, the bitstring
+
+    1011
+
+standing for the number eleven is encoded, right to left, as
+
+    x1 x1 x0 x1 nil
+
+Representations are not unique due to leading zeros.
+Hence, eleven is also represented by `001011`, encoded as
+
+    x1 x1 x0 x1 x0 x0 nil
+
+Define a function
+
+    inc : Bin → Bin
+
+that converts a bitstring to the bitstring for the next higher
+number.  For example, since `1100` encodes twelve, we should have
+
+    inc (x1 x1 x0 x1 nil) ≡ x0 x0 x1 x1 nil
+
+Confirm that this gives the correct answer for the bitstrings
+encoding zero through four.
+
+Using the above, define a pair of functions to convert
+between the two representations.
+
+    to   : ℕ → Bin
+    from : Bin → ℕ
+
+For the former, choose the bitstring to have no leading zeros if it
+represents a positive natural, and represent zero by `x0 nil`.
+Confirm that these both give the correct answer for zero through four.
+
+## Induction
+
+#### Exercise `operators` {#operators}
+
+Give another example of a pair of operators that have an identity
+and are associative, commutative, and distribute over one another.
+
+Give an example of an operator that has an identity and is
+associative but is not commutative.
+
+
+#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
+
+Write out what is known about associativity of addition on each of the first four
+days using a finite story of creation, as
+[earlier][plfa.Naturals#finite-creation]
+
+
+#### Exercise `+-swap` (recommended) {#plus-swap} 
+
+Show
+
+    m + (n + p) ≡ n + (m + p)
+
+for all naturals `m`, `n`, and `p`. No induction is needed,
+just apply the previous results which show addition
+is associative and commutative.  You may need to use
+the following function from the standard library:
+
+    sym : ∀ {m n : ℕ} → m ≡ n → n ≡ m
+
+\begin{code}
+swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+swap m n p rewrite sym (+-assoc m n p) | +-comm m n | +-assoc n m p = {!!}
+\end{code}
+
+#### Exercise `*-distrib-+` (recommended) {#times-distrib-plus}
+
+Show multiplication distributes over addition, that is,
+
+    (m + n) * p ≡ m * p + n * p
+
+for all naturals `m`, `n`, and `p`.
+
+#### Exercise `*-assoc` (recommended) {#times-assoc}
+
+Show multiplication is associative, that is,
+
+    (m * n) * p ≡ m * (n * p)
+
+for all naturals `m`, `n`, and `p`.
+
+#### Exercise `*-comm` {#times-comm}
+
+Show multiplication is commutative, that is,
+
+    m * n ≡ n * m
+
+for all naturals `m` and `n`.  As with commutativity of addition,
+you will need to formulate and prove suitable lemmas.
+
+#### Exercise `0∸n≡0` {#zero-monus}
+
+Show
+
+    zero ∸ n ≡ zero
+
+for all naturals `n`. Did your proof require induction?
+
+#### Exercise `∸-+-assoc` {#monus-plus-assoc}
+
+Show that monus associates with addition, that is,
+
+    m ∸ n ∸ p ≡ m ∸ (n + p)
+
+for all naturals `m`, `n`, and `p`.
+
+#### Exercise `Bin-laws` (stretch) {#Bin-laws}
+
+Recall that 
+Exercise [Bin][plfa.Naturals#Bin]
+defines a datatype `Bin` of bitstrings representing natural numbers
+and asks you to define functions
+
+    inc   : Bin → Bin
+    to    : ℕ → Bin
+    from  : Bin → ℕ
+
+Consider the following laws, where `n` ranges over naturals and `x`
+over bitstrings.
+
+    from (inc x) ≡ suc (from x)
+    to (from n) ≡ n
+    from (to x) ≡ x
+
+For each law: if it holds, prove; if not, give a counterexample.
+
+
+## Relations
+
+
+#### Exercise `orderings` {#orderings}
+
+Give an example of a preorder that is not a partial order.
+
+Give an example of a partial order that is not a preorder.
+
+
+#### Exercise `≤-antisym-cases` {#leq-antisym-cases} 
+
+The above proof omits cases where one argument is `z≤n` and one
+argument is `s≤s`.  Why is it ok to omit them?
+
+
+#### Exercise `*-mono-≤` (stretch)
+
+Show that multiplication is monotonic with regard to inequality.
+
+
+#### Exercise `<-trans` (recommended) {#less-trans}
+
+Show that strict inequality is transitive.
+
+#### Exercise `trichotomy` {#trichotomy}
+
+Show that strict inequality satisfies a weak version of trichotomy, in
+the sense that for any `m` and `n` that one of the following holds:
+  * `m < n`,
+  * `m ≡ n`, or
+  * `m > n`
+Define `m > n` to be the same as `n < m`.
+You will need a suitable data declaration,
+similar to that used for totality.
+(We will show that the three cases are exclusive after we introduce
+[negation][plfa.Negation].)
+
+#### Exercise `+-mono-<` {#plus-mono-less}
+
+Show that addition is monotonic with respect to strict inequality.
+As with inequality, some additional definitions may be required.
+
+#### Exercise `≤-iff-<` (recommended) {#leq-iff-less}
+
+Show that `suc m ≤ n` implies `m < n`, and conversely.
+
+#### Exercise `<-trans-revisited` {#less-trans-revisited}
+
+Give an alternative proof that strict inequality is transitive,
+using the relating between strict inequality and inequality and
+the fact that inequality is transitive.
+
+#### Exercise `o+o≡e` (stretch) {#odd-plus-odd}
+
+Show that the sum of two odd numbers is even.
+
+#### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
+
+Recall that 
+Exercise [Bin][plfa.Naturals#Bin]
+defines a datatype `Bin` of bitstrings representing natural numbers.
+Representations are not unique due to leading zeros.
+Hence, eleven may be represented by both of the following
+
+    x1 x1 x0 x1 nil
+    x1 x1 x0 x1 x0 x0 nil
+
+Define a predicate
+
+    Can : Bin → Set
+
+over all bitstrings that holds if the bitstring is canonical, meaning
+it has no leading zeros; the first representation of eleven above is
+canonical, and the second is not.  To define it, you will need an
+auxiliary predicate
+
+    One : Bin → Set
+
+that holds only if the bistring has a leading one.  A bitstring is
+canonical if it has a leading one (representing a positive number) or
+if it consists of a single zero (representing zero).
+
+Show that increment preserves canonical bitstrings.
+
+    Can x
+    ------------
+    Can (inc x)
+
+Show that converting a natural to a bitstring always yields a
+canonical bitstring.
+
+    ----------
+    Can (to n)
+
+Show that converting a canonical bitstring to a natural
+and back is the identity.
+
+    Can x
+    ---------------
+    to (from x) ≡ x
+
+\end{code}
+(Hint: For each of these, you may first need to prove related
+properties of `One`.)
diff --git a/tspl/Assignment2.lagda b/tspl/Assignment2.lagda
new file mode 100644
index 00000000..5329e017
--- /dev/null
+++ b/tspl/Assignment2.lagda
@@ -0,0 +1,365 @@
+---
+title     : "Assignment2: TSPL Assignment 2"
+layout    : page
+permalink : /Assignment2/
+---
+
+\begin{code}
+module Assignment2 where
+\end{code}
+
+## YOUR NAME AND EMAIL GOES HERE
+
+## Introduction
+
+This assignment is due **4pm Thursday 18 October** (Week 5).
+
+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.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
+open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
+  ≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
+open import plfa.Relations using (_<_; z<s; s<s)
+open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+open import Data.Unit using (⊤; tt)
+open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness)
+open import Relation.Nullary.Negation using (¬?)
+open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Sum using (_⊎-dec_)
+open import Relation.Nullary.Negation using (contraposition)
+open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
+open import plfa.Relations using (_<_; z<s; s<s)
+open import plfa.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
+open plfa.Isomorphism.≃-Reasoning
+\end{code}
+
+## Equality
+
+#### Exercise `≤-reasoning` (stretch)
+
+The proof of monotonicity from
+Chapter [Relations][plfa.Relations]
+can be written in a more readable form by using an anologue of our
+notation for `≡-reasoning`.  Define `≤-reasoning` analogously, and use
+it to write out an alternative proof that addition is monotonic with
+regard to inequality.  Rewrite both `+-monoˡ-≤` and `+-mono-≤`.
+
+
+
+## Isomorphism
+
+#### Exercise `≃-implies-≲`
+
+Show that every isomorphism implies an embedding.
+\begin{code}
+postulate
+  ≃-implies-≲ : ∀ {A B : Set}
+    → A ≃ B
+      -----
+    → A ≲ B  
+\end{code}
+
+#### Exercise `_⇔_` (recommended) {#iff}
+
+Define equivalence of propositions (also known as "if and only if") as follows.
+\begin{code}
+record _⇔_ (A B : Set) : Set where
+  field
+    to   : A → B
+    from : B → A
+
+open _⇔_
+\end{code}
+Show that equivalence is reflexive, symmetric, and transitive.
+
+#### Exercise `Bin-embedding` (stretch) {#Bin-embedding}
+
+Recall that Exercises
+[Bin][plfa.Naturals#Bin] and
+[Bin-laws][plfa.Induction#Bin-laws]
+define a datatype of bitstrings representing natural numbers.
+\begin{code}
+data Bin : Set where
+  nil : Bin
+  x0_ : Bin → Bin
+  x1_ : Bin → Bin
+\end{code}
+And ask you to define the following functions:
+
+    to : ℕ → Bin
+    from : Bin → ℕ
+
+which satisfy the following property:
+
+    from (to n) ≡ n
+
+Using the above, establish that there is an embedding of `ℕ` into `Bin`.
+Why is there not an isomorphism?
+
+
+## Connectives
+
+#### Exercise `⇔≃×` (recommended)
+
+Show that `A ⇔ B` as defined [earlier][plfa.Isomorphism#iff]
+is isomorphic to `(A → B) × (B → A)`.
+
+#### Exercise `⊎-comm` (recommended)
+
+Show sum is commutative up to isomorphism.
+
+#### Exercise `⊎-assoc`
+
+Show sum is associative up to ismorphism. 
+
+#### Exercise `⊥-identityˡ` (recommended)
+
+Show zero is the left identity of addition.
+
+#### Exercise `⊥-identityʳ`
+
+Show zero is the right identity of addition. 
+
+#### Exercise `⊎-weak-×` (recommended)
+
+Show that the following property holds.
+\begin{code}
+postulate
+  ⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
+\end{code}
+This is called a _weak distributive law_. Give the corresponding
+distributive law, and explain how it relates to the weak version.
+
+#### Exercise `⊎×-implies-×⊎`
+
+Show that a disjunct of conjuncts implies a conjunct of disjuncts.
+\begin{code}
+postulate
+  ⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
+\end{code}
+Does the converse hold? If so, prove; if not, give a counterexample.
+
+
+## Negation
+
+#### Exercise `<-irreflexive` (recommended)
+
+Using negation, show that
+[strict inequality][plfa.Relations#strict-inequality]
+is irreflexive, that is, `n < n` holds for no `n`.
+
+
+#### Exercise `trichotomy`
+
+Show that strict inequality satisfies
+[trichotomy][plfa.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 one of the three must hold, and each implies the
+negation of the other two.
+
+
+#### 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.
+
+Do we also have the following?
+
+    ¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
+
+If so, prove; if not, give a variant that does hold.
+
+
+#### 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.
+
+
+#### Exercise `Stable` (stretch)
+
+Say that a formula is _stable_ if double negation elimination holds for it.
+\begin{code}
+Stable : Set → Set
+Stable A = ¬ ¬ A → A
+\end{code}
+Show that any negated formula is stable, and that the conjunction
+of two stable formulas is stable.
+
+
+## Quantifiers
+
+#### Exercise `∀-distrib-×` (recommended)
+
+Show that universals distribute over conjunction.
+\begin{code}
+postulate
+  ∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
+    (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
+\end{code}
+Compare this with the result (`→-distrib-×`) in
+Chapter [Connectives][plfa.Connectives].
+
+#### Exercise `⊎∀-implies-∀⊎`
+
+Show that a disjunction of universals implies a universal of disjunctions.
+\begin{code}
+postulate
+  ⊎∀-implies-∀⊎ : ∀ {A : Set} { B C : A → Set } →
+    (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x)  →  ∀ (x : A) → B x ⊎ C x
+\end{code}
+Does the converse hold? If so, prove; if not, explain why.
+
+#### Exercise `∃-distrib-⊎` (recommended)
+
+Show that existentials distribute over disjunction.
+\begin{code}
+postulate
+  ∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} →
+    ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
+\end{code}
+
+#### Exercise `∃×-implies-×∃`
+
+Show that an existential of conjunctions implies a conjunction of existentials.
+\begin{code}
+postulate
+  ∃×-implies-×∃ : ∀ {A : Set} { B C : A → Set } →
+    ∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
+\end{code}
+Does the converse hold? If so, prove; if not, explain why.
+
+#### Exercise `∃-even-odd`
+
+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.
+
+#### Exercise `∃-+-≤`
+
+Show that `y ≤ z` holds if and only if there exists a `x` such that
+`x + y ≡ z`.
+
+#### Exercise `∃¬-implies-¬∀` (recommended)
+
+Show that existential of a negation implies negation of a universal.
+\begin{code}
+postulate
+  ∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set}
+    → ∃[ x ] (¬ B x)
+      --------------
+    → ¬ (∀ x → B x)
+\end{code}
+Does the converse hold? If so, prove; if not, explain why.
+
+
+#### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism}
+
+Recall that Exercises
+[Bin][plfa.Naturals#Bin],
+[Bin-laws][plfa.Induction#Bin-laws], and
+[Bin-predicates][plfa.Relations#Bin-predicates]
+define a datatype of bitstrings representing natural numbers.
+
+    data Bin : Set where
+      nil : Bin
+      x0_ : Bin → Bin
+      x1_ : Bin → Bin
+
+And ask 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 x
+    ---------------
+    to (from x) ≡ x
+
+Using the above, establish that there is an isomorphism between `ℕ` and
+`∃[ x ](Can x)`.
+
+
+## Decidable
+
+#### Exercise `_<?_` (recommended)
+
+Analogous to the function above, define a function to decide strict inequality.
+\begin{code}
+postulate
+  _<?_ : ∀ (m n : ℕ) → Dec (m < n)
+\end{code}
+
+#### Exercise `_≡ℕ?_`
+
+Define a function to decide whether two naturals are equal.
+\begin{code}
+postulate
+  _≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
+\end{code}
+
+
+#### Exercise `erasure`
+
+Show that erasure relates corresponding boolean and decidable operations.
+\begin{code}
+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 ⌋
+\end{code}
+  
+#### Exercise `iff-erasure` (recommended)
+
+Give analogues of the `_⇔_` operation from 
+Chapter [Isomorphism][plfa.Isomorphism#iff],
+operation on booleans and decidables, and also show the corresponding erasure.
+\begin{code}
+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 ⌋  
+\end{code}
+
diff --git a/tspl/Assignment3.lagda b/tspl/Assignment3.lagda
new file mode 100644
index 00000000..a26b2149
--- /dev/null
+++ b/tspl/Assignment3.lagda
@@ -0,0 +1,382 @@
+---
+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 (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Function using (_∘_)
+open import Algebra.Structures using (IsMonoid)
+open import Level using (Level)
+open import Relation.Unary using (Decidable)
+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; All; Any; here; there; _∈_)
+open import plfa.Lambda hiding (ƛ′_⇒_; case′_[zero⇒_|suc_⇒_]; μ′_⇒_; plus′)
+open import plfa.Properties hiding (value?; unstuck; preserves; wttdgs)
+\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-++-≃` (stretch)
+
+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?` (stretch)
+
+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.
+
+
+#### Exercise `filter?` (stretch)
+
+Define the following variant of the traditional `filter` function on lists,
+which given a list and a decidable predicate returns all elements of the
+list satisfying the predicate.
+\begin{code}
+postulate
+  filter? : ∀ {A : Set} {P : A → Set}
+    → (P? : Decidable P) → List A → ∃[ ys ]( All P ys )
+\end{code}
+
+
+## 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` (recommended)
+
+Using the term `mul` you defined earlier, write out the derivation
+showing that it is well-typed.
+
+
+## Properties
+
+
+#### Exercise `Progress-≃`
+
+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`
+
+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`
+
+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/Assignment4.lagda b/tspl/Assignment4.lagda
new file mode 100644
index 00000000..8321b539
--- /dev/null
+++ b/tspl/Assignment4.lagda
@@ -0,0 +1,1169 @@
+---
+title     : "Assignment4: TSPL Assignment 4"
+layout    : page
+permalink : /Assignment4/
+---
+
+\begin{code}
+module Assignment4 where
+\end{code}
+
+## YOUR NAME AND EMAIL GOES HERE
+
+
+## Introduction
+
+This assignment is due **4pm Thursday 15 November** (Week 9).
+
+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!
+
+_IMPORTANT_ For ease of marking, when modifying the given code please write
+
+  -- begin
+  -- end
+
+before and after code you add, to indicate your changes.
+
+
+## Imports
+
+\begin{code}
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
+open import Data.String using (String)
+open import Data.String.Unsafe using (_≟_)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+\end{code}
+
+
+## DeBruijn
+
+
+\begin{code}
+module DeBruijn where
+\end{code}
+
+Remember to indent all code by two spaces.
+
+\begin{code}
+  open import plfa.DeBruijn
+\end{code}
+
+
+#### Exercise (`mul`) (recommended)
+
+Write out the definition of a lambda term that multiplies
+two natural numbers, now adapted to the inherently typed
+DeBruijn represenation.
+
+
+#### Exercise `V¬—→`
+
+Following the previous development, show values do
+not reduce, and its corollary, terms that reduce are not
+values.
+
+
+#### Exercise `mul-example` (recommended)
+
+Using the evaluator, confirm that two times two is four.
+
+
+## More
+
+\begin{code}
+module More where
+\end{code}
+
+Remember to indent all code by two spaces.
+
+
+### Syntax
+
+\begin{code}
+  infix  4 _⊢_
+  infix  4 _∋_
+  infixl 5 _,_
+
+  infixr 7 _⇒_
+  infixr 8 _`⊎_
+  infixr 9 _`×_
+
+  infix  5 ƛ_
+  infix  5 μ_
+  infixl 7 _·_
+  infixl 8 _`*_
+  infix  8 `suc_
+  infix  9 `_
+  infix  9 S_
+  infix  9 #_
+\end{code}
+
+### Types
+
+\begin{code}
+  data Type : Set where
+    `ℕ    : Type
+    _⇒_   : Type → Type → Type
+    Nat   : Type
+    _`×_  : Type → Type → Type
+    _`⊎_  : Type → Type → Type
+    `⊤    : Type
+    `⊥    : Type
+    `List : Type → Type
+\end{code}
+
+### Contexts
+
+\begin{code}
+  data Context : Set where
+    ∅   : Context
+    _,_ : Context → Type → Context
+\end{code}
+
+### Variables and the lookup judgment
+
+\begin{code}
+  data _∋_ : Context → Type → Set where
+
+    Z : ∀ {Γ A}
+        ---------
+      → Γ , A ∋ A
+
+    S_ : ∀ {Γ A B}
+      → Γ ∋ B
+        ---------
+      → Γ , A ∋ B
+\end{code}   
+
+### Terms and the typing judgment
+
+\begin{code}
+  data _⊢_ : Context → Type → Set where
+
+    -- variables
+
+    `_ : ∀ {Γ A}
+      → Γ ∋ A
+        -----
+      → Γ ⊢ A
+
+    -- functions
+
+    ƛ_  :  ∀ {Γ A B}
+      → Γ , A ⊢ B
+        ---------
+      → Γ ⊢ A ⇒ B
+
+    _·_ : ∀ {Γ A B}
+      → Γ ⊢ A ⇒ B
+      → Γ ⊢ A
+        ---------
+      → Γ ⊢ B
+
+    -- naturals
+
+    `zero : ∀ {Γ}
+        ------
+      → Γ ⊢ `ℕ
+
+    `suc_ : ∀ {Γ}
+      → Γ ⊢ `ℕ
+        ------
+      → Γ ⊢ `ℕ
+
+    case : ∀ {Γ A}
+      → Γ ⊢ `ℕ
+      → Γ ⊢ A
+      → Γ , `ℕ ⊢ A
+        -----
+      → Γ ⊢ A
+
+    -- fixpoint
+
+    μ_ : ∀ {Γ A}
+      → Γ , A ⊢ A
+        ----------
+      → Γ ⊢ A
+
+    -- primitive numbers
+
+    con : ∀ {Γ}
+      → ℕ
+        -------
+      → Γ ⊢ Nat
+
+    _`*_ : ∀ {Γ}
+      → Γ ⊢ Nat
+      → Γ ⊢ Nat
+        -------
+      → Γ ⊢ Nat
+
+    -- let
+
+    `let : ∀ {Γ A B}
+      → Γ ⊢ A
+      → Γ , A ⊢ B
+        ----------
+      → Γ ⊢ B
+
+    -- products
+
+    `⟨_,_⟩ : ∀ {Γ A B}
+      → Γ ⊢ A
+      → Γ ⊢ B
+        -----------
+      → Γ ⊢ A `× B
+
+    `proj₁ : ∀ {Γ A B}
+      → Γ ⊢ A `× B
+        -----------
+      → Γ ⊢ A
+
+    `proj₂ : ∀ {Γ A B}
+      → Γ ⊢ A `× B
+        -----------
+      → Γ ⊢ B
+
+    -- alternative formulation of products
+
+    case× : ∀ {Γ A B C}
+      → Γ ⊢ A `× B
+      → Γ , A , B ⊢ C
+        --------------
+      → Γ ⊢ C
+
+\end{code}
+
+### Abbreviating de Bruijn indices
+
+\begin{code}
+  lookup : Context → ℕ → Type
+  lookup (Γ , A) zero     =  A
+  lookup (Γ , _) (suc n)  =  lookup Γ n
+  lookup ∅       _        =  ⊥-elim impossible
+    where postulate impossible : ⊥
+
+  count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n
+  count {Γ , _} zero     =  Z
+  count {Γ , _} (suc n)  =  S (count n)
+  count {∅}     _        =  ⊥-elim impossible
+    where postulate impossible : ⊥
+
+  #_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n
+  # n  =  ` count n
+\end{code}
+
+## Renaming
+
+\begin{code}
+  ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B)
+  ext ρ Z      =  Z
+  ext ρ (S x)  =  S (ρ x)
+
+  rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+  rename ρ (` x)          =  ` (ρ x)
+  rename ρ (ƛ N)          =  ƛ (rename (ext ρ) N)
+  rename ρ (L · M)        =  (rename ρ L) · (rename ρ M)
+  rename ρ (`zero)        =  `zero
+  rename ρ (`suc M)       =  `suc (rename ρ M)
+  rename ρ (case L M N)   =  case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
+  rename ρ (μ N)          =  μ (rename (ext ρ) N)
+  rename ρ (con n)        =  con n
+  rename ρ (M `* N)       =  rename ρ M `* rename ρ N
+  rename ρ (`let M N)     =  `let (rename ρ M) (rename (ext ρ) N)
+  rename ρ `⟨ M , N ⟩     =  `⟨ rename ρ M , rename ρ N ⟩
+  rename ρ (`proj₁ L)     =  `proj₁ (rename ρ L)
+  rename ρ (`proj₂ L)     =  `proj₂ (rename ρ L)
+  rename ρ (case× L M)    =  case× (rename ρ L) (rename (ext (ext ρ)) M)
+\end{code}
+
+## Simultaneous Substitution
+
+\begin{code}
+  exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B)
+  exts σ Z      =  ` Z
+  exts σ (S x)  =  rename S_ (σ x)
+
+  subst : ∀ {Γ Δ} → (∀ {C} → Γ ∋ C → Δ ⊢ C) → (∀ {C} → Γ ⊢ C → Δ ⊢ C)
+  subst σ (` k)          =  σ k
+  subst σ (ƛ N)          =  ƛ (subst (exts σ) N)
+  subst σ (L · M)        =  (subst σ L) · (subst σ M)
+  subst σ (`zero)        =  `zero
+  subst σ (`suc M)       =  `suc (subst σ M)
+  subst σ (case L M N)   =  case (subst σ L) (subst σ M) (subst (exts σ) N)
+  subst σ (μ N)          =  μ (subst (exts σ) N)
+  subst σ (con n)        =  con n
+  subst σ (M `* N)       =  subst σ M `* subst σ N
+  subst σ (`let M N)     =  `let (subst σ M) (subst (exts σ) N)
+  subst σ `⟨ M , N ⟩     =  `⟨ subst σ M , subst σ N ⟩
+  subst σ (`proj₁ L)     =  `proj₁ (subst σ L)
+  subst σ (`proj₂ L)     =  `proj₂ (subst σ L)
+  subst σ (case× L M)    =  case× (subst σ L) (subst (exts (exts σ)) M)
+\end{code}
+
+## Single and double substitution
+
+\begin{code}
+  _[_] : ∀ {Γ A B}
+    → Γ , A ⊢ B
+    → Γ ⊢ A
+    ------------
+    → Γ ⊢ B
+  _[_] {Γ} {A} N V =  subst {Γ , A} {Γ} σ N
+    where
+    σ : ∀ {B} → Γ , A ∋ B → Γ ⊢ B
+    σ Z      =  V
+    σ (S x)  =  ` x
+
+  _[_][_] : ∀ {Γ A B C}
+    → Γ , A , B ⊢ C
+    → Γ ⊢ A
+    → Γ ⊢ B
+      ---------------
+    → Γ ⊢ C
+  _[_][_] {Γ} {A} {B} N V W =  subst {Γ , A , B} {Γ} σ N
+    where
+    σ : ∀ {C} → Γ , A , B ∋ C → Γ ⊢ C
+    σ Z          =  W
+    σ (S Z)      =  V
+    σ (S (S x))  =  ` x
+\end{code}
+
+## Values
+
+\begin{code}
+  data Value : ∀ {Γ A} → Γ ⊢ A → Set where
+
+    -- functions
+
+    V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
+        ---------------------------
+      → Value (ƛ N)
+
+    -- naturals
+
+    V-zero : ∀ {Γ} →
+        -----------------
+        Value (`zero {Γ})
+
+    V-suc_ : ∀ {Γ} {V : Γ ⊢ `ℕ}
+      → Value V
+        --------------
+      → Value (`suc V)
+
+    -- primitives
+
+    V-con : ∀ {Γ n}
+        ---------------------
+      → Value {Γ = Γ} (con n)
+
+    -- products
+
+    V-⟨_,_⟩ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
+      → Value V
+      → Value W
+        ----------------
+      → Value `⟨ V , W ⟩
+\end{code}
+
+Implicit arguments need to be supplied when they are
+not fixed by the given arguments.
+
+## Reduction
+
+\begin{code}
+  infix 2 _—→_
+
+  data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+    -- functions
+
+    ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
+      → L —→ L′
+        ---------------
+      → L · M —→ L′ · M
+
+    ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
+      → Value V
+      → M —→ M′
+        ---------------
+      → V · M —→ V · M′
+
+    β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {V : Γ ⊢ A}
+      → Value V
+        --------------------
+      → (ƛ N) · V —→ N [ V ]
+
+    -- naturals
+
+    ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
+      → M —→ M′
+        -----------------
+      → `suc M —→ `suc M′
+
+    ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+      → L —→ L′
+        -------------------------
+      → case L M N —→ case L′ M N
+
+    β-zero :  ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+        -------------------
+      → case `zero M N —→ M
+
+    β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+      → Value V
+        ----------------------------
+      → case (`suc V) M N —→ N [ V ]
+
+    -- fixpoint
+
+    β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
+        ----------------
+      → μ N —→ N [ μ N ]
+
+    -- primitive numbers
+
+    ξ-*₁ : ∀ {Γ} {L L′ M : Γ ⊢ Nat}
+      → L —→ L′
+        -----------------
+      → L `* M —→ L′ `* M
+
+    ξ-*₂ : ∀ {Γ} {V M M′ : Γ ⊢ Nat}
+      → Value V
+      → M —→ M′
+        -----------------
+      → V `* M —→ V `* M′
+
+    δ-* : ∀ {Γ c d}
+        -------------------------------------
+      → con {Γ = Γ} c `* con d —→ con (c * d)
+
+    -- let
+
+    ξ-let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ , A ⊢ B}
+      → M —→ M′
+        ---------------------
+      → `let M N —→ `let M′ N
+
+    β-let : ∀ {Γ A B} {V : Γ ⊢ A} {N : Γ , A ⊢ B}
+      → Value V
+        -------------------
+      → `let V N —→ N [ V ]
+
+    -- products
+
+    ξ-⟨,⟩₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ ⊢ B}
+      → M —→ M′
+        -------------------------
+      → `⟨ M , N ⟩ —→ `⟨ M′ , N ⟩
+
+    ξ-⟨,⟩₂ : ∀ {Γ A B} {V : Γ ⊢ A} {N N′ : Γ ⊢ B}
+      → Value V
+      → N —→ N′
+        -------------------------
+      → `⟨ V , N ⟩ —→ `⟨ V , N′ ⟩
+
+    ξ-proj₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
+      → L —→ L′
+        ---------------------
+      → `proj₁ L —→ `proj₁ L′
+
+    ξ-proj₂ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
+      → L —→ L′
+        ---------------------
+      → `proj₂ L —→ `proj₂ L′
+
+    β-proj₁ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
+      → Value V
+      → Value W
+        ----------------------
+      → `proj₁ `⟨ V , W ⟩ —→ V
+
+    β-proj₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
+      → Value V
+      → Value W
+        ----------------------
+      → `proj₂ `⟨ V , W ⟩ —→ W
+
+    -- alternative formulation of products
+
+    ξ-case× : ∀ {Γ A B C} {L L′ : Γ ⊢ A `× B} {M : Γ , A , B ⊢ C}
+      → L —→ L′
+        -----------------------
+      → case× L M —→ case× L′ M
+
+    β-case× : ∀ {Γ A B C} {V : Γ ⊢ A} {W : Γ ⊢ B} {M : Γ , A , B ⊢ C}
+      → Value V
+      → Value W
+        ----------------------------------
+      → case× `⟨ V , W ⟩ M —→ M [ V ][ W ]
+\end{code}
+
+## Reflexive and transitive closure
+
+\begin{code}
+  infix  2 _—↠_
+  infix  1 begin_
+  infixr 2 _—→⟨_⟩_
+  infix  3 _∎
+
+  data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+    _∎ : ∀ {Γ A} (M : Γ ⊢ A)
+        --------
+      → M —↠ M
+
+    _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
+      → L —→ M
+      → M —↠ N
+        ------
+      → L —↠ N
+
+  begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
+    → M —↠ N
+      ------
+    → M —↠ N
+  begin M—↠N = M—↠N
+\end{code}
+
+
+## Values do not reduce
+
+\begin{code}
+  V¬—→ : ∀ {Γ A} {M N : Γ ⊢ A}
+    → Value M
+      ----------
+    → ¬ (M —→ N)
+  V¬—→ V-ƛ          ()
+  V¬—→ V-zero       ()
+  V¬—→ (V-suc VM)   (ξ-suc M—→M′)     =  V¬—→ VM M—→M′
+  V¬—→ V-con        ()
+  V¬—→ V-⟨ VM , _ ⟩ (ξ-⟨,⟩₁ M—→M′)    =  V¬—→ VM M—→M′
+  V¬—→ V-⟨ _ , VN ⟩ (ξ-⟨,⟩₂ _ N—→N′)  =  V¬—→ VN N—→N′
+\end{code}
+
+
+## Progress
+
+\begin{code}
+  data Progress {A} (M : ∅ ⊢ A) : Set where
+
+    step : ∀ {N : ∅ ⊢ A}
+      → M —→ N
+        ----------
+      → Progress M
+
+    done :
+        Value M
+        ----------
+      → Progress M
+
+  progress : ∀ {A}
+    → (M : ∅ ⊢ A)
+      -----------
+    → Progress M
+  progress (` ())
+  progress (ƛ N)                              =  done V-ƛ
+  progress (L · M) with progress L
+  ...    | step L—→L′                         =  step (ξ-·₁ L—→L′)
+  ...    | done V-ƛ with progress M
+  ...        | step M—→M′                     =  step (ξ-·₂ V-ƛ M—→M′)
+  ...        | done VM                        =  step (β-ƛ VM)
+  progress (`zero)                            =  done V-zero
+  progress (`suc M) with progress M
+  ...    | step M—→M′                         =  step (ξ-suc M—→M′)
+  ...    | done VM                            =  done (V-suc VM)
+  progress (case L M N) with progress L
+  ...    | step L—→L′                         =  step (ξ-case L—→L′)
+  ...    | done V-zero                        =  step β-zero
+  ...    | done (V-suc VL)                    =  step (β-suc VL)
+  progress (μ N)                              =  step β-μ
+  progress (con n)                            =  done V-con
+  progress (L `* M) with progress L
+  ...    | step L—→L′                         =  step (ξ-*₁ L—→L′)
+  ...    | done V-con with progress M
+  ...        | step M—→M′                     =  step (ξ-*₂ V-con M—→M′)
+  ...        | done V-con                     =  step δ-*
+  progress (`let M N) with progress M
+  ...    | step M—→M′                         =  step (ξ-let M—→M′)
+  ...    | done VM                            =  step (β-let VM)
+  progress `⟨ M , N ⟩ with progress M
+  ...    | step M—→M′                         =  step (ξ-⟨,⟩₁ M—→M′)
+  ...    | done VM with progress N
+  ...        | step N—→N′                     =  step (ξ-⟨,⟩₂ VM N—→N′)
+  ...        | done VN                        =  done (V-⟨ VM , VN ⟩)
+  progress (`proj₁ L) with progress L
+  ...    | step L—→L′                         =  step (ξ-proj₁ L—→L′)
+  ...    | done (V-⟨ VM , VN ⟩)               =  step (β-proj₁ VM VN)
+  progress (`proj₂ L) with progress L
+  ...    | step L—→L′                         =  step (ξ-proj₂ L—→L′)
+  ...    | done (V-⟨ VM , VN ⟩)               =  step (β-proj₂ VM VN)
+  progress (case× L M) with progress L
+  ...    | step L—→L′                         =  step (ξ-case× L—→L′)
+  ...    | done (V-⟨ VM , VN ⟩)               =  step (β-case× VM VN)
+\end{code}
+
+
+## Evaluation
+
+\begin{code}
+  data Gas : Set where
+    gas : ℕ → Gas
+
+  data Finished {Γ A} (N : Γ ⊢ A) : Set where
+
+     done :
+         Value N
+         ----------
+       → Finished N
+
+     out-of-gas :
+         ----------
+         Finished N
+
+  data Steps : ∀ {A} → ∅ ⊢ A → Set where
+
+    steps : ∀ {A} {L N : ∅ ⊢ A}
+      → L —↠ N
+      → Finished N
+        ----------
+      → Steps L
+
+  eval : ∀ {A}
+    → Gas
+    → (L : ∅ ⊢ A)
+      -----------
+    → Steps L
+  eval (gas zero)    L                     =  steps (L ∎) out-of-gas
+  eval (gas (suc m)) L with progress L
+  ... | done VL                            =  steps (L ∎) (done VL)
+  ... | step {M} L—→M with eval (gas m) M
+  ...    | steps M—↠N fin                  =  steps (L —→⟨ L—→M ⟩ M—↠N) fin
+\end{code}
+
+## Examples
+
+\begin{code}
+  cube : ∅ ⊢ Nat ⇒ Nat
+  cube = ƛ (# 0 `* # 0 `* # 0)
+
+  _ : cube · con 2 —↠ con 8
+  _ = 
+    begin
+      cube · con 2
+    —→⟨ β-ƛ V-con ⟩
+      con 2 `* con 2 `* con 2
+    —→⟨ ξ-*₁ δ-* ⟩
+      con 4 `* con 2
+    —→⟨ δ-* ⟩
+      con 8
+    ∎
+
+  exp10 : ∅ ⊢ Nat ⇒ Nat
+  exp10 = ƛ (`let (# 0 `* # 0)
+              (`let (# 0 `* # 0)
+                (`let (# 0 `* # 2)
+                  (# 0 `* # 0))))
+
+  _ : exp10 · con 2 —↠ con 1024
+  _ =
+    begin
+      exp10 · con 2
+    —→⟨ β-ƛ V-con ⟩
+      `let (con 2 `* con 2) (`let (# 0 `* # 0) (`let (# 0 `* con 2) (# 0 `* # 0)))
+    —→⟨ ξ-let δ-* ⟩
+      `let (con 4) (`let (# 0 `* # 0) (`let (# 0 `* con 2) (# 0 `* # 0)))
+    —→⟨ β-let V-con ⟩
+      `let (con 4 `* con 4) (`let (# 0 `* con 2) (# 0 `* # 0))
+    —→⟨ ξ-let δ-* ⟩
+      `let (con 16) (`let (# 0 `* con 2) (# 0 `* # 0))
+    —→⟨ β-let V-con ⟩
+      `let (con 16 `* con 2) (# 0 `* # 0)
+    —→⟨ ξ-let δ-* ⟩
+      `let (con 32) (# 0 `* # 0)
+    —→⟨ β-let V-con ⟩
+      con 32 `* con 32
+    —→⟨ δ-* ⟩
+      con 1024
+    ∎
+
+  swap× : ∀ {A B} → ∅ ⊢ A `× B ⇒ B `× A
+  swap× = ƛ `⟨ `proj₂ (# 0) , `proj₁ (# 0) ⟩
+
+  _ : swap× · `⟨ con 42 , `zero ⟩ —↠ `⟨ `zero , con 42 ⟩
+  _ =
+    begin
+      swap× · `⟨ con 42 , `zero ⟩
+    —→⟨ β-ƛ V-⟨ V-con , V-zero ⟩ ⟩
+      `⟨ `proj₂ `⟨ con 42 , `zero ⟩ , `proj₁ `⟨ con 42 , `zero ⟩ ⟩
+    —→⟨ ξ-⟨,⟩₁ (β-proj₂ V-con V-zero) ⟩
+      `⟨ `zero , `proj₁ `⟨ con 42 , `zero ⟩ ⟩
+    —→⟨ ξ-⟨,⟩₂ V-zero (β-proj₁ V-con V-zero) ⟩
+      `⟨ `zero , con 42 ⟩
+    ∎
+
+  swap×-case : ∀ {A B} → ∅ ⊢ A `× B ⇒ B `× A
+  swap×-case = ƛ case× (# 0) `⟨ # 0 , # 1 ⟩
+
+  _ : swap×-case · `⟨ con 42 , `zero ⟩ —↠ `⟨ `zero , con 42 ⟩
+  _ =
+    begin
+       swap×-case · `⟨ con 42 , `zero ⟩
+     —→⟨ β-ƛ V-⟨ V-con , V-zero ⟩ ⟩
+       case× `⟨ con 42 , `zero ⟩ `⟨ # 0 , # 1 ⟩
+     —→⟨ β-case× V-con V-zero ⟩
+       `⟨ `zero , con 42 ⟩
+     ∎
+\end{code}
+
+
+#### Exercise `More` (recommended in part)
+
+Formalise the remaining constructs defined in this chapter.
+Evaluate each example, applied to data as needed,
+to confirm it returns the expected answer.
+
+  * sums (recommended)
+  * unit type
+  * an alternative formulation of unit type
+  * empty type (recommended)
+  * lists
+
+
+## Bisimulation
+
+(No recommended exercises for this chapter.)
+
+#### Exercise `sim⁻¹`
+
+Show that we also have a simulation in the other direction, and hence that we have
+a bisimulation.
+
+#### Exercise `products`
+
+Show that the two formulations of products in
+Chapter [More][plfa.More]
+are in bisimulation.  The only constructs you need to include are
+variables, and those connected to functions and products.
+In this case, the simulation is _not_ lock-step.
+
+## Inference
+
+\begin{code}
+module Inference where
+\end{code}
+
+Remember to indent all code by two spaces.
+
+### Imports
+
+\begin{code}
+  import plfa.More as DB
+\end{code}
+
+### Syntax
+
+\begin{code}
+  infix   4  _∋_⦂_
+  infix   4  _⊢_↑_
+  infix   4  _⊢_↓_
+  infixl  5  _,_⦂_
+
+  infixr  7  _⇒_
+
+  infix   5  ƛ_⇒_
+  infix   5  μ_⇒_
+  infix   6  _↑
+  infix   6  _↓_
+  infixl  7  _·_
+  infix   8  `suc_
+  infix   9  `_
+\end{code}
+
+### Identifiers, types, and contexts
+
+\begin{code}
+  Id : Set
+  Id = String
+
+  data Type : Set where
+    `ℕ    : Type
+    _⇒_   : Type → Type → Type
+
+  data Context : Set where
+    ∅     : Context
+    _,_⦂_ : Context → Id → Type → Context
+\end{code}
+
+### Terms
+
+\begin{code}
+  data Term⁺ : Set
+  data Term⁻ : Set
+
+  data Term⁺ where
+    `_                        : Id → Term⁺
+    _·_                       : Term⁺ → Term⁻ → Term⁺
+    _↓_                       : Term⁻ → Type → Term⁺
+
+  data Term⁻ where
+    ƛ_⇒_                     : Id → Term⁻ → Term⁻
+    `zero                    : Term⁻
+    `suc_                    : Term⁻ → Term⁻
+    `case_[zero⇒_|suc_⇒_]    : Term⁺ → Term⁻ → Id → Term⁻ → Term⁻
+    μ_⇒_                     : Id → Term⁻ → Term⁻
+    _↑                       : Term⁺ → Term⁻
+\end{code}
+
+### Sample terms
+
+\begin{code}
+  two : Term⁻
+  two = `suc (`suc `zero)
+
+  plus : Term⁺
+  plus = (μ "p" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
+            `case (` "m") [zero⇒ ` "n" ↑
+                          |suc "m" ⇒ `suc (` "p" · (` "m" ↑) · (` "n" ↑) ↑) ])
+              ↓ `ℕ ⇒ `ℕ ⇒ `ℕ
+
+  2+2 : Term⁺
+  2+2 = plus · two · two
+\end{code}
+
+### Lookup 
+
+\begin{code}
+  data _∋_⦂_ : Context → Id → Type → Set where
+
+    Z : ∀ {Γ x A}
+        --------------------
+      → Γ , x ⦂ A ∋ x ⦂ A
+
+    S : ∀ {Γ x y A B}
+      → x ≢ y
+      → Γ ∋ x ⦂ A
+        -----------------
+      → Γ , y ⦂ B ∋ x ⦂ A
+\end{code}
+
+### Bidirectional type checking
+
+\begin{code}
+  data _⊢_↑_ : Context → Term⁺ → Type → Set
+  data _⊢_↓_ : Context → Term⁻ → Type → Set
+
+  data _⊢_↑_ where
+
+    ⊢` : ∀ {Γ A x}
+      → Γ ∋ x ⦂ A
+        -----------
+      → Γ ⊢ ` x ↑ A
+
+    _·_ : ∀ {Γ L M A B}
+      → Γ ⊢ L ↑ A ⇒ B
+      → Γ ⊢ M ↓ A
+        -------------
+      → Γ ⊢ L · M ↑ B
+
+    ⊢↓ : ∀ {Γ M A}
+      → Γ ⊢ M ↓ A
+        ---------------
+      → Γ ⊢ (M ↓ A) ↑ A
+
+  data _⊢_↓_ where
+
+    ⊢ƛ : ∀ {Γ x N A B}
+      → Γ , x ⦂ A ⊢ N ↓ B
+        -------------------
+      → Γ ⊢ ƛ x ⇒ N ↓ A ⇒ B
+
+    ⊢zero : ∀ {Γ}
+        --------------
+      → Γ ⊢ `zero ↓ `ℕ
+
+    ⊢suc : ∀ {Γ M}
+      → Γ ⊢ M ↓ `ℕ
+        ---------------
+      → Γ ⊢ `suc M ↓ `ℕ
+
+    ⊢case : ∀ {Γ L M x N A}
+      → Γ ⊢ L ↑ `ℕ
+      → Γ ⊢ M ↓ A
+      → Γ , x ⦂ `ℕ ⊢ N ↓ A
+        -------------------------------------
+      → Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ↓ A
+
+    ⊢μ : ∀ {Γ x N A}
+      → Γ , x ⦂ A ⊢ N ↓ A
+        -----------------
+      → Γ ⊢ μ x ⇒ N ↓ A
+
+    ⊢↑ : ∀ {Γ M A B}
+      → Γ ⊢ M ↑ A
+      → A ≡ B
+        -------------
+      → Γ ⊢ (M ↑) ↓ B
+\end{code}
+
+
+### Type equality
+
+\begin{code}
+  _≟Tp_ : (A B : Type) → Dec (A ≡ B)
+  `ℕ      ≟Tp `ℕ              =  yes refl
+  `ℕ      ≟Tp (A ⇒ B)         =  no λ()
+  (A ⇒ B) ≟Tp `ℕ              =  no λ()
+  (A ⇒ B) ≟Tp (A′ ⇒ B′)
+    with A ≟Tp A′ | B ≟Tp B′
+  ...  | no A≢    | _         =  no λ{refl → A≢ refl}
+  ...  | yes _    | no B≢     =  no λ{refl → B≢ refl}
+  ...  | yes refl | yes refl  =  yes refl
+\end{code}
+
+### Prerequisites
+
+\begin{code}
+  dom≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′
+  dom≡ refl = refl
+
+  rng≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → B ≡ B′
+  rng≡ refl = refl
+
+  ℕ≢⇒ : ∀ {A B} → `ℕ ≢ A ⇒ B
+  ℕ≢⇒ ()
+\end{code}
+
+
+### Unique lookup
+
+\begin{code}
+  uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
+  uniq-∋ Z Z                 =  refl
+  uniq-∋ Z (S x≢y _)         =  ⊥-elim (x≢y refl)
+  uniq-∋ (S x≢y _) Z         =  ⊥-elim (x≢y refl)
+  uniq-∋ (S _ ∋x) (S _ ∋x′)  =  uniq-∋ ∋x ∋x′
+\end{code}
+
+### Unique synthesis
+
+\begin{code}
+  uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B
+  uniq-↑ (⊢` ∋x) (⊢` ∋x′)       =  uniq-∋ ∋x ∋x′
+  uniq-↑ (⊢L · ⊢M) (⊢L′ · ⊢M′)  =  rng≡ (uniq-↑ ⊢L ⊢L′)
+  uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′)       =  refl 
+\end{code}
+
+## Lookup type of a variable in the context
+
+\begin{code}
+  ext∋ : ∀ {Γ B x y}
+    → x ≢ y
+    → ¬ ∃[ A ]( Γ ∋ x ⦂ A )
+      -----------------------------
+    → ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
+  ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
+  ext∋ _   ¬∃ ⟨ A , S _ ⊢x ⟩  =  ¬∃ ⟨ A , ⊢x ⟩
+
+  lookup : ∀ (Γ : Context) (x : Id)
+      -----------------------
+    → Dec (∃[ A ](Γ ∋ x ⦂ A))
+  lookup ∅ x                        =  no  (λ ())
+  lookup (Γ , y ⦂ B) x with x ≟ y
+  ... | yes refl                    =  yes ⟨ B , Z ⟩
+  ... | no x≢y with lookup Γ x
+  ...             | no  ¬∃          =  no  (ext∋ x≢y ¬∃)
+  ...             | yes ⟨ A , ⊢x ⟩  =  yes ⟨ A , S x≢y ⊢x ⟩
+\end{code}
+
+### Promoting negations
+
+\begin{code}
+  ¬arg : ∀ {Γ A B L M}
+    → Γ ⊢ L ↑ A ⇒ B
+    → ¬ Γ ⊢ M ↓ A
+      -------------------------
+    → ¬ ∃[ B′ ](Γ ⊢ L · M ↑ B′)
+  ¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
+
+  ¬switch : ∀ {Γ M A B}
+    → Γ ⊢ M ↑ A
+    → A ≢ B
+      ---------------
+    → ¬ Γ ⊢ (M ↑) ↓ B
+  ¬switch ⊢M A≢B (⊢↑ ⊢M′ A′≡B) rewrite uniq-↑ ⊢M ⊢M′ = A≢B A′≡B
+\end{code}
+
+
+## Synthesize and inherit types
+
+\begin{code}
+  synthesize : ∀ (Γ : Context) (M : Term⁺)
+      -----------------------
+    → Dec (∃[ A ](Γ ⊢ M ↑ A))
+
+  inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
+      ---------------
+    → Dec (Γ ⊢ M ↓ A)
+
+  synthesize Γ (` x) with lookup Γ x
+  ... | no  ¬∃              =  no  (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ })
+  ... | yes ⟨ A , ∋x ⟩      =  yes ⟨ A , ⊢` ∋x ⟩
+  synthesize Γ (L · M) with synthesize Γ L
+  ... | no  ¬∃              =  no  (λ{ ⟨ _ , ⊢L  · _  ⟩  →  ¬∃ ⟨ _ , ⊢L ⟩ })
+  ... | yes ⟨ `ℕ ,    ⊢L ⟩  =  no  (λ{ ⟨ _ , ⊢L′ · _  ⟩  →  ℕ≢⇒ (uniq-↑ ⊢L ⊢L′) })
+  ... | yes ⟨ A ⇒ B , ⊢L ⟩ with inherit Γ M A
+  ...    | no  ¬⊢M          =  no  (¬arg ⊢L ¬⊢M)
+  ...    | yes ⊢M           =  yes ⟨ B , ⊢L · ⊢M ⟩  
+  synthesize Γ (M ↓ A) with inherit Γ M A
+  ... | no  ¬⊢M             =  no  (λ{ ⟨ _ , ⊢↓ ⊢M ⟩  →  ¬⊢M ⊢M })
+  ... | yes ⊢M              =  yes ⟨ A , ⊢↓ ⊢M ⟩
+
+  inherit Γ (ƛ x ⇒ N) `ℕ      =  no  (λ())
+  inherit Γ (ƛ x ⇒ N) (A ⇒ B) with inherit (Γ , x ⦂ A) N B
+  ... | no ¬⊢N                =  no  (λ{ (⊢ƛ ⊢N)  →  ¬⊢N ⊢N })
+  ... | yes ⊢N                =  yes (⊢ƛ ⊢N)
+  inherit Γ `zero `ℕ          =  yes ⊢zero
+  inherit Γ `zero (A ⇒ B)     =  no  (λ())
+  inherit Γ (`suc M) `ℕ with inherit Γ M `ℕ
+  ... | no ¬⊢M                =  no  (λ{ (⊢suc ⊢M)  →  ¬⊢M ⊢M })
+  ... | yes ⊢M                =  yes (⊢suc ⊢M)
+  inherit Γ (`suc M) (A ⇒ B)  =  no  (λ())
+  inherit Γ (`case L [zero⇒ M |suc x ⇒ N ]) A with synthesize Γ L
+  ... | no ¬∃                 =  no  (λ{ (⊢case ⊢L  _ _) → ¬∃ ⟨ `ℕ , ⊢L ⟩})
+  ... | yes ⟨ _ ⇒ _ , ⊢L ⟩    =  no  (λ{ (⊢case ⊢L′ _ _) → ℕ≢⇒ (uniq-↑ ⊢L′ ⊢L) })   
+  ... | yes ⟨ `ℕ ,    ⊢L ⟩ with inherit Γ M A
+  ...    | no ¬⊢M             =  no  (λ{ (⊢case _ ⊢M _) → ¬⊢M ⊢M })
+  ...    | yes ⊢M with inherit (Γ , x ⦂ `ℕ) N A
+  ...       | no ¬⊢N          =  no  (λ{ (⊢case _ _ ⊢N) → ¬⊢N ⊢N })
+  ...       | yes ⊢N          =  yes (⊢case ⊢L ⊢M ⊢N)
+  inherit Γ (μ x ⇒ N) A with inherit (Γ , x ⦂ A) N A
+  ... | no ¬⊢N                =  no  (λ{ (⊢μ ⊢N) → ¬⊢N ⊢N })
+  ... | yes ⊢N                =  yes (⊢μ ⊢N)
+  inherit Γ (M ↑) B with synthesize Γ M
+  ... | no  ¬∃                =  no  (λ{ (⊢↑ ⊢M _) → ¬∃ ⟨ _ , ⊢M ⟩ })
+  ... | yes ⟨ A , ⊢M ⟩ with A ≟Tp B
+  ...   | no  A≢B             =  no  (¬switch ⊢M A≢B)
+  ...   | yes A≡B             =  yes (⊢↑ ⊢M A≡B)
+\end{code}
+
+### Erasure
+
+\begin{code}
+  ∥_∥Tp : Type → DB.Type
+  ∥ `ℕ ∥Tp             =  DB.`ℕ
+  ∥ A ⇒ B ∥Tp          =  ∥ A ∥Tp DB.⇒ ∥ B ∥Tp
+
+  ∥_∥Cx : Context → DB.Context
+  ∥ ∅ ∥Cx              =  DB.∅
+  ∥ Γ , x ⦂ A ∥Cx      =  ∥ Γ ∥Cx DB., ∥ A ∥Tp
+
+  ∥_∥∋ : ∀ {Γ x A} → Γ ∋ x ⦂ A → ∥ Γ ∥Cx DB.∋ ∥ A ∥Tp
+  ∥ Z ∥∋               =  DB.Z
+  ∥ S x≢ ⊢x ∥∋         =  DB.S ∥ ⊢x ∥∋
+
+  ∥_∥⁺ : ∀ {Γ M A} → Γ ⊢ M ↑ A → ∥ Γ ∥Cx DB.⊢ ∥ A ∥Tp
+  ∥_∥⁻ : ∀ {Γ M A} → Γ ⊢ M ↓ A → ∥ Γ ∥Cx DB.⊢ ∥ A ∥Tp
+
+  ∥ ⊢` ⊢x ∥⁺           =  DB.` ∥ ⊢x ∥∋
+  ∥ ⊢L · ⊢M ∥⁺         =  ∥ ⊢L ∥⁺ DB.· ∥ ⊢M ∥⁻
+  ∥ ⊢↓ ⊢M ∥⁺           =  ∥ ⊢M ∥⁻
+
+  ∥ ⊢ƛ ⊢N ∥⁻           =  DB.ƛ ∥ ⊢N ∥⁻
+  ∥ ⊢zero ∥⁻           =  DB.`zero
+  ∥ ⊢suc ⊢M ∥⁻         =  DB.`suc ∥ ⊢M ∥⁻
+  ∥ ⊢case ⊢L ⊢M ⊢N ∥⁻  =  DB.case ∥ ⊢L ∥⁺ ∥ ⊢M ∥⁻ ∥ ⊢N ∥⁻
+  ∥ ⊢μ ⊢M ∥⁻           =  DB.μ ∥ ⊢M ∥⁻
+  ∥ ⊢↑ ⊢M refl ∥⁻      =  ∥ ⊢M ∥⁺
+\end{code}
+
+#### Exercise `bidirectional-mul` (recommended) {#bidirectional-mul}
+
+Rewrite your definition of multiplication from
+Chapter [Lambda][plfa.Lambda], decorated to support inference.
+
+
+#### Exercise `bidirectional-products` (recommended) {#bidirectional-products}
+
+Extend the bidirectional type rules to include products from
+Chapter [More][plfa.More].
+
+
+#### Exercise `bidirectional-rest` (stretch)
+
+Extend the bidirectional type rules to include the rest of the constructs from
+Chapter [More][plfa.More].
+
+
+#### Exercise `inference-mul` (recommended)
+
+Rewrite your definition of multiplication from
+Chapter [Lambda][plfa.Lambda] decorated to support inference, and show
+that erasure of the inferred typing yields your definition of
+multiplication from Chapter [DeBruijn][plfa.DeBruijn].
+
+
+#### Exercise `inference-products` (recommended)
+
+Extend bidirectional inference to include products from
+Chapter [More][plfa.More].
+
+
+#### Exercise `inference-rest` (stretch)
+
+Extend bidirectional inference to include the rest of the constructs from
+Chapter [More][plfa.More].
+
+## Untyped
+
+#### Exercise (`Type≃⊤`)
+
+Show that `Type` is isomorphic to `⊤`, the unit type.
+
+#### Exercise (`Context≃ℕ`)
+
+Show that `Context` is isomorphic to `ℕ`.
+
+#### Exercise (`variant-1`)
+
+How would the rules change if we want call-by-value where terms
+normalise completely?  Assume that `β` should not permit reduction
+unless both terms are in normal form.
+
+#### Exercise (`variant-2`)
+
+How would the rules change if we want call-by-value where terms
+do not reduce underneath lambda?  Assume that `β`
+permits reduction when both terms are values (that is, lambda
+abstractions).  What would `2+2ᶜ` reduce to in this case?
+
+#### Exercise `2+2≡four`
+
+Use the evaluator to confirm that `2+2` and `four` normalise to
+the same term.
+
+#### Exercise `multiplication-untyped` (recommended)
+
+Use the encodings above to translate your definition of
+multiplication from previous chapters with the Scott
+representation and the encoding of the fixpoint operator.
+Confirm that two times two is four.
+
+#### Exercise `encode-more` (stretch)
+
+Along the lines above, encode all of the constructs of
+Chapter [More][plfa.More],
+save for primitive numbers, in the untyped lambda calculus.
diff --git a/tspl/Assignment5.pdf b/tspl/Assignment5.pdf
new file mode 100644
index 00000000..46f859d9
Binary files /dev/null and b/tspl/Assignment5.pdf differ
diff --git a/tspl/Assignment5.tex b/tspl/Assignment5.tex
new file mode 100644
index 00000000..ee9e2e61
--- /dev/null
+++ b/tspl/Assignment5.tex
@@ -0,0 +1,422 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% I N F O R M A T I C S
+%  Honours Exam LaTeX Template for Exam Authors
+%
+%  Created: 12-Oct-2009 by G.O.Passmore.
+%  Last Updated: 10-Sep-2018 by I. Murray
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% The following define the status of the exam papers in the order
+%%% required.  Simply remove the comment (i.e., the % symbol) just
+%%% before the appropriate one and comment the others out.
+
+%\newcommand\status{\internal}
+%\newcommand\status{\external}
+\newcommand\status{\final}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% The following three lines are always required.  You may add
+%%% custom packages to the one already defined if necessary.
+
+\documentclass{examhons2018}
+\usepackage{amssymb}
+\usepackage{amsmath}
+\usepackage{semantic}
+\usepackage{stix}
+
+%%% Uncomment the \checkmarksfalse line if the macros that check the
+%%% mark totals cause problems. However, please do not make your
+%%% questions add up to a non-standard number of marks without
+%%% permission of the convenor.
+%\checkmarksfalse
+
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Replace {ad} below with the ITO code for your course.  This will
+%  be used by the ITO LaTeX installation to install course-specific
+%  data into the exam versions it produces from this document.
+% 
+% Your choices are (in course title order):
+%
+%   {anlp}     - Acc. Natural Language Processing	            (MSc)
+%   {aleone}   - Adaptive Learning Environments 1              (Inf4)
+%   {adbs}     - Advanced Databases                            (Inf4)
+%   {av}       - Advanced Vision                               (Inf4)
+%   {av-dl}    - Advanced Vision - distance learning            (MSc)
+%   {apl}      - Advances in Programming Languages             (Inf4)
+%   {abs}      - Agent Based Systems [L10]                     (Inf3)
+%   {afds}     - Algorithmic Foundations of Data Science        (MSc)
+%   {agta}     - Algorithmic Game Theory and its Apps.          (MSc)
+%   {ads}      - Algorithms and Data Structures                (Inf3)
+%   {ad}       - Applied Databases                              (MSc)
+%   {aipf}     - Artificial Intelligence Present and Future     (MSc)
+%   {ar}       - Automated Reasoning 	                       (Inf3)
+%   {asr}      - Automatic Speech Recognition                  (Inf4)
+%   {bioone}   - Bioinformatics 1                               (MSc)
+%   {biotwo}   - Bioinformatics 2                               (MSc)
+%	{bdl}      - Blockchains and Distributed Ledgers		   (Inf4)
+%   {cqi}      - Categories and Quantum Informatics             (MSc)
+%   {copt}     - Compiler Opimisation [L11]                    (Inf4)
+%   {ct}       - Compiling Techniques                          (Inf3)
+%   {ccs}      - Computational Cognitive Science               (Inf3)
+%   {cmc}      - Computational Complexity                      (Inf4)
+%   {ca}       - Computer Algebra                              (Inf4)
+%   {cav}      - Computer Animation and Visualisation          (Inf4)
+%   {car}      - Computer Architecture                         (Inf3)
+%   {comn}     - Computer Comms. and Networks                  (Inf3)
+%   {cd}       - Computer Design                               (Inf3)
+%   {cg}       - Computer Graphics [L11]                       (Inf4)
+%   {cn}       - Computer Networking [L11]                     (Inf4)
+%   {cp}       - Computer Prog. Skills and Concepts         (nonhons)
+%   {cs}       - Computer Security                             (Inf3)
+%   {dds}      - Data, Design and Society                   (nonhons)
+%   {dme}      - Data Mining and Exploration                   (Msc)
+%   {dbs}      - Database Systems                              (Inf3)
+%   {dmr}      - Decision Making in Robots and Autonomous Agents(MSc)
+%   {dmmr}     - Discrete Maths. and Math. Reasoning        (nonhons)
+%   {ds}       - Distributed Systems [L11]                     (Inf4)
+%   {epl}      - Elements of Programming Languages             (Inf3)
+%   {es}       - Embedded Software                             (Inf4)
+%   {exc}      - Extreme Computing                             (Inf4)
+%   {fv}       - Formal Verification                           (Inf4)
+%   {fnlp}     - Foundations of Natural Language Processing    (Inf3)
+%   {hci}      - Human-Computer Interaction [L11]              (Inf4)
+%   {infonea}  - Informatics 1 - Introduction to Computation(nonhons)
+%   different sittings for INF1A programming exams
+%   {infoneapone}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infoneaptwo}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infoneapthree}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infonecg} - Informatics 1 - Cognitive Science          (nonhons)
+%   {infonecl} - Informatics 1 - Computation and Logic      (nonhons)
+%   {infoneda} - Informatics 1 - Data and Analysis          (nonhons)
+%   {infonefp} - Informatics 1 - Functional Programming     (nonhons)
+%   If there are two sittings of FP, use infonefpam for the first
+%   paper and infonefppm for the second sitting.
+%   {infoneop} - Informatics 1 - Object-Oriented Programming(nonhons)
+%   If there are two sittings of OOP, use infoneopam for the first
+%   paper and infoneoppm for the second sitting.
+%   {inftwoa}  - Informatics 2A: Proc. F&N Languages        (nonhons)
+%   {inftwob}  - Informatics 2B: Algs., D.Structs., Learning(nonhons)
+%   {inftwoccs}- Informatics 2C-CS: Computer Systems        (nonhons)
+%   {inftwocse}- Informatics 2C: Software Engineering       (nonhons)
+%   {inftwod}  - Informatics 2D: Reasoning and Agents       (nonhons)
+%   {iar}      - Intelligent Autonomous Robotics               (Inf4)
+%   {it}       - Information Theory                             (MSc)
+%   {imc}      - Introduction to Modern Cryptography           (Inf4)
+%   {iotssc}   - Internet of Things, Systems, Security and the Cloud   (Inf4)
+%   (iqc)      - Introduction to Quantum Computing             (Inf4)
+%   (itcs)     - Introduction to Theoretical Computer Science  (Inf3)
+%   {ivc}      - Image and Vision Computing			           (MSc)
+%   {ivr}      - Introduction to Vision and Robotics           (Inf3)
+%   {ivr-dl}   - Introduction to Vision and Robotics - distance learning (Msc)
+%   {iaml}     - Introductory Applied Machine Learning         (MSc)
+%   {iaml-dl}  - Introductory Applied Machine Learning - distance learning (MSc)
+%   {lpt}      - Logic Programming - Theory                    (Inf3)
+%   {lpp}      - Logic Programming - Programming               (Inf3)
+%   {mlpr}     - Machine Learning & Pattern Recognition        (Inf4)
+%   {mt}       - Machine Translation                           (Inf4)    
+%   {mi}       - Music Informatics                              (MSc)
+%   {nlu}      - Natural Language Understanding [L11]          (Inf4)
+%   {nc}       - Neural Computation                             (MSc)
+%   {nat}      - Natural Computing                              (MSc)
+%   {nluplus}  - Natural Language Understanding, Generation, and Machine Translation(MSc)
+%   {nip}      - Neural Information Processing                  (MSc)
+%   {os}       - Operating Systems                             (Inf3)
+%   {pa}       - Parallel Architectures [L11]                  (Inf4)
+%   {pdiot}    - Principles and Design of IoT Systems          (Inf4)
+%   {ppls}     - Parallel Prog. Langs. and Sys. [L11]          (Inf4)
+%   {pm}       - Performance Modelling                         (Inf4)  
+%   {pmr}      - Probabilistic Modelling and Reasoning          (MSc)
+%   {pi}       - Professional Issues                           (Inf3)
+%   {rc}       - Randomness and Computation                    (Inf4)
+%   {rl}       - Reinforcement Learning                         (MSc)
+%   {rlsc}     - Robot Learning and Sensorimotor Control        (MSc)
+%   {rss}      - Robotics: Science and Systems                  (MSc)
+%   {sp}       - Secure Programming                            (Inf4)
+%   {sws}      - Semantic Web Systems                          (Inf4)
+%   {stn}      - Social and Technological Networks             (Inf4)
+%   {sapm}     - Software Arch., Proc. and Mgmt. [L11]         (Inf4)
+%   {sdm}      - Software Design and Modelling                 (Inf3)
+%   {st}       - Software Testing                              (Inf3)
+%   {ttds}     - Text Technologies for Data Science            (Inf4)
+%   {tspl}     - Types and Semantics for Programming Langs.    (Inf4)
+%   {usec}     - Usable Security and Privacy                   (Inf4)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\setcourse{tspl}
+\initcoursedata
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Set your exam rubric type.
+% 
+% Most courses in the School have exams that add up to 50 marks,
+% and your choices are:
+%    {qu1_and_either_qu2_or_qu3, any_two_of_three, do_exam}
+% (which include the "CALCULATORS MAY NOT BE USED..." text), or
+%    {qu1_and_either_qu2_or_qu3_calc, any_two_of_three_calc, do_exam_calc}
+% (which DO NOT include the "CALCULATORS MAY NOT BE USED..." text), or
+%    {custom}.
+%
+% Note, if you opt to create a custom rubric, you must: 
+%    
+%   (i) **have permission** from the appropriate authority, and 
+%  (ii) execute:
+%
+%        \setrubrictype{} to specify the custom rubric information.
+% 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\setrubric{qu1_and_either_qu2_or_qu3}
+
+\examtitlepage
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Manual override for total page number computation.
+%
+% As long as you run latex upon this document three times in a row,
+%  the right number of `total pages' should be computed and placed
+%  in the footer of all pages except the title page.  
+%
+% But, if this fails, you can set that number yourself with the 
+%  following command:
+%
+%    \settotalpages{n} with n a natural number.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Beginning of your exam text.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{enumerate}
+ 
+\item \rubricqA
+
+\newcommand{\Tree}{\texttt{Tree}}
+\newcommand{\AllT}{\texttt{AllT}}
+\newcommand{\AnyT}{\texttt{AnyT}}
+\newcommand{\leaf}{\texttt{leaf}}
+\newcommand{\branch}{\texttt{branch}}  
+\newcommand{\here}{\texttt{here}}
+\renewcommand{\left}{\texttt{left}}
+\renewcommand{\right}{\texttt{right}}
+\newcommand{\ubar}{\texttt{\underline{~}}}
+
+Consider a type of trees defined as follows.
+\begin{gather*}
+%
+  \inference[\leaf]
+    {A}
+    {Tree~A}
+%
+\quad
+%    
+  \inference[\ubar\branch\ubar]
+    {Tree~A \\
+     Tree~A}
+   {Tree~A}
+%
+\end{gather*}
+
+Given a predicate $P$ over $A$, we define predicates $\AllT$ and
+$\AnyT$ which hold when $P$ holds for \emph{every} leaf in the tree
+and when $P$ holds for \emph{some} leaf in the tree, respectively.
+\begin{gather*}
+%
+  \inference[\leaf]
+    {P~x}
+    {\AllT~P~(\leaf~x)}
+%
+\quad
+%    
+  \inference[\ubar\branch\ubar]
+    {\AllT~P~xt \\   
+     \AllT~P~yt}
+    {\AllT~P~(xt~\branch~yt)}
+%  
+\\~\\  
+%
+  \inference[\leaf]
+    {P~x}
+    {\AnyT~P~(\leaf~x)}
+%
+\quad
+%    
+  \inference[\left]
+    {\AnyT~P~xt}  
+    {\AnyT~P~(xt~\branch~yt)}
+%
+\quad
+%    
+  \inference[\right]
+    {\AnyT~P~yt}  
+    {\AnyT~P~(xt~\branch~yt)}
+%
+\end{gather*}    
+
+\begin{itemize}
+
+\item[(a)] Formalise the definitions above.
+
+\marks{12}
+
+\item[(b)] Prove $\AllT~({\neg\ubar}~\circ~P)~xt$
+  implies $\neg~(\AnyT~P~xt)$, for all trees $xt$.
+
+\marks{13}
+
+\end{itemize}
+
+\newpage
+
+\item \rubricqB
+
+\newcommand{\COMP}{\texttt{Comp}}
+\newcommand{\OK}{\texttt{ok}}
+\newcommand{\ERROR}{\texttt{error}}
+\newcommand{\LETC}{\texttt{letc}}
+\newcommand{\IN}{\texttt{in}}  
+
+\newcommand{\Comp}[1]{\COMP~#1}
+\newcommand{\error}[1]{\ERROR~#1}
+\newcommand{\ok}[1]{\OK~#1}
+\newcommand{\letc}[3]{\LETC~#1\leftarrow#2~\IN~#3}
+
+\newcommand{\comma}{\,,\,}
+\newcommand{\V}{\texttt{V}}
+\newcommand{\dash}{\texttt{-}}
+\newcommand{\Value}{\texttt{Value}}
+\newcommand{\becomes}{\longrightarrow}
+\newcommand{\subst}[3]{#1~\texttt{[}~#2~\texttt{:=}~#3~\texttt{]}}
+
+You will be provided with a definition of intrinsically-typed lambda
+calculus in Agda. Consider constructs satisfying the following rules,
+written in extrinsically-typed style.
+
+A computation of type $\Comp{A}$ returns either an error with a
+message $msg$ which is a string, or an ok value of a term $M$ of type $A$.
+Consider constructs satisfying the following rules:
+
+Typing:
+\begin{gather*}
+\inference[$\ERROR$]
+  {}
+  {\Gamma \vdash \error{msg} \typecolon \Comp{A}}
+\qquad
+\inference[$\OK$]
+  {\Gamma \vdash M \typecolon A}
+  {\Gamma \vdash \ok{M} \typecolon \Comp{A}}
+\\~\\
+\inference[$\LETC$]
+  {\Gamma \vdash M \typecolon \Comp{A} \\
+   \Gamma \comma x \typecolon A \vdash N \typecolon \Comp{B}}
+  {\Gamma \vdash \letc{x}{M}{N} \typecolon \Comp{B}}
+\end{gather*}
+
+Values:
+\begin{gather*}
+\inference[\V\dash\ERROR]
+  {}
+  {\Value~(\error{msg})}
+\qquad
+\inference[\V\dash\OK]
+  {\Value~V}
+  {\Value~(\ok{V})}
+\end{gather*}
+
+Reduction:
+\begin{gather*}
+\inference[$\xi\dash\OK$]
+  {M \becomes M'}
+  {\ok{M} \becomes \ok{M'}}
+\qquad
+\inference[$\xi\dash\LETC$]
+  {M \becomes M'}
+  {\letc{x}{M}{N} \becomes \letc{x}{M'}{N}}
+\\~\\
+\inference[$\beta\dash\ERROR$]
+  {}
+  {\letc{x}{(\error{msg})}{t} \becomes \error{msg}}
+\\~\\
+\inference[$\beta\dash\OK$]
+  {\Value{V}}
+  {\letc{x}{(\ok{V})}{N} \becomes \subst{N}{x}{V}}
+\end{gather*}
+
+\begin{enumerate}
+\item[(a)] Extend the given definition to formalise the evaluation
+           and typing rules, including any other required definitions.
+      \marks{12}
+
+\item[(b)] Prove progress. You will be provided with a proof of progress for
+           the simply-typed lambda calculus that you may extend.
+      \marks{13}
+\end{enumerate}
+
+Please delimit any code you add as follows.
+\begin{verbatim}
+-- begin
+-- end
+\end{verbatim}
+
+\newpage
+
+\item \rubricqC
+
+\newcommand{\TT}{\texttt{tt}}
+\newcommand{\CASETOP}{{\texttt{case}\top}}
+\newcommand{\casetop}[2]{\CASETOP~#1~{\texttt{[tt}\!\Rightarrow}~#2~\texttt{]}}
+\newcommand{\up}{\uparrow}
+\newcommand{\dn}{\downarrow}
+
+You will be provided with a definition of inference for extrinsically-typed lambda
+calculus in Agda. Consider constructs satisfying the following rules,
+written in extrinsically-typed style that support bidirectional inference.
+
+Typing:
+\begin{gather*}
+\inference[$\TT$]
+  {}
+  {\Gamma \vdash \TT \dn \top}
+\\~\\
+\inference[$\CASETOP$]
+  {\Gamma \vdash L \up \top \\
+   \Gamma \vdash M \dn A}
+  {\Gamma \vdash \casetop{L}{M} \dn A} 
+\end{gather*}
+
+\begin{enumerate}
+\item[(a)] Extend the given definition to formalise the typing rules,
+      and update the definition of equality on types.
+      \marks{10}
+
+\item[(b)] Extend the code to support type inference for the new features.
+      \marks{15}
+\end{enumerate}
+
+Please delimit any code you add as follows.
+\begin{verbatim}
+-- begin
+-- end
+\end{verbatim}
+
+\end{enumerate}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% End of your exam text.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
+
diff --git a/tspl/Assignments.lagda b/tspl/Assignments.lagda
new file mode 100644
index 00000000..bc9491ea
--- /dev/null
+++ b/tspl/Assignments.lagda
@@ -0,0 +1,164 @@
+---
+title     : "Assignments: Summary of all assignments"
+layout    : page
+permalink : /Assignments/
+---
+
+## Assignments
+
+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.
+
+* [Assignment 1][Assignment1] Due 4pm Thursday 4 October (Week 3)
+
+  + Naturals
+    - `seven`
+    - `+-example`
+    - `*-example`
+    - `_^_` (recommended)
+    - `∸-examples` (recommended)
+    - `Bin` (stretch)
+
+  + Induction
+    - `operators`
+    - `finite-+-assoc` (stretch)
+    - `+-swap` (recommended)
+    - `*-distribʳ-+` (recommended)
+    - `*-assoc` (recommended)
+    - `*-comm`
+    - `0∸n≡n`
+    - `∸-+-assoc`
+    - `Bin-laws` (stretch)
+
+  + Relations
+    - `orderings`
+    - `≤-antisym-cases`
+    - `*-mono-≤` (stretch)
+    - `<-trans` (recommended)
+    - `trichotomy`
+    - `+-mono-<`
+    - `≤-iff-<` (recommended)
+    - `<-trans-revisited`
+    - `o+o≡e` (recommended)
+    - `Bin-predicates` (stretch)
+
+* [Assignment 2][Assignment2]. Due 4pm Thursday 18 October (Week 5)
+
+  + Equality
+    - `≤-reasoning` (stretch)
+
+  + Isomorphism
+    - `≃-implies-≲`
+    - `_⇔_` (recommended)
+    - `Bin-embedding` (stretch)
+
+  + Connectives
+    - `⇔≃×` (recommended)
+    - `⊎-comm` (recommended)
+    - `⊎-assoc`
+    - `⊥-identityˡ` (recommended)
+    - `⊥-identityʳ`
+    - `⊎-weak-×` (recommended)
+    - `⊎×-implies-×⊎`
+
+  + Negation
+    - `<-irreflexive` (recommended)
+    - `trichotomy`
+    - `⊎-dual-×` (recommended)
+    - `Classical` (stretch)
+    - `Stable` (stretch)
+
+  + Quantifiers
+    - `∀-distrib-×` (recommended)
+    - `⊎∀-implies-∀⊎`
+    - `∃-distrib-⊎` (recommended)
+    - `∃×-implies-×∃`
+    - `∃-even-odd`
+    - `∃-+-≤`
+    - `∃¬-implies-¬∀` (recommended)
+    - `Bin-isomorphism` (stretch)
+
+  + Decidable
+    - `_<?_` (recommended)
+    - `_≡ℕ?_`
+    - `erasure`
+    - `iff-erasure` (recommended)
+
+* Assignment 3. Due 4pm Thursday 1 November (Week 7)
+
+  + Lists
+    - `reverse-++-commute` (recommended)
+    - `reverse-involutive` (recommended)
+    - `map-compose`
+    - `map-++-commute`
+    - `map-Tree`
+    - `product` (recommended)
+    - `fold-++` (recommended)
+    - `map-is-foldr`
+    - `fold-Tree`
+    - `map-is-fold-Tree`
+    - `sum-downFrom` (stretch)
+    - `foldl`
+    - `foldr-monoid-foldl`
+    - `Any-++-⇔` (recommended)
+    - `All-++-≃` (stretch)
+    - `¬Any≃All¬` (stretch)
+    - `any?` (stretch)
+    - `filter?` (stretch)
+
+  + Lambda
+    - `mul` (recommended)
+    - `primed` (stretch)
+    - `_[_:=_]′` (stretch)
+    - `—↠≃—↠′`
+    - `plus-example`
+    - `mul-type` (recommended)
+
+  + Properties
+    - `Progress-≃`
+    - `progress′`
+    - `value?` (recommended)
+    - `subst′` (stretch)
+    - `mul-example` (recommended)
+    - `progress-preservation`
+    - `subject-expansion`
+    - `stuck`
+    - `unstuck` (recommended)
+
+* Assignment 4. Due 4pm Thursday 15 November (Week 9)
+
+
+  + DeBruijn
+    - `mul` (recommended)
+    - `V¬—→`
+    - `mul-example` (recommended)
+
+  + More
+    - `More` (recommended)
+
+  + Bisimulation
+    - `_†`
+    - `~val⁻¹`
+    - `sim⁻¹`
+    - `products`
+
+  + Inference
+    - `bidirectional-ps` (recommended)
+    - `bidirectional-rest` (stretch)
+    - `inference-p` (recommended)
+    - `inference-rest` (stretch)
+
+  + Untyped
+    - `Type≃⊤`
+    - `Context≃ℕ`
+    - `variant-1` (recommended)
+    - `variant-2`
+    - `2+2≡four` (recommended)
+    - `encode-more` (stretch)
+
+* Assignment 5. Due 4pm Thursday 22 November (Week 10)
diff --git a/tspl/Exam.lagda b/tspl/Exam.lagda
new file mode 100644
index 00000000..4962ae29
--- /dev/null
+++ b/tspl/Exam.lagda
@@ -0,0 +1,680 @@
+---
+title     : "Exam: TSPL Mock Exam file"
+layout    : page
+permalink : /Exam/
+---
+
+
+\begin{code}
+module Exam where
+\end{code}
+
+**IMPORTANT** For ease of marking, when modifying the given code please write
+
+    -- begin
+    -- end
+
+before and after code you add, to indicate your changes.
+
+## Imports
+
+\begin{code}
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_; refl; sym; trans; cong; _≢_)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.List using (List; []; _∷_; _++_)
+open import Data.Product using (∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
+open import Data.String using (String)
+open import Data.String.Unsafe using (_≟_)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import Relation.Binary using (Decidable)
+\end{code}
+
+## Problem 1
+
+\begin{code}
+module Problem1 where
+
+  open import Function using (_∘_)
+\end{code}
+
+Remember to indent all code by two spaces.
+
+### (a)
+
+### (b)
+
+### (c)
+
+
+## Problem 2
+
+Remember to indent all code by two spaces.
+
+\begin{code}
+module Problem2 where
+\end{code}
+
+### Infix declarations
+
+\begin{code}
+  infix  4 _⊢_
+  infix  4 _∋_
+  infixl 5 _,_
+
+  infixr 7 _⇒_
+
+  infix  5 ƛ_
+  infix  5 μ_
+  infixl 7 _·_
+  infix  8 `suc_
+  infix  9 `_
+  infix  9 S_
+  infix  9 #_ 
+\end{code}
+
+### Types and contexts
+
+\begin{code}
+  data Type : Set where
+    _⇒_   : Type → Type → Type
+    `ℕ    : Type
+
+  data Context : Set where
+    ∅   : Context
+    _,_ : Context → Type → Context
+\end{code}
+
+### Variables and the lookup judgment
+
+\begin{code}
+  data _∋_ : Context → Type → Set where
+
+    Z : ∀ {Γ A}
+        ----------
+      → Γ , A ∋ A
+
+    S_ : ∀ {Γ A B}
+      → Γ ∋ A
+        ---------
+      → Γ , B ∋ A
+\end{code}
+
+### Terms and the typing judgment
+
+\begin{code}
+  data _⊢_ : Context → Type → Set where
+
+    `_ : ∀ {Γ} {A}
+      → Γ ∋ A
+        ------
+      → Γ ⊢ A
+
+    ƛ_  :  ∀ {Γ} {A B}
+      → Γ , A ⊢ B
+        ----------
+      → Γ ⊢ A ⇒ B
+
+    _·_ : ∀ {Γ} {A B}
+      → Γ ⊢ A ⇒ B
+      → Γ ⊢ A
+        ----------
+      → Γ ⊢ B
+
+    `zero : ∀ {Γ}
+        ----------
+      → Γ ⊢ `ℕ
+
+    `suc_ : ∀ {Γ}
+      → Γ ⊢ `ℕ
+        -------
+      → Γ ⊢ `ℕ
+
+    case : ∀ {Γ A}
+      → Γ ⊢ `ℕ
+      → Γ ⊢ A
+      → Γ , `ℕ ⊢ A
+        -----------
+      → Γ ⊢ A
+
+    μ_ : ∀ {Γ A}
+      → Γ , A ⊢ A
+        ----------
+      → Γ ⊢ A
+\end{code}
+
+### Abbreviating de Bruijn indices
+
+\begin{code}
+  lookup : Context → ℕ → Type
+  lookup (Γ , A) zero     =  A
+  lookup (Γ , _) (suc n)  =  lookup Γ n
+  lookup ∅       _        =  ⊥-elim impossible
+    where postulate impossible : ⊥
+
+  count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n
+  count {Γ , _} zero     =  Z
+  count {Γ , _} (suc n)  =  S (count n)
+  count {∅}     _        =  ⊥-elim impossible
+    where postulate impossible : ⊥
+
+  #_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n
+  # n  =  ` count n
+\end{code}
+
+### Renaming
+
+\begin{code}
+  ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
+      -----------------------------------
+    → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
+  ext ρ Z      =  Z
+  ext ρ (S x)  =  S (ρ x)
+
+  rename : ∀ {Γ Δ}
+    → (∀ {A} → Γ ∋ A → Δ ∋ A)
+      ------------------------
+    → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+  rename ρ (` x)          =  ` (ρ x)
+  rename ρ (ƛ N)          =  ƛ (rename (ext ρ) N)
+  rename ρ (L · M)        =  (rename ρ L) · (rename ρ M)
+  rename ρ (`zero)        =  `zero
+  rename ρ (`suc M)       =  `suc (rename ρ M)
+  rename ρ (case L M N)   =  case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
+  rename ρ (μ N)          =  μ (rename (ext ρ) N)
+\end{code}
+
+### Simultaneous Substitution
+
+\begin{code}
+  exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A)
+      ----------------------------------
+    → (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
+  exts σ Z      =  ` Z
+  exts σ (S x)  =  rename S_ (σ x)
+
+  subst : ∀ {Γ Δ}
+    → (∀ {A} → Γ ∋ A → Δ ⊢ A)
+      ------------------------
+    → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
+  subst σ (` k)          =  σ k
+  subst σ (ƛ N)          =  ƛ (subst (exts σ) N)
+  subst σ (L · M)        =  (subst σ L) · (subst σ M)
+  subst σ (`zero)        =  `zero
+  subst σ (`suc M)       =  `suc (subst σ M)
+  subst σ (case L M N)   =  case (subst σ L) (subst σ M) (subst (exts σ) N)
+  subst σ (μ N)          =  μ (subst (exts σ) N)
+\end{code}
+
+### Single substitution
+
+\begin{code}
+  _[_] : ∀ {Γ A B}
+          → Γ , B ⊢ A
+          → Γ ⊢ B 
+            ---------
+          → Γ ⊢ A
+  _[_] {Γ} {A} {B} N M =  subst {Γ , B} {Γ} σ {A} N
+    where
+    σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A
+    σ Z      =  M
+    σ (S x)  =  ` x
+\end{code}
+
+### Values
+
+\begin{code}
+  data Value : ∀ {Γ A} → Γ ⊢ A → Set where
+
+    V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
+        ---------------------------
+      → Value (ƛ N)
+
+    V-zero : ∀ {Γ}
+        -----------------
+      → Value (`zero {Γ})
+
+    V-suc : ∀ {Γ} {V : Γ ⊢ `ℕ}
+      → Value V
+        --------------
+      → Value (`suc V)
+\end{code}
+
+### Reduction
+
+\begin{code}
+  infix 2 _—→_
+
+  data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+    ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
+      → L —→ L′
+        -----------------
+      → L · M —→ L′ · M
+
+    ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
+      → Value V
+      → M —→ M′
+        --------------
+      → V · M —→ V · M′
+
+    β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
+      → Value W
+        -------------------
+      → (ƛ N) · W —→ N [ W ]
+
+    ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
+      → M —→ M′
+        ----------------
+      → `suc M —→ `suc M′
+
+    ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+      → L —→ L′
+        --------------------------
+      → case L M N —→ case L′ M N
+
+    β-zero :  ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+        -------------------
+      → case `zero M N —→ M
+
+    β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
+      → Value V
+        -----------------------------
+      → case (`suc V) M N —→ N [ V ]
+
+    β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
+        ---------------
+      → μ N —→ N [ μ N ]
+\end{code}
+
+
+### Reflexive and transitive closure
+
+\begin{code}
+  infix  2 _—↠_
+  infix  1 begin_
+  infixr 2 _—→⟨_⟩_
+  infix  3 _∎
+
+  data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+
+    _∎ : ∀ {Γ A} (M : Γ ⊢ A)
+        --------
+      → M —↠ M
+
+    _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
+      → L —→ M
+      → M —↠ N
+        ---------
+      → L —↠ N
+
+  begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
+    → M —↠ N
+      ------
+    → M —↠ N
+  begin M—↠N = M—↠N
+\end{code}
+
+
+### Progress
+
+\begin{code}
+  data Progress {A} (M : ∅ ⊢ A) : Set where
+
+    step : ∀ {N : ∅ ⊢ A}
+      → M —→ N
+        -------------
+      → Progress M
+
+    done :
+        Value M
+        ----------
+      → Progress M
+
+  progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
+  progress (` ())
+  progress (ƛ N)                          =  done V-ƛ
+  progress (L · M) with progress L
+  ...    | step L—→L′                     =  step (ξ-·₁ L—→L′)
+  ...    | done V-ƛ with progress M
+  ...        | step M—→M′                 =  step (ξ-·₂ V-ƛ M—→M′)
+  ...        | done VM                    =  step (β-ƛ VM)
+  progress (`zero)                        =  done V-zero
+  progress (`suc M) with progress M
+  ...    | step M—→M′                     =  step (ξ-suc M—→M′)
+  ...    | done VM                        =  done (V-suc VM)
+  progress (case L M N) with progress L
+  ...    | step L—→L′                     =  step (ξ-case L—→L′)
+  ...    | done V-zero                    =  step (β-zero)
+  ...    | done (V-suc VL)                =  step (β-suc VL)
+  progress (μ N)                          =  step (β-μ)
+\end{code}
+
+### Evaluation
+
+\begin{code}
+  data Gas : Set where
+    gas : ℕ → Gas
+
+  data Finished {Γ A} (N : Γ ⊢ A) : Set where
+
+     done :
+         Value N
+         ----------
+       → Finished N
+
+     out-of-gas :
+         ----------
+         Finished N
+
+  data Steps : ∀ {A} → ∅ ⊢ A → Set where
+
+    steps : ∀ {A} {L N : ∅ ⊢ A}
+      → L —↠ N
+      → Finished N
+        ----------
+      → Steps L
+
+  eval : ∀ {A}
+    → Gas
+    → (L : ∅ ⊢ A)
+      -----------
+    → Steps L
+  eval (gas zero)    L                     =  steps (L ∎) out-of-gas
+  eval (gas (suc m)) L with progress L
+  ... | done VL                            =  steps (L ∎) (done VL)
+  ... | step {M} L—→M with eval (gas m) M
+  ...    | steps M—↠N fin                  =  steps (L —→⟨ L—→M ⟩ M—↠N) fin
+\end{code}
+
+## Problem 3
+
+Remember to indent all code by two spaces.
+
+\begin{code}
+module Problem3 where
+\end{code}
+
+### Imports
+
+\begin{code}
+  import plfa.DeBruijn as DB
+\end{code}
+
+### Syntax
+
+\begin{code}
+  infix   4  _∋_⦂_
+  infix   4  _⊢_↑_
+  infix   4  _⊢_↓_
+  infixl  5  _,_⦂_
+
+  infix   5  ƛ_⇒_
+  infix   5  μ_⇒_
+  infix   6  _↑
+  infix   6  _↓_
+  infixl  7  _·_
+  infix   8  `suc_
+  infix   9  `_
+\end{code}
+
+### Types
+
+\begin{code}
+  data Type : Set where
+    _⇒_   : Type → Type → Type
+    `ℕ    : Type
+\end{code}
+
+### Identifiers 
+
+\begin{code}
+  Id : Set
+  Id = String
+\end{code}
+
+### Contexts
+
+\begin{code}
+  data Context : Set where
+    ∅     : Context
+    _,_⦂_ : Context → Id → Type → Context
+\end{code}
+
+### Terms
+
+\begin{code}
+  data Term⁺ : Set
+  data Term⁻ : Set
+
+  data Term⁺ where
+    `_                        : Id → Term⁺
+    _·_                       : Term⁺ → Term⁻ → Term⁺
+    _↓_                       : Term⁻ → Type → Term⁺
+
+  data Term⁻ where
+    ƛ_⇒_                     : Id → Term⁻ → Term⁻
+    `zero                    : Term⁻
+    `suc_                    : Term⁻ → Term⁻
+    `case_[zero⇒_|suc_⇒_]    : Term⁺ → Term⁻ → Id → Term⁻ → Term⁻
+    μ_⇒_                     : Id → Term⁻ → Term⁻
+    _↑                       : Term⁺ → Term⁻
+\end{code}
+
+### Lookup 
+
+\begin{code}
+  data _∋_⦂_ : Context → Id → Type → Set where
+
+    Z : ∀ {Γ x A}
+        --------------------
+      → Γ , x ⦂ A ∋ x ⦂ A
+
+    S : ∀ {Γ x y A B}
+      → x ≢ y
+      → Γ ∋ x ⦂ A
+        -----------------
+      → Γ , y ⦂ B ∋ x ⦂ A
+\end{code}
+
+### Bidirectional type checking
+
+\begin{code}
+  data _⊢_↑_ : Context → Term⁺ → Type → Set
+  data _⊢_↓_ : Context → Term⁻ → Type → Set
+
+  data _⊢_↑_ where
+
+    ⊢` : ∀ {Γ A x}
+      → Γ ∋ x ⦂ A
+        -----------
+      → Γ ⊢ ` x ↑ A
+
+    _·_ : ∀ {Γ L M A B}
+      → Γ ⊢ L ↑ A ⇒ B
+      → Γ ⊢ M ↓ A
+        -------------
+      → Γ ⊢ L · M ↑ B
+
+    ⊢↓ : ∀ {Γ M A}
+      → Γ ⊢ M ↓ A
+        ---------------
+      → Γ ⊢ (M ↓ A) ↑ A
+
+  data _⊢_↓_ where
+
+    ⊢ƛ : ∀ {Γ x N A B}
+      → Γ , x ⦂ A ⊢ N ↓ B
+        -------------------
+      → Γ ⊢ ƛ x ⇒ N ↓ A ⇒ B
+
+    ⊢zero : ∀ {Γ}
+        --------------
+      → Γ ⊢ `zero ↓ `ℕ
+
+    ⊢suc : ∀ {Γ M}
+      → Γ ⊢ M ↓ `ℕ
+        ---------------
+      → Γ ⊢ `suc M ↓ `ℕ
+
+    ⊢case : ∀ {Γ L M x N A}
+      → Γ ⊢ L ↑ `ℕ
+      → Γ ⊢ M ↓ A
+      → Γ , x ⦂ `ℕ ⊢ N ↓ A
+        -------------------------------------
+      → Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ↓ A
+
+    ⊢μ : ∀ {Γ x N A}
+      → Γ , x ⦂ A ⊢ N ↓ A
+        -----------------
+      → Γ ⊢ μ x ⇒ N ↓ A
+
+    ⊢↑ : ∀ {Γ M A B}
+      → Γ ⊢ M ↑ A
+      → A ≡ B
+        -------------
+      → Γ ⊢ (M ↑) ↓ B
+\end{code}
+
+
+### Type equality
+
+\begin{code}
+  _≟Tp_ : (A B : Type) → Dec (A ≡ B)
+  `ℕ      ≟Tp `ℕ              =  yes refl
+  `ℕ      ≟Tp (A ⇒ B)         =  no λ()
+  (A ⇒ B) ≟Tp `ℕ              =  no λ()
+  (A ⇒ B) ≟Tp (A′ ⇒ B′)
+    with A ≟Tp A′ | B ≟Tp B′
+  ...  | no A≢    | _         =  no λ{refl → A≢ refl}
+  ...  | yes _    | no B≢     =  no λ{refl → B≢ refl}
+  ...  | yes refl | yes refl  =  yes refl
+\end{code}
+
+### Prerequisites
+
+\begin{code}
+  dom≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → A ≡ A′
+  dom≡ refl = refl
+
+  rng≡ : ∀ {A A′ B B′} → A ⇒ B ≡ A′ ⇒ B′ → B ≡ B′
+  rng≡ refl = refl
+
+  ℕ≢⇒ : ∀ {A B} → `ℕ ≢ A ⇒ B
+  ℕ≢⇒ ()
+\end{code}
+
+
+### Unique lookup
+
+\begin{code}
+  uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
+  uniq-∋ Z Z                 =  refl
+  uniq-∋ Z (S x≢y _)         =  ⊥-elim (x≢y refl)
+  uniq-∋ (S x≢y _) Z         =  ⊥-elim (x≢y refl)
+  uniq-∋ (S _ ∋x) (S _ ∋x′)  =  uniq-∋ ∋x ∋x′
+\end{code}
+
+### Unique synthesis
+
+\begin{code}
+  uniq-↑ : ∀ {Γ M A B} → Γ ⊢ M ↑ A → Γ ⊢ M ↑ B → A ≡ B
+  uniq-↑ (⊢` ∋x) (⊢` ∋x′)       =  uniq-∋ ∋x ∋x′
+  uniq-↑ (⊢L · ⊢M) (⊢L′ · ⊢M′)  =  rng≡ (uniq-↑ ⊢L ⊢L′)
+  uniq-↑ (⊢↓ ⊢M) (⊢↓ ⊢M′)       =  refl 
+\end{code}
+
+## Lookup type of a variable in the context
+
+\begin{code}
+  ext∋ : ∀ {Γ B x y}
+    → x ≢ y
+    → ¬ ∃[ A ]( Γ ∋ x ⦂ A )
+      -----------------------------
+    → ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
+  ext∋ x≢y _  ⟨ A , Z ⟩       =  x≢y refl
+  ext∋ _   ¬∃ ⟨ A , S _ ⊢x ⟩  =  ¬∃ ⟨ A , ⊢x ⟩
+
+  lookup : ∀ (Γ : Context) (x : Id)
+      -----------------------
+    → Dec (∃[ A ](Γ ∋ x ⦂ A))
+  lookup ∅ x                        =  no  (λ ())
+  lookup (Γ , y ⦂ B) x with x ≟ y
+  ... | yes refl                    =  yes ⟨ B , Z ⟩
+  ... | no x≢y with lookup Γ x
+  ...             | no  ¬∃          =  no  (ext∋ x≢y ¬∃)
+  ...             | yes ⟨ A , ⊢x ⟩  =  yes ⟨ A , S x≢y ⊢x ⟩
+\end{code}
+
+### Promoting negations
+
+\begin{code}
+  ¬arg : ∀ {Γ A B L M}
+    → Γ ⊢ L ↑ A ⇒ B
+    → ¬ Γ ⊢ M ↓ A
+      -------------------------
+    → ¬ ∃[ B′ ](Γ ⊢ L · M ↑ B′)
+  ¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
+
+  ¬switch : ∀ {Γ M A B}
+    → Γ ⊢ M ↑ A
+    → A ≢ B
+      ---------------
+    → ¬ Γ ⊢ (M ↑) ↓ B
+  ¬switch ⊢M A≢B (⊢↑ ⊢M′ A′≡B) rewrite uniq-↑ ⊢M ⊢M′ = A≢B A′≡B
+\end{code}
+
+
+## Synthesize and inherit types
+
+\begin{code}
+  synthesize : ∀ (Γ : Context) (M : Term⁺)
+      -----------------------
+    → Dec (∃[ A ](Γ ⊢ M ↑ A))
+
+  inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
+      ---------------
+    → Dec (Γ ⊢ M ↓ A)
+
+  synthesize Γ (` x) with lookup Γ x
+  ... | no  ¬∃              =  no  (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ })
+  ... | yes ⟨ A , ∋x ⟩      =  yes ⟨ A , ⊢` ∋x ⟩
+  synthesize Γ (L · M) with synthesize Γ L
+  ... | no  ¬∃              =  no  (λ{ ⟨ _ , ⊢L  · _  ⟩  →  ¬∃ ⟨ _ , ⊢L ⟩ })
+  ... | yes ⟨ `ℕ ,    ⊢L ⟩  =  no  (λ{ ⟨ _ , ⊢L′ · _  ⟩  →  ℕ≢⇒ (uniq-↑ ⊢L ⊢L′) })
+  ... | yes ⟨ A ⇒ B , ⊢L ⟩ with inherit Γ M A
+  ...    | no  ¬⊢M          =  no  (¬arg ⊢L ¬⊢M)
+  ...    | yes ⊢M           =  yes ⟨ B , ⊢L · ⊢M ⟩  
+  synthesize Γ (M ↓ A) with inherit Γ M A
+  ... | no  ¬⊢M             =  no  (λ{ ⟨ _ , ⊢↓ ⊢M ⟩  →  ¬⊢M ⊢M })
+  ... | yes ⊢M              =  yes ⟨ A , ⊢↓ ⊢M ⟩
+
+  inherit Γ (ƛ x ⇒ N) `ℕ      =  no  (λ())
+  inherit Γ (ƛ x ⇒ N) (A ⇒ B) with inherit (Γ , x ⦂ A) N B
+  ... | no ¬⊢N                =  no  (λ{ (⊢ƛ ⊢N)  →  ¬⊢N ⊢N })
+  ... | yes ⊢N                =  yes (⊢ƛ ⊢N)
+  inherit Γ `zero `ℕ          =  yes ⊢zero
+  inherit Γ `zero (A ⇒ B)     =  no  (λ())
+  inherit Γ (`suc M) `ℕ with inherit Γ M `ℕ
+  ... | no ¬⊢M                =  no  (λ{ (⊢suc ⊢M)  →  ¬⊢M ⊢M })
+  ... | yes ⊢M                =  yes (⊢suc ⊢M)
+  inherit Γ (`suc M) (A ⇒ B)  =  no  (λ())
+  inherit Γ (`case L [zero⇒ M |suc x ⇒ N ]) A with synthesize Γ L
+  ... | no ¬∃                 =  no  (λ{ (⊢case ⊢L  _ _) → ¬∃ ⟨ `ℕ , ⊢L ⟩})
+  ... | yes ⟨ _ ⇒ _ , ⊢L ⟩    =  no  (λ{ (⊢case ⊢L′ _ _) → ℕ≢⇒ (uniq-↑ ⊢L′ ⊢L) })   
+  ... | yes ⟨ `ℕ ,    ⊢L ⟩ with inherit Γ M A
+  ...    | no ¬⊢M             =  no  (λ{ (⊢case _ ⊢M _) → ¬⊢M ⊢M })
+  ...    | yes ⊢M with inherit (Γ , x ⦂ `ℕ) N A
+  ...       | no ¬⊢N          =  no  (λ{ (⊢case _ _ ⊢N) → ¬⊢N ⊢N })
+  ...       | yes ⊢N          =  yes (⊢case ⊢L ⊢M ⊢N)
+  inherit Γ (μ x ⇒ N) A with inherit (Γ , x ⦂ A) N A
+  ... | no ¬⊢N                =  no  (λ{ (⊢μ ⊢N) → ¬⊢N ⊢N })
+  ... | yes ⊢N                =  yes (⊢μ ⊢N)
+  inherit Γ (M ↑) B with synthesize Γ M
+  ... | no  ¬∃                =  no  (λ{ (⊢↑ ⊢M _) → ¬∃ ⟨ _ , ⊢M ⟩ })
+  ... | yes ⟨ A , ⊢M ⟩ with A ≟Tp B
+  ...   | no  A≢B             =  no  (¬switch ⊢M A≢B)
+  ...   | yes A≡B             =  yes (⊢↑ ⊢M A≡B)
+\end{code}
+
diff --git a/tspl/TSPL.lagda b/tspl/TSPL.lagda
new file mode 100644
index 00000000..2bb18594
--- /dev/null
+++ b/tspl/TSPL.lagda
@@ -0,0 +1,118 @@
+---
+title     : "TSPL: Course notes"
+layout    : page
+permalink : /TSPL/
+---
+
+## Staff
+
+* **Instructor**
+    [Philip Wadler](https://homepages.inf.ed.ac.uk/wadler)
+* **Teaching assistants**
+  - [Wen Kokke](mailto:wen.kokke@ed.ac.uk)
+  - [Chad Nester](mailto:chad.nester@gmail.com)
+
+## Lectures
+
+Lectures take place Monday, Wednesday, and Friday in AT 7.02. (Moved from AT 5.07 and AT 4.12.)
+* **9.00--9.50am** Lecture
+* **10.00--10.50am** Tutorial
+
+<table>
+ <tr>
+  <th>Week</th>
+  <th>Mon</th>
+  <th>Wed</th>
+  <th>Fri</th>
+ </tr>
+ <tr>
+  <td>1</td>
+  <td><b>17 Sep</b> <a href="/Naturals/">Naturals</a></td>
+  <td><b>19 Sep</b> <a href="/Induction/">Induction</a></td>
+  <td><b>21 Sep</b> <a href="/Induction/">Induction</a></td>
+ </tr>
+ <tr>
+  <td>2</td>
+  <td><b>24 Sep</b> <a href="/Relations/">Relations</a> (Chad)</td>
+  <td><b>26 Sep</b> <a href="/Relations/">Relations</a> (Chad)</td>
+  <td><b>28 Sep</b> (no class)</td>
+ </tr>
+ <tr>
+  <td>3</td>
+  <td><b>1 Oct</b> <a href="/Equality/">Equality</a> &amp; <a href="/Isomorphism/">Isomorphism</a></td>
+  <td><b>3 Oct</b> <a href="/Connectives/">Connectives</a></td>
+  <td><b>5 Oct</b> <a href="/Negation/">Negation</a></td>
+ </tr>
+ <tr>
+  <td>4</td>
+  <td><b>8 Oct</b> <a href="/Quantifiers/">Quantifiers</a></td>
+  <td><b>10 Oct</b> <a href="/Decidable/">Decidable</a></td>
+  <td><b>12 Oct</b> (tutorial only)</td>
+ </tr>
+ <tr>
+  <td>5</td>
+  <td><b>15 Oct</b> <a href="/Lists/">Lists</a></td>
+  <td><b>17 Oct</b> (tutorial only)</td>
+  <td><b>19 Oct</b> <a href="/Lists/">Lists</a></td>
+ </tr>
+ <tr>
+  <td>6</td>
+  <td><b>22 Oct</b> <a href="/Lambda/">Lambda</a></td>
+  <td><b>24 Oct</b> (no class)</td>
+  <td><b>26 Oct</b> <a href="/Properties/">Properties</a></td>
+ </tr>
+ <tr>
+  <td>7</td>
+  <td><b>29 Oct</b> <a href="/DeBruijn/">DeBruijn</a></td>
+  <td><b>31 Oct</b> <a href="/More/">More</a></td>
+  <td><b>2 Nov</b> <a href="/Inference/">Inference</a></td>
+ </tr>
+ <tr>
+  <td>8</td>
+  <td><b>5 Nov</b> (no class)</td>
+  <td><b>7 Nov</b> (tutorial only)</td>
+  <td><b>9 Nov</b> <a href="/Untyped/">Untyped</a></td>
+ </tr>
+ <tr>
+  <td>9</td>
+  <td><b>12 Nov</b> (no class)</td>
+  <td><b>14 Nov</b> (tutorial only)</td>
+  <td><b>16 Nov</b> (no class)</td>
+ </tr>
+ <tr>
+  <td>10</td>
+  <td><b>19 Nov</b> (no class)</td>
+  <td><b>21 Nov</b> Propositions as Types</td>
+  <td><b>23 Nov</b> (no class)</td>
+ </tr>
+ <tr>
+  <td>11</td>
+  <td><b>26 Nov</b> (no class)</td>
+  <td><b>28 Nov</b> Quantitative Type Theory (Wen)</td>
+  <td><b>30 Nov</b> (mock exam)</td>
+ </tr>
+</table>
+
+## Assignments
+
+For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/).
+
+* [Assignment 1][Assignment1] cw1 due 4pm Thursday 4 October (Week 3)
+* [Assignment 2][Assignment2] cw2 due 4pm Thursday 18 October (Week 5)
+* [Assignment 3][Assignment3] cw3 due 4pm Thursday 1 November (Week 7)
+* [Assignment 4][Assignment4] cw4 due 4pm Thursday 15 November (Week 9)
+* [Assignment 5](/tspl/Assignment5.pdf) cw5 due 4pm Thursday 22 November (Week 10)
+  <br />
+  Use file [Exam][Exam]. Despite the rubric, do **all three questions**.
+  
+
+Assignments are submitted by running
+``` bash
+submit tspl cwN AssignmentN.lagda
+```
+where N is the number of the assignment.
+
+## Mock exam
+
+Here is the text of the [mock](/tspl/mock.pdf)
+and the exam [instructions](/tspl/instructions.pdf).
diff --git a/tspl/examhons2018.cls b/tspl/examhons2018.cls
new file mode 100644
index 00000000..857d30ce
--- /dev/null
+++ b/tspl/examhons2018.cls
@@ -0,0 +1,1248 @@
+ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% I N F O R M A T I C S
+%  Honours Exam LaTeX Package v0.1
+%
+%  Created: 12-Oct-2009 by G.O.Passmore.
+%  Last Updated: 11-07-2017 by G.Hall
+%
+%  Note: We are changing the file and package name of this style
+%   from year to year, so as to make people aware of the version
+%   they are using.  The format is `examhons<YYYY>.sty' with <YYYY>
+%   replaced appropriately. 
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{examhons2016}[2009/10/12 v0.1 (GOP)]
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Set the ITO path for status.tex.
+%
+% * Note that course organisers / exam preparers do not need 
+%    status.tex.  When building their exam on their own machines, 
+%    the exam title / date / etc. information will be automatically
+%    filled-in with dummy values for mock-up purposes. 
+% 
+%    Once the exam document is processed on the ITO machines, 
+%    however, the mock-up exam title / date / etc. data will be 
+%    overwritten with the officially sanctioned data held in 
+%    the ITO's master status.tex file.
+%
+%  This file resides in the relative path below.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\itostatuspath{../exam-macros/}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Inherit the proper letter class.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\LoadClass[12pt,a4paper]{article}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% 
+% Take care of `page x of y' the proper way, based on a combination 
+%  of the J. Goldberg (lastpage) method, the C. Huggins (using fh)
+%  code, woven together with some use of the ifthen package for 
+%  branching on p0 (the exam title page, which shouldn't be num'd).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\RequirePackage{fancyhdr,ifthen,a4}
+\pagestyle{fancy}
+\fancyhf{}
+
+\def\lastpage@putlabel{\addtocounter{page}{-1}%
+   \immediate\write\@auxout{\string
+   \newlabel{LastPage}{{}{\thepage}}}%
+   \addtocounter{page}{1}}
+
+\AtEndDocument{%
+   \message{*** Setting LastPage: Make sure you 
+     run LaTeX upon your exam file at least 3
+     times to get this right.}%
+   \clearpage\lastpage@putlabel}%
+
+\newcommand{\totalpagesoverride}{0}
+
+ {\rfoot{\ifthenelse{\totalpagesoverride=0}
+          {\ifthenelse{\thepage>0}
+           {\scriptsize{Page \thepage{} of \pageref{LastPage}}}
+           {}}
+          {{\scriptsize{Page \thepage{} of \@forcedtotalpages}}}}}
+
+
+\renewcommand\headrulewidth{0pt}  
+
+\newcommand{\settotalpages}[1]{
+ \def\@forcedtotalpages{#1}
+ \renewcommand{\totalpagesoverride}{1}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Inlining of the EPSF package by Rokicki et al.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newread\epsffilein    % file to \read
+\newif\ifepsffileok    % continue looking for the bounding box?
+\newif\ifepsfbbfound   % success?
+\newif\ifepsfverbose   % report what you're making?
+\newif\ifepsfdraft     % use draft mode?
+\newdimen\epsfxsize    % horizontal size after scaling
+\newdimen\epsfysize    % vertical size after scaling
+\newdimen\epsftsize    % horizontal size before scaling
+\newdimen\epsfrsize    % vertical size before scaling
+\newdimen\epsftmp      % register for arithmetic manipulation
+\newdimen\pspoints     % conversion factor
+%
+\pspoints=1bp          % Adobe points are `big'
+\epsfxsize=0pt         % Default value, means `use natural size'
+\epsfysize=0pt         % ditto
+%
+\def\epsfbox#1{\global\def\epsfllx{72}\global\def\epsflly{72}%
+   \global\def\epsfurx{540}\global\def\epsfury{720}%
+   \def\lbracket{[}\def\testit{#1}\ifx\testit\lbracket
+   \let\next=\epsfgetlitbb\else\let\next=\epsfnormal\fi\next{#1}}%
+%
+\def\epsfgetlitbb#1#2 #3 #4 #5]#6{\epsfgrab #2 #3 #4 #5 .\\%
+   \epsfsetgraph{#6}}%
+%
+\def\epsfnormal#1{\epsfgetbb{#1}\epsfsetgraph{#1}}%
+%
+\def\epsfgetbb#1{%
+%
+%   The first thing we need to do is to open the
+%   PostScript file, if possible.
+%
+\openin\epsffilein=#1
+\ifeof\epsffilein\errmessage{I couldn't open #1, will ignore it}\else
+%
+%   Okay, we got it. Now we'll scan lines until we find one that doesn't
+%   start with %. We're looking for the bounding box comment.
+%
+   {\epsffileoktrue \chardef\other=12
+    \def\do##1{\catcode`##1=\other}\dospecials \catcode`\ =10
+    \loop
+       \read\epsffilein to \epsffileline
+       \ifeof\epsffilein\epsffileokfalse\else
+%
+%   We check to see if the first character is a % sign;
+%   if not, we stop reading (unless the line was entirely blank);
+%   if so, we look further and stop only if the line begins with
+%   `%%BoundingBox:'.
+%
+          \expandafter\epsfaux\epsffileline:. \\%
+       \fi
+   \ifepsffileok\repeat
+   \ifepsfbbfound\else
+    \ifepsfverbose\message{No bounding box comment in #1; using defaults}\fi\fi
+   }\closein\epsffilein\fi}%
+%
+%   Now we have to calculate the scale and offset values to use.
+%   First we compute the natural sizes.
+%
+\def\epsfclipon{\def\epsfclipstring{ clip}}%
+\def\epsfclipoff{\def\epsfclipstring{\ifepsfdraft\space clip\fi}}%
+\epsfclipoff
+%
+\def\epsfsetgraph#1{%
+   \epsfrsize=\epsfury\pspoints
+   \advance\epsfrsize by-\epsflly\pspoints
+   \epsftsize=\epsfurx\pspoints
+   \advance\epsftsize by-\epsfllx\pspoints
+%
+%   If `epsfxsize' is 0, we default to the natural size of the picture.
+%   Otherwise we scale the graph to be \epsfxsize wide.
+%
+   \epsfxsize\epsfsize\epsftsize\epsfrsize
+   \ifnum\epsfxsize=0 \ifnum\epsfysize=0
+      \epsfxsize=\epsftsize \epsfysize=\epsfrsize
+      \epsfrsize=0pt
+%
+%   We have a sticky problem here:  TeX doesn't do floating point arithmetic!
+%   Our goal is to compute y = rx/t. The following loop does this reasonably
+%   fast, with an error of at most about 16 sp (about 1/4000 pt).
+% 
+     \else\epsftmp=\epsftsize \divide\epsftmp\epsfrsize
+       \epsfxsize=\epsfysize \multiply\epsfxsize\epsftmp
+       \multiply\epsftmp\epsfrsize \advance\epsftsize-\epsftmp
+       \epsftmp=\epsfysize
+       \loop \advance\epsftsize\epsftsize \divide\epsftmp 2
+       \ifnum\epsftmp>0
+          \ifnum\epsftsize<\epsfrsize\else
+             \advance\epsftsize-\epsfrsize \advance\epsfxsize\epsftmp \fi
+       \repeat
+       \epsfrsize=0pt
+     \fi
+   \else \ifnum\epsfysize=0
+     \epsftmp=\epsfrsize \divide\epsftmp\epsftsize
+     \epsfysize=\epsfxsize \multiply\epsfysize\epsftmp   
+     \multiply\epsftmp\epsftsize \advance\epsfrsize-\epsftmp
+     \epsftmp=\epsfxsize
+     \loop \advance\epsfrsize\epsfrsize \divide\epsftmp 2
+     \ifnum\epsftmp>0
+        \ifnum\epsfrsize<\epsftsize\else
+           \advance\epsfrsize-\epsftsize \advance\epsfysize\epsftmp \fi
+     \repeat
+     \epsfrsize=0pt
+    \else
+     \epsfrsize=\epsfysize
+    \fi
+   \fi
+%
+%  Finally, we make the vbox and stick in a \special that dvips can parse.
+%
+   \ifepsfverbose\message{#1: width=\the\epsfxsize, height=\the\epsfysize}\fi
+   \epsftmp=10\epsfxsize \divide\epsftmp\pspoints
+   \vbox to\epsfysize{\vfil\hbox to\epsfxsize{%
+      \ifnum\epsfrsize=0\relax
+        \special{PSfile=\ifepsfdraft psdraft.ps\else#1\fi\space
+             llx=\epsfllx\space lly=\epsflly\space
+             urx=\epsfurx\space ury=\epsfury\space rwi=\number\epsftmp
+             \epsfclipstring}%
+      \else
+        \epsfrsize=10\epsfysize \divide\epsfrsize\pspoints
+        \special{PSfile=\ifepsfdraft psdraft.ps\else#1\fi\space
+             llx=\epsfllx\space lly=\epsflly\space
+             urx=\epsfurx\space ury=\epsfury\space rwi=\number\epsftmp\space
+             rhi=\number\epsfrsize \epsfclipstring}%
+      \fi
+      \hfil}}%
+\global\epsfxsize=0pt\global\epsfysize=0pt}%
+%
+%   We still need to define the tricky \epsfaux macro. This requires
+%   a couple of magic constants for comparison purposes.
+%
+{\catcode`\%=12 \global\let\epsfpercent=%\global\def\epsfbblit{%BoundingBox}}%
+%
+%   So we're ready to check for `%BoundingBox:' and to grab the
+%   values if they are found.
+%
+\long\def\epsfaux#1#2:#3\\{\ifx#1\epsfpercent
+   \def\testit{#2}\ifx\testit\epsfbblit
+      \epsfgrab #3 . . . \\%
+      \epsffileokfalse
+      \global\epsfbbfoundtrue
+   \fi\else\ifx#1\par\else\epsffileokfalse\fi\fi}%
+%
+%   Here we grab the values and stuff them in the appropriate definitions.
+%
+\def\epsfempty{}%
+\def\epsfgrab #1 #2 #3 #4 #5\\{%
+\global\def\epsfllx{#1}\ifx\epsfllx\epsfempty
+      \epsfgrab #2 #3 #4 #5 .\\\else
+   \global\def\epsflly{#2}%
+   \global\def\epsfurx{#3}\global\def\epsfury{#4}\fi}%
+%
+%   We default the epsfsize macro.
+%
+\def\epsfsize#1#2{\epsfxsize}
+%
+%   Finally, another definition for compatibility with older macros.
+%
+\let\epsffile=\epsfbox
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Inlining of the UK date package by A. Clark.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\@cent{\count0 }                      
+\def\@diy{\count1 }                        
+\def\@dow{\count2 }                        
+\def\@epact{\count3 }                      
+\def\@golden{\count4 }                     
+\def\@leap{\count5 }                       
+\def\@x{\count6 }                          
+\def\@y{\count7 }                          
+
+\def\@up#1{{\@savestyle\thinspace$^{\underline{\hbox{%
+  \scriptsize\@setstyle#1\fam=-1 }}}$}}
+\def\st{\@up{st}}
+\def\nd{\@up{nd}}
+\def\rd{\@up{rd}}
+\def\th{\@up{th}}
+
+\def\@savestyle{\count0=\the\fam}
+\def\@setstyle{\ifcase\count0\rm\or\mit\or\cal\or\rm
+  \or\it\or\sl\or\bf\or\tt\fi}
+
+\def\today{\dayofweek{} \number\day\ifcase\day
+  \or\st\or\nd\or\rd\or\th\or\th\or\th\or\th\or\th\or\th\or\th
+  \or\th\or\th\or\th\or\th\or\th\or\th\or\th\or\th\or\th\or\th
+  \or\st\or\nd\or\rd\or\th\or\th\or\th\or\th\or\th\or\th\or\th\or\st\fi
+  \space\ifcase\month\or January\or February\or March\or April\or May\or
+  June\or July\or August\or September\or October\or November\or December\fi
+  \space\number\year}
+
+\def\dayofweek{{%
+  \@leap=\month \advance\@leap by -14 \divide\@leap by 12
+  \advance\@leap by \year
+  \@dow=\month \advance\@dow by 10
+  \@y=\@dow \divide\@y by 13 \multiply\@y by 12
+  \advance\@dow by -\@y \multiply\@dow by 13 
+  \advance\@dow by -1 \divide\@dow by 5
+  \advance\@dow by \day \advance\@dow by 77
+  \@x=\@leap \@y=\@x \divide\@y by 100 \multiply\@y by 100 \advance\@x by -\@y
+  \multiply\@x by 5 \divide\@x by 4 \advance\@dow by \@x
+  \@x=\@leap \divide\@x by 400 \advance\@dow by \@x
+  \@x=\@leap \divide\@x by 100 \multiply\@x by 2 \advance\@dow by -\@x
+  \@x=\@dow \divide\@x by 7 \multiply\@x by 7 \advance\@dow by -\@x
+  \ifcase\@dow Sunday\or Monday\or Tuesday\or Wednesday\or
+      Thursday\or Friday\or Saturday\fi}}
+\def\phaseofmoon{{%
+  \@diy=\day \advance\@diy by \ifcase\month            
+      -1\or -1\or 30\or 58\or 89\or 119\or 150\or      
+      180\or 211\or 241\or 272\or 303\or 333\fi        
+  \ifnum \month>2
+    \@x=\year \@y=\@x \divide\@y by 4 \multiply\@y by 4 \advance\@x by -\@y
+    \ifnum \@x=0                    
+      \@x=\year \@y=\@x \divide\@y by 400 
+      \multiply\@y by 400 \advance\@x by -\@y
+      \ifnum \@x=0                  
+      \advance\@diy by 1            
+      \else                         
+      \@x=\year \@y=\@x \divide\@y by 100 
+      \multiply\@y by 100 \advance\@x by -\@y
+      \ifnum \@x>0                  
+          \advance\@diy by 1        
+      \fi                           
+      \fi                           
+    \fi                             
+  \fi                               
+  \@cent=\year \divide\@cent by 100 \advance\@cent by 1
+  \@golden=\year
+  \@y=\year \divide\@y by 19 \multiply\@y by 19 \advance\@golden by -\@y
+  \advance\@golden by 1
+  \@epact=11 \multiply\@epact by \@golden
+  \advance\@epact by 20
+  \@x=8 \multiply\@x by \@cent \advance\@x by 5
+  \divide\@x by 25 \advance\@x by -5
+  \advance\@epact by \@x
+  \@x=3 \multiply\@x by \@cent \divide\@x by 4 \advance\@x by -12
+  \advance\@epact by -\@x
+  \@y=\@epact \divide\@y by 30 \multiply\@y by 30 \advance\@epact by -\@y
+  \ifnum \@epact<0
+    \advance\@epact by 30
+  \fi
+  \ifnum \@epact=25
+    \ifnum \@golden>11
+      \advance \@epact by 1
+    \fi
+  \else
+    \ifnum \@epact=24
+      \advance \@epact by 1
+    \fi
+  \fi
+  \@x=\@diy \advance\@x by \@epact \multiply\@x by 6 \advance\@x by 11
+  \@y=\@x \divide\@y by 177 \multiply\@y by 177 \advance\@x by -\@y
+  \divide\@x by 22
+  \ifcase\@x new\or waxing crescent\or in its first quarter\or
+      waxing gibbous\or full\or waning gibbous\or
+      in its last quarter\or waning crescent\or new\fi}}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Now, we want to define commands for exam title, time, conveners,
+%  and so on, *but* we want to provide hard-coded dummy values
+%  for exam preparers who are working on their own machines.
+%  This is so that status.tex does not need to be ever copied from
+%  the ITO installation; it is only for ITO.  
+%
+% The logic here is simple.  If we find \itostatuspath status.tex
+%  to exist, then we populate the values of exam title, time, and
+%  so on using those it contains corresponding to \courseid, which
+%  is set by the exam preparer using the \setcourse command.
+%  This is done internally by executing a command named 
+%  \<courseid>details, with <courseid> replaced by their courseid.
+%
+% Otherwise, we use dummy values, but we've gone to the effort to
+%  at least include the correct course title and type (Inf3,MSc,..)
+%  within these mock values so as to keep the preparer happy ;-).
+%
+% Once that's done, we need to work out the rubric.  The rubric
+%  is printed on the title page and is set by the exam author
+%  using the \setrubric command.  They have the following options:
+%
+%   {qu1_and_either_qu2_or_qu3, any_two_of_three, custom}.
+%
+% Again, the usage of this information follows the same structure
+%  as above.  On an ITO machine, the master files are sourced from
+%  the itostatuspath directory.  On an exam preparer's machine,
+%  we generate mock-up values for the rubric form and type.
+%
+% Note, if they create a custom rubric, they must then execute:
+%
+%  \setrubricform{} and \setrubrictype to specify the custom
+%   rubric information.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\coursestatusfcn}{}
+\newcommand{\courseid}{}
+\newcommand{\rubricid}{}
+\newcommand{\rubricform}{}
+\newcommand{\rubrictype}{}
+
+\providecommand{\status}{}
+
+\newcommand{\setcourse}[1]{
+ \renewcommand{\courseid}{#1}
+}
+
+\newcommand{\setrubric}[1]{\renewcommand{\rubricid}{#1}}
+\newcommand{\setrubricform}[1]{\renewcommand{\rubricform}{#1}}
+\newcommand{\setrubrictype}[1]{\renewcommand{\rubrictype}{#1}}
+
+\AtBeginDocument{
+ \newcounter{Day}   \setcounter{Day}{\day}
+ \newcounter{Month} \setcounter{Month}{\month}
+ \newcounter{Year}  \setcounter{Year}{\year}
+}
+
+\newenvironment{hint}{\par[{\bf Hint:} }{\nolinebreak]}
+\newenvironment{hints}{\par[{\bf Hints:} }{\nolinebreak]}
+\newenvironment{note}{\par[{\bf Note:} }{\nolinebreak]}
+\newenvironment{notes}{\par[{\bf Notes:} }{\nolinebreak]}
+
+\def\ps@header{\let\@mkboth\@gobbletwo
+     \let\@oddfoot\@empty\let\@evenhead\@empty\let\@evenfoot\@oddfoot}
+\def\setstatus#1{\def\@status{#1}}
+\def\@status{}
+\def\@nextone{f}\def\@nextbutone{f}%
+\def\@oddhead{{\bf\it \@status}\hfil\it\@conthead}
+\def\@conthead{\if\@nextone t\relax QUESTION CONTINUED FROM PREVIOUS PAGE\fi\xdef\@nextone{\@nextbutone}\gdef\@nextbutone{f}}
+\def\continued{%
+\gdef\@nextbutone{t}
+\par\rightline{\it QUESTION CONTINUES ON NEXT PAGE}\newpage%
+}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Display the exam status (for `internal'/`external' scrutiny, or 
+%  `final' which will print no corresponding notice).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\internal{
+  \setstatus{\it FOR INTERNAL SCRUTINY (date of this version: \theDay/\theMonth/\theYear)}}
+\def\external{
+  \setstatus{\it FOR EXTERNAL EXAMINER (date of this version: \theDay/\theMonth/\theYear)}}
+\def\final{\setstatus{}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Setup the proper marks displays.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\Marks#1#2{\marginpar{\raisebox{#2\baselineskip}{[{\it #1 
+  \ifnum #1=1 mark\else marks\fi\/}]}}}
+%Version for most situations.
+\def\marks#1{\Marks{#1}{0}}
+% The next version is to get around the problem that you cannot put a 
+% marginpar in maths display.  Put \marksl just before the display line.
+\def\marksd#1{\Marks{#1}{-2}}
+% As above but raises the box.
+\def\marksu#1{\Marks{#1}{1}}
+
+\leftmargini=0pt
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% EPS macros by KK.
+%
+% The first argument is the filename and the second the size (of the 
+%  x-axis or the y-axis respectively.  
+%
+% For example \psfigx{graph1.epsf}{5in} will input your first graph 
+%  and make the x-axis equal to 4.5in, with the y-axis appropriately
+%  scaled.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\psfigx#1#2{
+  \begin{center}
+     \leavevmode
+     \epsfxsize=#2
+     \epsffile{#1}
+   \end{center}}
+   
+\def\psfigy#1#2{
+  \begin{center}
+     \leavevmode
+     \epsfysize=#2
+     \epsffile{#1}
+   \end{center}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Commands for manipulating exam course data.
+%
+% We will use them to assign dummy values on exam preparer machines,
+%  and otherwise will source the master ITO status.tex if it exists
+%  (e.g., when we are compiling on an ITO machine).
+%
+% Also, the papertype.inc files and rubric.inc files will be 
+%  loaded if we are on an ITO machine.  Otherwise, we will provide
+%  dummy mock-up values for those as well.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand\papertitle[1]{\global\def\nameofpaper{\uppercase{#1}}}
+\newcommand\papertype[1]{\global\def\typeofpaper{
+ \InputIfFileExists{\itostatuspath #1}{}
+  { 
+    %
+    % If we're here, then this is running on exam preparer's
+    % machine.  So, we will use mock-up values for the exam
+    % type text corresponding to #1.
+    %
+    % Options for #1 are {msc.inc, inf4msc.inc, inf3.inc, inf4.inc,
+    %                     nonhons.inc}.
+    %
+
+   \ifthenelse{\equal{#1}{msc.inc}}
+     {MSc Courses
+       \vskip 0.1in
+      Convener: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine}{}
+   \ifthenelse{\equal{#1}{inf4msc.inc}}
+     {Year 4 Courses
+       \vskip 0.1in
+      Convener: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine
+       \vskip 0.5in
+      MSc Courses
+       \vskip 0.1in
+      Convener: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine}{}
+   \ifthenelse{\equal{#1}{inf3inf4.inc}}
+     {Year 3 Courses
+       \vskip 0.1in
+      Convenor: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine
+       \vskip 0.5in
+      Year 4 Courses
+       \vskip 0.1in
+      Convener: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine}{}
+   \ifthenelse{\equal{#1}{inf3.inc}}
+     {Year 3 Courses
+       \vskip 0.1in
+      Convener: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine}{}
+   \ifthenelse{\equal{#1}{inf4.inc}}
+     {Year 4 Courses
+       \vskip 0.1in
+      Convener: ITO-Will-Determine\\
+      External Examiners: ITO-Will-Determine}{}
+   \ifthenelse{\equal{#1}{nonhons}}
+     {\vskip 0.2in
+      Convener: ITO-Will-Determine\\
+      External Examiner: ITO-Will-Determine}{}}}}
+
+\newcommand{\paperdate}[3]{\global\def\day{#1}\global\def\month{#2}\global\def\year{#3}}
+\newcommand{\papertimes}[2]{\global\def\timeofpaper{#1 to #2}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Now, we first see if we're on an ITO machine and can load the 
+%  proper status.tex.  If so, we do it and execute the corresponding
+%  \coursestatusfcn.  
+%
+% Otherwise, based upon the value of courseid, we need to populate  
+%  the title and type with basic mock-up data.
+%
+% This command must be called in the top-level exam document, after
+%  the courseid has been set.
+%
+% To do so: \initcoursedata
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\newcommand{\initcoursedata}{
+ \IfFileExists{\itostatuspath status.tex}
+  {
+   %
+   % If we're here, then we're on an ITO machine.
+   %
+
+   \input{\itostatuspath status.tex}
+
+   %
+   % We've loaded status.tex properly then, and can now execute
+   %  the corresponding \XXXdetails command.
+   %
+
+    \ifthenelse{\equal{\courseid}{anlp}}
+      {\anlpdetails}{}
+    \ifthenelse{\equal{\courseid}{aleone}} 
+      {\aleonedetails}{}
+	\ifthenelse{\equal{\courseid}{adbs}} 
+      {\adbsdetails}{}
+    \ifthenelse{\equal{\courseid}{av}}
+      {\avdetails}{}
+	\ifthenelse{\equal{\courseid}{apl}}
+      {\apldetails}{}
+    \ifthenelse{\equal{\courseid}{abs}}
+      {\absdetails}{}
+    \ifthenelse{\equal{\courseid}{agta}}
+      {\agtadetails}{}
+    \ifthenelse{\equal{\courseid}{ads}}
+      {\adsdetails}{}
+	\ifthenelse{\equal{\courseid}{ad}}
+	  {\addetails}{}
+    \ifthenelse{\equal{\courseid}{ar}}
+      {\ardetails}{}
+    \ifthenelse{\equal{\courseid}{asr}}
+      {\asrdetails}{}
+    \ifthenelse{\equal{\courseid}{bioone}}
+      {\bioonedetails}{}
+    \ifthenelse{\equal{\courseid}{biotwo}}
+      {\biotwodetails}{}
+    \ifthenelse{\equal{\courseid}{bdl}}
+      {\bdldetails}{}
+	 \ifthenelse{\equal{\courseid}{cqi}}
+      {\cqidetails}{}
+    \ifthenelse{\equal{\courseid}{copt}}
+      {\coptdetails}{}
+    \ifthenelse{\equal{\courseid}{ct}}
+      {\ctdetails}{}
+    \ifthenelse{\equal{\courseid}{ccs}}
+      {\ccsdetails}{}
+    \ifthenelse{\equal{\courseid}{cmc}}
+      {\cmcdetails}{}
+    \ifthenelse{\equal{\courseid}{ca}}
+      {\cadetails}{}
+    \ifthenelse{\equal{\courseid}{cav}}
+      {\cavdetails}{}
+    \ifthenelse{\equal{\courseid}{car}}
+      {\cardetails}{}
+    \ifthenelse{\equal{\courseid}{comn}}
+      {\comndetails}{}
+    \ifthenelse{\equal{\courseid}{cd}}
+      {\cddetails}{}
+    \ifthenelse{\equal{\courseid}{cg}}
+      {\cgdetails}{}
+    \ifthenelse{\equal{\courseid}{cn}}
+      {\cndetails}{}
+    \ifthenelse{\equal{\courseid}{cp}}
+      {\cpdetails}{}
+    \ifthenelse{\equal{\courseid}{cs}}
+      {\csdetails}{}
+	\ifthenelse{\equal{\courseid}{dme}}
+	  {\dmedetails}{}
+	\ifthenelse{\equal{\courseid}{dds}}
+	  {\ddsdetails}{}
+    \ifthenelse{\equal{\courseid}{dbs}}
+      {\dbsdetails}{}
+    \ifthenelse{\equal{\courseid}{dmmr}}
+      {\dmmrdetails}{}
+    \ifthenelse{\equal{\courseid}{dmr}}
+      {\dmrdetails}{}	  
+    \ifthenelse{\equal{\courseid}{ds}}
+      {\dsdetails}{}
+	\ifthenelse{\equal{\courseid}{epl}}
+	  {\epldetails}{}
+    \ifthenelse{\equal{\courseid}{es}}
+      {\esdetails}{}
+    \ifthenelse{\equal{\courseid}{exc}}
+      {\excdetails}{}
+    \ifthenelse{\equal{\courseid}{fv}}
+      {\fvdetails}{}
+    \ifthenelse{\equal{\courseid}{fnlp}}
+      {\fnlpdetails}{}
+    \ifthenelse{\equal{\courseid}{hci}}
+      {\hcidetails}{}
+    \ifthenelse{\equal{\courseid}{infonecg}}
+      {\infonecgdetails}{}
+    \ifthenelse{\equal{\courseid}{infonecl}}
+      {\infonecldetails}{}
+    \ifthenelse{\equal{\courseid}{infoneda}}
+      {\infonedadetails}{}
+    \ifthenelse{\equal{\courseid}{infonefp}}
+      {\infonefpdetails}{}
+    \ifthenelse{\equal{\courseid}{infonefpam}}
+      {\infonefpamdetails}{}
+    \ifthenelse{\equal{\courseid}{infonefppm}}
+      {\infonefppmdetails}{}
+    \ifthenelse{\equal{\courseid}{infoneop}}
+      {\infoneopdetails}{}
+    \ifthenelse{\equal{\courseid}{infoneopam}}
+      {\infoneopamdetails}{}
+    \ifthenelse{\equal{\courseid}{infoneoppm}}
+      {\infoneoppmdetails}{}
+    \ifthenelse{\equal{\courseid}{inftwoa}}
+      {\inftwoadetails}{}
+    \ifthenelse{\equal{\courseid}{inftwob}}
+      {\inftwobdetails}{}
+    \ifthenelse{\equal{\courseid}{inftwoccs}}
+      {\inftwoccsdetails}{}
+    \ifthenelse{\equal{\courseid}{inftwocse}}
+      {\inftwocsedetails}{}
+    \ifthenelse{\equal{\courseid}{inftwod}}
+      {\inftwoddetails}{}
+    \ifthenelse{\equal{\courseid}{iar}}
+      {\iardetails}{}
+    \ifthenelse{\equal{\courseid}{imc}}
+      {\imcdetails}{}
+    \ifthenelse{\equal{\courseid}{iotssc}}
+      {\iotsscdetails}{}	  
+    \ifthenelse{\equal{\courseid}{iqc}}
+      {\iqcdetails}{}
+    \ifthenelse{\equal{\courseid}{itcs}}
+      {\itcsdetails}{}
+    \ifthenelse{\equal{\courseid}{ivc}}
+      {\ivcdetails}{}	  
+    \ifthenelse{\equal{\courseid}{ivr}}
+      {\ivrdetails}{}
+    \ifthenelse{\equal{\courseid}{iaml}}
+      {\iamldetails}{}
+    \ifthenelse{\equal{\courseid}{lpt}}
+      {\lptdetails}{}
+    \ifthenelse{\equal{\courseid}{lpp}}
+      {\lppdetails}{}
+    \ifthenelse{\equal{\courseid}{mlpr}}
+      {\mlprdetails}{}
+    \ifthenelse{\equal{\courseid}{mt}}
+      {\mtdetails}{}
+	\ifthenelse{\equal{\courseid}{mi}}
+	  {\midetails}{}
+    \ifthenelse{\equal{\courseid}{nlu}} 
+      {\nludetails}{}
+    \ifthenelse{\equal{\courseid}{nc}} 
+      {\ncdetails}{}
+    \ifthenelse{\equal{\courseid}{nip}}
+      {\nipdetails}{}
+    \ifthenelse{\equal{\courseid}{os}}
+      {\osdetails}{}
+    \ifthenelse{\equal{\courseid}{pa}}
+      {\padetails}{}
+    \ifthenelse{\equal{\courseid}{pdiot}}
+      {\pdiotdetails}{}	  
+    \ifthenelse{\equal{\courseid}{ppls}}
+      {\pplsdetails}{}
+    \ifthenelse{\equal{\courseid}{pm}}
+      {\pmdetails}{}
+    \ifthenelse{\equal{\courseid}{pmr}}
+      {\pmrdetails}{}
+    \ifthenelse{\equal{\courseid}{pi}}
+      {\pidetails}{}
+    \ifthenelse{\equal{\courseid}{rc}}
+      {\rcdetails}{}
+    \ifthenelse{\equal{\courseid}{rl}}
+      {\rldetails}{}
+    \ifthenelse{\equal{\courseid}{rlsc}}
+      {\rlscdetails}{}
+    \ifthenelse{\equal{\courseid}{rss}}
+      {\rssdetails}{}
+	\ifthenelse{\equal{\courseid}{sp}}
+	  {\spdetails}{}
+    \ifthenelse{\equal{\courseid}{sws}}
+      {\swsdetails}{}
+	\ifthenelse{\equal{\courseid}{stn}}
+	  {\stndetails}{}
+    \ifthenelse{\equal{\courseid}{sapm}}
+      {\sapmdetails}{}
+    \ifthenelse{\equal{\courseid}{sdm}}
+      {\sdmdetails}{}
+    \ifthenelse{\equal{\courseid}{st}}
+      {\stdetails}{}
+    \ifthenelse{\equal{\courseid}{ttds}}
+      {\ttdsdetails}{}
+    \ifthenelse{\equal{\courseid}{tspl}}
+      {\tspldetails}{}
+
+  }
+  { 
+   %
+   % If we're here, then we're on an exam preparer's machine.
+   % So, we're going to use their set \courseid to give some
+   %  nice mock-up values to the title and type text.
+   %
+  
+    \ifthenelse{\equal{\courseid}{anlp}}
+      {\papertitle{INFR 11125 Accelerated Natural Language Processing}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{aleone}}
+      {\papertitle{Adaptive Learning Environments (Level 11)}
+       \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{adbs}}
+      {\papertitle{Advanced Databases}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{av}}
+      {\papertitle{Advanced Vision (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{apl}}
+      {\papertitle{Advances in Programming Languages}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{abs}}
+      {\papertitle{Agent Based Systems}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{agta}}
+      {\papertitle{Algorithmic Game Theory and its Applications}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{ads}}
+      {\papertitle{Algorithms and Data Structures}
+       \papertype{inf3.inc}}{}
+	\ifthenelse{\equal{\courseid}{ad}}
+	  {\papertitle{INFR11015 Applied Databases}
+	   \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{ar}}
+      {\papertitle{Automated Reasoning (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{asr}}
+      {\papertitle{Automatic Speech Recognition}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{bioone}}
+      {\papertitle{Bioinformatics 1}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{biotwo}}
+      {\papertitle{Bioinformatics 2}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{bdl}}
+      {\papertitle{INFR11144 Blockchains and Distributed Ledgers}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{cqi}}
+      {\papertitle{Categories and Quantum Informatics}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{copt}}
+      {\papertitle{Compiler Optimisation (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{ct}}
+      {\papertitle{Compiling Techniques}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{ccs}}
+      {\papertitle{Computational Cognitive Science}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{cmc}}
+      {\papertitle{Computational Complexity}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{ca}}
+      {\papertitle{Computer Algebra}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{cav}}
+      {\papertitle{Computer Animation and Visualisation (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{car}}
+      {\papertitle{Computer Architecture}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{comn}}
+      {\papertitle{Computer Communications and Networks}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{cd}}
+      {\papertitle{Computer Design}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{cg}}
+      {\papertitle{Computer Graphics (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{cn}}
+      {\papertitle{Computer Networking (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{cp}}
+      {\papertitle{Computer Programming Skills and Concepts}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{cs}}
+      {\papertitle{Computer Security}
+       \papertype{inf3.inc}}{}
+	\ifthenelse{\equal{\courseid}{dds}}
+	  {\papertitle{INFR08024 Data, Design and Society}
+	   \papertype{nonhons.inc}}{}
+	\ifthenelse{\equal{\courseid}{dme}}
+	  {\papertitle{Data Mining and Exploration}
+	   \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{dbs}}
+      {\papertitle{Database Systems}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{dmr}}
+      {\papertitle{Decision Making in Robots and Autonomous Agents}
+       \papertype{nonhons.inc}}{}	   
+    \ifthenelse{\equal{\courseid}{dmmr}}
+      {\papertitle{Discrete Mathematics and Mathematical Reasoning}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{ds}}
+      {\papertitle{Distributed Systems (Level 11)}
+       \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{epl}}
+	  {\papertitle{INFR10061 Elements of Programming Languages}
+	   \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{es}}
+      {\papertitle{Embedded Software}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{exc}}
+      {\papertitle{Extreme Computing}
+       \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{fv}}
+      {\papertitle{Formal Verification}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{fnlp}}
+      {\papertitle{Foundations of Natural Language Processing}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{hci}}
+      {\papertitle{Human-Computer Interaction (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{infonecg}}
+      {\papertitle{Informatics 1 --- Cognitive Science}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infonecl}}
+      {\papertitle{Informatics 1 --- Computation \& Logic}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infoneda}}
+      {\papertitle{Informatics 1 --- Data \& Analysis}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infonefp}}
+      {\papertitle{Informatics 1 --- Functional Programming}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infonefpam}}
+      {\papertitle{Informatics 1 --- Functional Programming}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infonefppm}}
+      {\papertitle{Informatics 1 --- Functional Programming}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infoneop}}
+      {\papertitle{Informatics 1 --- Object-Oriented Programming}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infoneopam}}
+      {\papertitle{Informatics 1 --- Object-Oriented Programming}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{infoneoppm}}
+      {\papertitle{Informatics 1 --- Object-Oriented Programming}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{inftwoa}}
+      {\papertitle{Informatics 2A: Processing Formal and Natural Languages}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{inftwob}}
+      {\papertitle{Informatics 2B: Algorithms, Data Structures, Learning}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{inftwoccs}}
+      {\papertitle{Informatics 2C: Introduction to Computer Systems}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{inftwocse}}
+      {\papertitle{Informatics 2C: Introduction to Software Engineering}
+       \papertype{nonhons.inc}}{}
+    \ifthenelse{\equal{\courseid}{inftwod}}
+      {\papertitle{Informatics 2D: Reasoning and Agents}
+       \papertype{nonhons.inc}}{}
+  \ifthenelse{\equal{\courseid}{iar}}
+       {\papertitle{Intelligent Autonomous Robotics (Level 10)}
+       \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{imc}}
+       {\papertitle{Introduction to Modern Cryptography}
+       \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{iotssc}}
+       {\papertitle{Internet of Things Systems, Security, and the Cloud}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{iqc}}
+       {\papertitle{Introduction to Quantum Computing}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{itcs}}
+       {\papertitle{Introduction to Theoretical Computer Science}
+        \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{ivc}}
+      {\papertitle{Image and Vision Computing}
+       \papertype{msc.inc}}{}		
+    \ifthenelse{\equal{\courseid}{ivr}}
+      {\papertitle{Introduction to Vision and Robotics}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{iaml}}
+      {\papertitle{Introductory Applied Machine Learning}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{lpt}}
+      {\papertitle{Logic Programming --- Theory}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{lpp}}
+      {\papertitle{Logic Programming --- Programming}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{mlpr}}
+      {\papertitle{Machine Learning and Pattern Recognition}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{mt}}
+      {\papertitle{Machine Translation (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{mi}}
+      {\papertitle{INFR11079 Music Informatics}
+       \papertype{msc.inc}}{}	  
+    \ifthenelse{\equal{\courseid}{nlu}}
+      {\papertitle{Natural Language Understanding (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{nc}}
+      {\papertitle{Neural Computation}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{nip}}
+      {\papertitle{Neural Information Processing}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{os}}
+      {\papertitle{Operating Systems}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{pa}}
+      {\papertitle{Parallel Architectures (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{pdiot}}
+      {\papertitle{Principles and Design of IoT Systems}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{ppls}}
+      {\papertitle{Parallel Programming Languages and Systems (Level 11)}
+       \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{pm}}
+      {\papertitle{Performance Modelling}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{pmr}}
+      {\papertitle{Probabilistic Modelling and Reasoning}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{pi}}
+      {\papertitle{Professional Issues}
+       \papertype{inf3.inc}}{}
+	\ifthenelse{\equal{\courseid}{rc}}
+      {\papertitle{Randomness and Computation}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{rl}}
+      {\papertitle{Reinforcement Learning}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{rlsc}}
+      {\papetitle{Robot Learning and Sensorimotor Control}
+       \papertype{msc.inc}}{}
+    \ifthenelse{\equal{\courseid}{rss}}
+      {\papertitle{Robotics: Science and Systems}
+       \papertype{msc.inc}}{}
+	\ifthenelse{\equal{\courseid}{sp}}
+	  {\papertitle{INFR11098 Secure Programming}
+	   \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{sws}}
+	  {\papertitle{INFR11104 Semantic Web Systems}
+	   \papertype{inf4.inc}}{}
+	\ifthenelse{\equal{\courseid}{stn}}
+	  {\papertitle{INFR11124 Social and Technological Networks}
+	   \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{sapm}}
+      {\papertitle{Software Architecture, Process and Management (Level 11)}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{sdm}}
+      {\papertitle{Software Design and Modelling}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{st}}
+      {\papertitle{Software Testing}
+       \papertype{inf3.inc}}{}
+    \ifthenelse{\equal{\courseid}{ttds}}
+      {\papertitle{Text Technologies for Data Science}
+       \papertype{inf4.inc}}{}
+    \ifthenelse{\equal{\courseid}{tspl}}
+      {\papertitle{Types and Semantics for Programming Languages}
+       \papertype{inf4.inc}}{}
+
+ %   \ifthenelse{\equal{\courseid}{XXX}}
+ %     { }{}
+
+ %
+ % Let's also do a mock-up date/time to make the exam preparer happy:
+ % (Aren't we sweet?)
+ %
+  
+    \paperdate{1}{4}{2017}
+    \papertimes{00:00}{00:00}
+
+ %
+ % Also, we'll set the exam status to internal for the mock-up.
+ %
+
+    \internal
+
+  }}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Now, we can build the appropriate rubric form and type.
+%
+% We set rubric type and form to alert values.  These will be over-
+%  written if the author has done things right.  Otherwise, they
+%  will provide good error messages to the author.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\setrubricform{Rubric Form has not been initialized.}
+\setrubrictype{Rubric type has not been initialized.}
+
+\newcommand{\initrubricdata}{
+
+ %
+ % We need to load both form and type data for the rubric.
+ %
+ % If we're on an ITO machine, we'll load it from the master path.
+ % If not, we'll setup some mock-up values.
+ %
+ % We only do this if the rubric is not custom, though.
+ %
+ % This section also defines \rubricqA, B and C.  These are initialised as empty definitions
+ % and then the correct text is added depending on the rubric selected
+ %
+ \def\rubricqA{}
+ \def\rubricqB{}
+ \def\rubricqC{}
+
+ \ifthenelse{\equal{\rubricid}{custom}}{}
+ {
+     %% HONS RUBRICS
+     
+     \ifthenelse{\equal{\rubricid}{qu1_and_either_qu2_or_qu3}}{
+     \setrubrictype{
+         Answer QUESTION 1 and ONE other question. \\
+          \bigskip
+         Question 1 is COMPULSORY. If both QUESTION 2 and QUESTION 3 are answered, only QUESTION 2 will be marked. \\
+          \bigskip
+         All questions carry equal weight.\\
+	      \bigskip
+	     CALCULATORS MAY NOT BE USED IN THIS EXAMINATION \\
+         }
+         
+         %% Additional command to be used for question 1.
+         \def\rubricqA{THIS QUESTION IS COMPULSORY}
+		 \def\rubricqB{ANSWER EITHER THIS QUESTION OR QUESTION 3}
+		 \def\rubricqC{ANSWER EITHER THIS QUESTION OR QUESTION 2}
+     }{}
+
+     \ifthenelse{\equal{\rubricid}{qu1_and_either_qu2_or_qu3_calc}}{
+     \setrubrictype{
+         Answer QUESTION 1 and ONE other question. \\
+	      \bigskip
+	     Question 1 is COMPULSORY. If both QUESTION 2 and QUESTION 3 are answered, only QUESTION 2 will be marked. \\
+	      \bigskip
+	     All questions carry equal weight.\\
+           \bigskip
+
+         CALCULATORS MAY BE USED IN THIS EXAMINATION \\
+         }
+         
+         %% Additional command to be used for question 1.
+         \def\rubricqA{THIS QUESTION IS COMPULSORY}
+		 \def\rubricqB{ANSWER EITHER THIS QUESTION OR QUESTION 3}
+		 \def\rubricqC{ANSWER EITHER THIS QUESTION OR QUESTION 2}
+     }{}
+
+     \ifthenelse{\equal{\rubricid}{any_two_of_three}}{
+     \setrubrictype{
+         Answer any TWO of the three questions. If more than two questions are answered, only QUESTION 1 and QUESTION 2 will be marked.\\
+          \bigskip
+         All questions carry equal weight.\\
+	      \bigskip
+         CALCULATORS MAY NOT BE USED IN THIS EXAMINATION \\
+         }
+     }{}
+
+     \ifthenelse{\equal{\rubricid}{any_two_of_three_calc}}{
+     \setrubrictype{
+	     Answer any TWO of the three questions. If more than two questions are answered, only QUESTION 1 and QUESTION 2 will be marked.\\
+	      \bigskip
+         All questions carry equal weight.\\
+          \bigskip
+         CALCULATORS MAY BE USED IN THIS EXAMINATION \\
+         }
+     }{}
+       
+     \ifthenelse{\equal{\rubricid}{infone}}{
+     \setrubrictype{
+	     \begin{enumerate}
+	     \item Note that ALL QUESTIONS ARE COMPULSORY.
+	     \item DIFFERENT QUESTIONS MAY HAVE DIFFERENT NUMBERS OF TOTAL MARKS.
+	           Take note of this in allocating time to questions.
+	     \item CALCULATORS MAY NOT BE USED IN THIS EXAMINATION.
+	     \end{enumerate}
+         }
+     }{}
+
+	 \ifthenelse{\equal{\rubricid}{infone_calcs}}{
+     \setrubrictype{
+	     \begin{enumerate}
+         \item Note that ALL QUESTIONS ARE COMPULSORY.
+         \item DIFFERENT QUESTIONS MAY HAVE DIFFERENT NUMBERS OF TOTAL MARKS.
+               Take note of this in allocating time to questions.
+         \item CALCULATORS MAY BE USED IN THIS EXAMINATION.
+         \end{enumerate}
+         }
+     }{}
+
+     \ifthenelse{\equal{\rubricid}{infone_openbook}}{
+     \setrubrictype{
+         \begin{enumerate}
+         \item Note that ALL QUESTIONS ARE COMPULSORY.
+         \item DIFFERENT QUESTIONS MAY HAVE DIFFERENT NUMBERS OF TOTAL MARKS.
+               Take note of this in allocating time to questions.
+         \item This is an OPEN BOOK examination: notes and printed material are allowed,
+               but no electronic devices or electronic media.
+         \end{enumerate}
+         }
+     }{}
+	
+ }
+}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Now, we can build the title page.  This command must be called
+%  from the top-level exam document.
+%
+% To do so: \examtitlepage 
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+\newcommand{\examtitlepage}{
+
+\initrubricdata
+
+\status
+
+\thispagestyle{header}
+\begin{center}
+ {UNIVERSITY OF EDINBURGH}
+ \vskip 0.1in
+ {COLLEGE OF SCIENCE AND ENGINEERING}
+ \vskip 0.1in
+ {SCHOOL OF INFORMATICS}
+ \vskip 0.5in
+
+\begin{bf}
+{\nameofpaper}
+
+\begin{small}
+\vskip 0.5in
+{\today} \\
+\vskip 0.2in
+{\timeofpaper}
+\vskip 0.75in
+\end{small}
+
+{INSTRUCTIONS TO CANDIDATES} \\
+\bigskip\bigskip
+
+\rubrictype
+\end{bf}
+
+\vskip 0.5in
+
+\begin{small}
+{\typeofpaper}
+\end{small}
+
+\vskip 0.5in
+THIS EXAMINATION WILL BE MARKED ANONYMOUSLY
+
+\end{center}
+
+\setcounter{page}{0}
+\newpage
+
+\status
+}
+
+
diff --git a/tspl/instructions.pdf b/tspl/instructions.pdf
new file mode 100644
index 00000000..0eb17918
Binary files /dev/null and b/tspl/instructions.pdf differ
diff --git a/tspl/instructions.tex b/tspl/instructions.tex
new file mode 100644
index 00000000..5e924fc8
--- /dev/null
+++ b/tspl/instructions.tex
@@ -0,0 +1,122 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Instructions for TSPL Exam
+% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\documentclass[12pt]{article}
+\usepackage{a4,amssymb}
+% \setlength{\oddsidemargin}{-1.5cm}
+% \addtolength{\textwidth}{2cm}
+% \addtolength{\textheight}{3cm}
+
+\begin{document}
+\pagestyle{empty}
+\setcounter{page}{1}
+
+\begin{center}
+\large Types and Semantics for Programming Languages
+\end{center}
+
+\section*{Instructions}
+
+\begin{enumerate}
+
+\item
+  The exam lasts two hours.
+
+\item
+  Place your student identity card face-up on the desk in front of you.  The
+  invigilator may come to check your identity, and in this case you may be asked
+  to allow the invigilator to briefly use your computer.  The exam time has been
+  calculated to allow time for such interruptions.
+
+\item
+  You may log into your computer as soon as you are ready to do so.
+
+\item
+  To download the exam paper, open a terminal window and type:
+  \begin{center}
+    \texttt{getpapers}
+  \end{center}
+  This will create a subdirectory \texttt{tspl-pe} in your home directory,
+  containing the following files.
+  \begin{center}
+    \begin{tabular}{ll}
+      \texttt{tspl-pe/papers/exam.pdf}                & the exam \\
+      \texttt{tspl-pe/papers/instructions.pdf}        & these instructions \\
+      \texttt{tspl-pe/templates/Exam.lagda}           & exam template to edit \\
+      \texttt{tspl-pe/original\_templates/Exam.lagda} & backup of exam template
+    \end{tabular}
+  \end{center}
+  The directories \texttt{tspl-pe/papers} and
+  \texttt{tspl-pe/original\_templates}
+  are read only, but you may read and write \texttt{tspl-pe/templates}.
+
+\item
+  To setup the Agda environment, open a second terminal window and type:
+  \begin{center}
+    \texttt{tspl-setup}
+  \end{center}
+  This will open a browser, with three tabs which contain the textbook
+  \emph{Programming Language Foundations in Agda}, the documentation for the
+  Agda standard library, and the documentation for Agda.  (The browser may
+  also attempt to link to the internet, which brings up a tab labeled
+  ``Problem loading page''; this is expected and not a problem.)
+
+{\it (Note that internet access has been disabled.)}
+
+\begin{center}
+  \textbf{Do nothing further until the start of the exam is announced!}
+\end{center}
+
+\hfill \textit{Please Turn Over}
+\newpage
+
+\item When the start of the exam is announced, open the exam paper
+\begin{center}
+  \texttt{tspl-pe/papers/exam.pdf}
+\end{center}
+with the standard PDF viewer.
+
+\item Change to the template directory
+\begin{center}
+  \texttt{cd tspl-pe/templates}
+\end{center}
+and edit the file
+\begin{center}
+  \texttt{Exam.lagda}
+\end{center}
+to include your answers, using Emacs or anything else suitable.
+You are recommended to save your work on a regular basis.
+
+\item Before submitting, make sure your file is processed by Agda
+  correctly. Code which prevents the file from compiling should be
+  made into comments. If you fail to solve part of a problem, you
+  may get more credit if you indicate clearly which part you have
+  not solved. 
+
+\item \emph{Please ensure before submission that the file}
+  \texttt{Exam.lagda} \emph{contains your solutions to the exam.}  Submit
+  your file using the command:
+  \begin{center}
+  \texttt{examsubmit Exam.lagda}
+  \end{center}
+  If you get an error, please check carefully that your file is called
+  \texttt{Exam.lagda} and that you are in the same directory as this
+  file. If you continue to have problems, please contact one of the
+  invigilators.
+ 
+Repeated submit commands are allowed, and will overwrite previous
+submissions.  The last file submitted will be the one marked.
+
+\item When the invigilators announce the end of the exam, you must
+  submit and log out immediately.
+
+\end{enumerate}
+
+\end{document}
+
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
diff --git a/tspl/mock.pdf b/tspl/mock.pdf
new file mode 100644
index 00000000..afbf55c4
Binary files /dev/null and b/tspl/mock.pdf differ
diff --git a/tspl/mock.tex b/tspl/mock.tex
new file mode 100644
index 00000000..33eb1306
--- /dev/null
+++ b/tspl/mock.tex
@@ -0,0 +1,407 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% I N F O R M A T I C S
+%  Honours Exam LaTeX Template for Exam Authors
+%
+%  Created: 12-Oct-2009 by G.O.Passmore.
+%  Last Updated: 10-Sep-2018 by I. Murray
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% The following define the status of the exam papers in the order
+%%% required.  Simply remove the comment (i.e., the % symbol) just
+%%% before the appropriate one and comment the others out.
+
+%\newcommand\status{\internal}
+%\newcommand\status{\external}
+\newcommand\status{\final}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% The following three lines are always required.  You may add
+%%% custom packages to the one already defined if necessary.
+
+\documentclass{examhons2018}
+\usepackage{amssymb}
+\usepackage{amsmath}
+\usepackage{semantic}
+\usepackage{stix}
+
+%%% Uncomment the \checkmarksfalse line if the macros that check the
+%%% mark totals cause problems. However, please do not make your
+%%% questions add up to a non-standard number of marks without
+%%% permission of the convenor.
+%\checkmarksfalse
+
+\begin{document}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Replace {ad} below with the ITO code for your course.  This will
+%  be used by the ITO LaTeX installation to install course-specific
+%  data into the exam versions it produces from this document.
+%
+% Your choices are (in course title order):
+%
+%   {anlp}     - Acc. Natural Language Processing	            (MSc)
+%   {aleone}   - Adaptive Learning Environments 1              (Inf4)
+%   {adbs}     - Advanced Databases                            (Inf4)
+%   {av}       - Advanced Vision                               (Inf4)
+%   {av-dl}    - Advanced Vision - distance learning            (MSc)
+%   {apl}      - Advances in Programming Languages             (Inf4)
+%   {abs}      - Agent Based Systems [L10]                     (Inf3)
+%   {afds}     - Algorithmic Foundations of Data Science        (MSc)
+%   {agta}     - Algorithmic Game Theory and its Apps.          (MSc)
+%   {ads}      - Algorithms and Data Structures                (Inf3)
+%   {ad}       - Applied Databases                              (MSc)
+%   {aipf}     - Artificial Intelligence Present and Future     (MSc)
+%   {ar}       - Automated Reasoning 	                       (Inf3)
+%   {asr}      - Automatic Speech Recognition                  (Inf4)
+%   {bioone}   - Bioinformatics 1                               (MSc)
+%   {biotwo}   - Bioinformatics 2                               (MSc)
+%	{bdl}      - Blockchains and Distributed Ledgers		   (Inf4)
+%   {cqi}      - Categories and Quantum Informatics             (MSc)
+%   {copt}     - Compiler Opimisation [L11]                    (Inf4)
+%   {ct}       - Compiling Techniques                          (Inf3)
+%   {ccs}      - Computational Cognitive Science               (Inf3)
+%   {cmc}      - Computational Complexity                      (Inf4)
+%   {ca}       - Computer Algebra                              (Inf4)
+%   {cav}      - Computer Animation and Visualisation          (Inf4)
+%   {car}      - Computer Architecture                         (Inf3)
+%   {comn}     - Computer Comms. and Networks                  (Inf3)
+%   {cd}       - Computer Design                               (Inf3)
+%   {cg}       - Computer Graphics [L11]                       (Inf4)
+%   {cn}       - Computer Networking [L11]                     (Inf4)
+%   {cp}       - Computer Prog. Skills and Concepts         (nonhons)
+%   {cs}       - Computer Security                             (Inf3)
+%   {dds}      - Data, Design and Society                   (nonhons)
+%   {dme}      - Data Mining and Exploration                   (Msc)
+%   {dbs}      - Database Systems                              (Inf3)
+%   {dmr}      - Decision Making in Robots and Autonomous Agents(MSc)
+%   {dmmr}     - Discrete Maths. and Math. Reasoning        (nonhons)
+%   {ds}       - Distributed Systems [L11]                     (Inf4)
+%   {epl}      - Elements of Programming Languages             (Inf3)
+%   {es}       - Embedded Software                             (Inf4)
+%   {exc}      - Extreme Computing                             (Inf4)
+%   {fv}       - Formal Verification                           (Inf4)
+%   {fnlp}     - Foundations of Natural Language Processing    (Inf3)
+%   {hci}      - Human-Computer Interaction [L11]              (Inf4)
+%   {infonea}  - Informatics 1 - Introduction to Computation(nonhons)
+%   different sittings for INF1A programming exams
+%   {infoneapone}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infoneaptwo}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infoneapthree}  - Informatics 1 - Introduction to Computation(nonhons)
+%   {infonecg} - Informatics 1 - Cognitive Science          (nonhons)
+%   {infonecl} - Informatics 1 - Computation and Logic      (nonhons)
+%   {infoneda} - Informatics 1 - Data and Analysis          (nonhons)
+%   {infonefp} - Informatics 1 - Functional Programming     (nonhons)
+%   If there are two sittings of FP, use infonefpam for the first
+%   paper and infonefppm for the second sitting.
+%   {infoneop} - Informatics 1 - Object-Oriented Programming(nonhons)
+%   If there are two sittings of OOP, use infoneopam for the first
+%   paper and infoneoppm for the second sitting.
+%   {inftwoa}  - Informatics 2A: Proc. F&N Languages        (nonhons)
+%   {inftwob}  - Informatics 2B: Algs., D.Structs., Learning(nonhons)
+%   {inftwoccs}- Informatics 2C-CS: Computer Systems        (nonhons)
+%   {inftwocse}- Informatics 2C: Software Engineering       (nonhons)
+%   {inftwod}  - Informatics 2D: Reasoning and Agents       (nonhons)
+%   {iar}      - Intelligent Autonomous Robotics               (Inf4)
+%   {it}       - Information Theory                             (MSc)
+%   {imc}      - Introduction to Modern Cryptography           (Inf4)
+%   {iotssc}   - Internet of Things, Systems, Security and the Cloud   (Inf4)
+%   (iqc)      - Introduction to Quantum Computing             (Inf4)
+%   (itcs)     - Introduction to Theoretical Computer Science  (Inf3)
+%   {ivc}      - Image and Vision Computing			           (MSc)
+%   {ivr}      - Introduction to Vision and Robotics           (Inf3)
+%   {ivr-dl}   - Introduction to Vision and Robotics - distance learning (Msc)
+%   {iaml}     - Introductory Applied Machine Learning         (MSc)
+%   {iaml-dl}  - Introductory Applied Machine Learning - distance learning (MSc)
+%   {lpt}      - Logic Programming - Theory                    (Inf3)
+%   {lpp}      - Logic Programming - Programming               (Inf3)
+%   {mlpr}     - Machine Learning & Pattern Recognition        (Inf4)
+%   {mt}       - Machine Translation                           (Inf4)
+%   {mi}       - Music Informatics                              (MSc)
+%   {nlu}      - Natural Language Understanding [L11]          (Inf4)
+%   {nc}       - Neural Computation                             (MSc)
+%   {nat}      - Natural Computing                              (MSc)
+%   {nluplus}  - Natural Language Understanding, Generation, and Machine Translation(MSc)
+%   {nip}      - Neural Information Processing                  (MSc)
+%   {os}       - Operating Systems                             (Inf3)
+%   {pa}       - Parallel Architectures [L11]                  (Inf4)
+%   {pdiot}    - Principles and Design of IoT Systems          (Inf4)
+%   {ppls}     - Parallel Prog. Langs. and Sys. [L11]          (Inf4)
+%   {pm}       - Performance Modelling                         (Inf4)
+%   {pmr}      - Probabilistic Modelling and Reasoning          (MSc)
+%   {pi}       - Professional Issues                           (Inf3)
+%   {rc}       - Randomness and Computation                    (Inf4)
+%   {rl}       - Reinforcement Learning                         (MSc)
+%   {rlsc}     - Robot Learning and Sensorimotor Control        (MSc)
+%   {rss}      - Robotics: Science and Systems                  (MSc)
+%   {sp}       - Secure Programming                            (Inf4)
+%   {sws}      - Semantic Web Systems                          (Inf4)
+%   {stn}      - Social and Technological Networks             (Inf4)
+%   {sapm}     - Software Arch., Proc. and Mgmt. [L11]         (Inf4)
+%   {sdm}      - Software Design and Modelling                 (Inf3)
+%   {st}       - Software Testing                              (Inf3)
+%   {ttds}     - Text Technologies for Data Science            (Inf4)
+%   {tspl}     - Types and Semantics for Programming Langs.    (Inf4)
+%   {usec}     - Usable Security and Privacy                   (Inf4)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\setcourse{tspl}
+\initcoursedata
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Set your exam rubric type.
+%
+% Most courses in the School have exams that add up to 50 marks,
+% and your choices are:
+%    {qu1_and_either_qu2_or_qu3, any_two_of_three, do_exam}
+% (which include the "CALCULATORS MAY NOT BE USED..." text), or
+%    {qu1_and_either_qu2_or_qu3_calc, any_two_of_three_calc, do_exam_calc}
+% (which DO NOT include the "CALCULATORS MAY NOT BE USED..." text), or
+%    {custom}.
+%
+% Note, if you opt to create a custom rubric, you must:
+%
+%   (i) **have permission** from the appropriate authority, and
+%  (ii) execute:
+%
+%        \setrubrictype{} to specify the custom rubric information.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\setrubric{qu1_and_either_qu2_or_qu3}
+
+\examtitlepage
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Manual override for total page number computation.
+%
+% As long as you run latex upon this document three times in a row,
+%  the right number of `total pages' should be computed and placed
+%  in the footer of all pages except the title page.
+%
+% But, if this fails, you can set that number yourself with the
+%  following command:
+%
+%    \settotalpages{n} with n a natural number.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% Beginning of your exam text.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\begin{enumerate}
+
+\item \rubricqA
+
+\newcommand{\key}{\texttt}
+\newcommand{\List}{\key{list}}
+\newcommand{\nil}{\texttt{[]}}
+\newcommand{\cons}{\mathbin{\key{::}}}
+\newcommand{\member}{\key{member}}
+\newcommand{\sublist}{\key{sublist}}
+
+This question uses the library definition of $\List$ in Agda.
+Here is an informal definition of the predicates $\in$
+and $\subseteq$.  (In Emacs, you can type $\in$ as \verb$\in$ and $\subseteq$ as \verb$\subseteq$.)
+$\subseteq$
+\begin{gather*}
+\inference[$\key{here}$]
+  {}
+  {x \in (x \cons xs)}
+\qquad
+\inference[$\key{there}$]
+  {x \in ys}
+  {x \in (y \cons ys)}
+\\~\\
+\inference[$\key{done}$]
+  {}
+  {\nil \subseteq ys}
+\\~\\
+\inference[$\key{keep}$]
+  {xs \subseteq ys}
+  {(x \cons xs) \subseteq (x \cons ys)}
+\qquad
+\inference[$\key{drop}$]
+  {xs \subseteq ys}
+  {xs \subseteq (y \cons ys)}
+\end{gather*}
+
+\begin{itemize}
+
+\item[(a)] Formalise the definition above.
+\marks{10}
+
+\item[(b)] Prove each of the following.
+  \begin{itemize}
+  \item[(i)]  $\key{2} \in \key{[1,2,3]}$
+  \item[(ii)]  $\key{[1,3]} \subseteq \key{[1,2,3,4]}$
+  \end{itemize}
+\marks{5}
+
+\item[(c)] Prove the following.
+\begin{center}
+If $xs \subseteq ys$ then $z \in xs$ implies $z \in ys$ for all $z$.
+\end{center}
+\marks{10}
+
+\end{itemize}
+
+\newpage
+
+\item \rubricqB
+
+\newcommand{\Tree}{\texttt{Tree}}
+\newcommand{\leaf}{\texttt{leaf}}
+\newcommand{\branch}{\texttt{branch}}
+\newcommand{\CASET}{\texttt{caseT}}
+\newcommand{\caseT}[6]{\texttt{case}~#1~\texttt{[leaf}~#2~\Rightarrow~#3~\texttt{|}~#4~\texttt{branch}~#5~\Rightarrow~#6\texttt{]}}
+\newcommand{\ubar}{\texttt{\underline{~}}}
+\newcommand{\comma}{\,\texttt{,}\,}
+\newcommand{\V}{\texttt{V}}
+\newcommand{\dash}{\texttt{-}}
+\newcommand{\Value}{\texttt{Value}}
+\newcommand{\becomes}{\longrightarrow}
+\newcommand{\subst}[3]{#1~\texttt{[}~#2~\texttt{:=}~#3~\texttt{]}}
+
+
+You will be provided with a definition of intrinsically-typed lambda
+calculus in Agda. Consider constructs satisfying the following rules,
+written in extrinsically-typed style.
+
+Typing:
+\begin{gather*}
+  \inference[\leaf]
+    {\Gamma \vdash M \typecolon A}
+    {\Gamma \vdash \leaf~M \typecolon \Tree~A}
+\quad
+  \inference[\branch]
+    {\Gamma \vdash M \typecolon \Tree~A \\
+     \Gamma \vdash N \typecolon \Tree~A}
+    {\Gamma \vdash M~\branch~N \typecolon \Tree~A}
+\\~\\
+  \inference[\CASET]
+    {\Gamma \vdash L \typecolon \Tree~A \\
+     \Gamma \comma x \typecolon A \vdash M \typecolon B \\
+     \Gamma \comma y \typecolon \Tree~A \comma z \typecolon \Tree~A \vdash N \typecolon B}
+    {\Gamma \vdash \caseT{L}{x}{M}{y}{z}{N} \typecolon B}
+\end{gather*}
+
+Values:
+\begin{gather*}
+\inference[\V\dash\leaf]
+  {\Value~V}
+  {\Value~(\leaf~V)}
+\qquad
+\inference[\V\dash\branch]
+  {\Value~V \\
+   \Value~W}
+  {\Value~(V~\branch~W)}
+\end{gather*}
+
+Reduction:
+\begin{gather*}
+\inference[$\xi\dash\leaf$]
+  {M \becomes M'}
+  {\leaf{M} \becomes \leaf{M'}}
+\\~\\
+\inference[$\xi\dash\branch_1$]
+  {M \becomes M'}
+  {M~\branch~N \becomes M'~\branch~N}
+\qquad
+\inference[$\xi\dash\branch_2$]
+  {\Value~V \\
+   N \becomes N'}
+  {V~\branch~N \becomes V~\branch~N'}
+\\~\\
+\inference[$\xi\dash\CASET$]
+  {L \becomes L'}
+  {\begin{array}{c}
+     \caseT{L}{x}{M}{y}{z}{N} \becomes \\
+     {} \quad \caseT{L'}{x}{M}{y}{z}{N}
+   \end{array}}
+\\~\\
+\inference[$\beta\dash\leaf$]
+  {\Value~V}
+  {\caseT{(\leaf~V)}{x}{M}{y}{z}{N} \becomes \subst{M}{x}{V}}
+\\~\\
+\inference[$\beta\dash\branch$]
+  {\Value~V \\
+   \Value~W}
+  {\caseT{(V~\branch~W)}{x}{M}{y}{z}{N} \becomes \subst{\subst{N}{y}{V}}{z}{W}}
+\end{gather*}
+
+\begin{enumerate}
+\item[(a)] Extend the given definition to formalise the evaluation and
+  typing rules, including any other required definitions.
+      \marks{12}
+
+\item[(b)] Prove progress. You will be provided with a proof of
+  progress for the simply-typed lambda calculus that you may
+  extend.
+      \marks{13}
+\end{enumerate}
+
+Please delimit any code you add as follows.
+\begin{verbatim}
+-- begin
+-- end
+\end{verbatim}
+
+\newpage
+
+\item \rubricqC
+
+\newcommand{\Lift}{\texttt{Lift}}
+\newcommand{\delay}{\texttt{delay}}
+\newcommand{\force}{\texttt{force}}
+\newcommand{\up}{\uparrow}
+\newcommand{\dn}{\downarrow}
+
+You will be provided with a definition of inference for extrinsically-typed lambda
+calculus in Agda. Consider constructs satisfying the following rules,
+written in extrinsically-typed style that support bidirectional inference.
+
+Typing:
+\begin{gather*}
+\inference[$\delay$]
+  {\Gamma \vdash M \dn A}
+  {\Gamma \vdash \delay~M \dn \Lift~A}
+\\~\\
+\inference[$\force$]
+  {\Gamma \vdash L \up \Lift~A}
+  {\Gamma \vdash \force~L \up A}
+\end{gather*}
+
+\begin{enumerate}
+\item[(a)] Extend the given definition to formalise the typing rules,
+and update the definition of equality on types.
+      \marks{10}
+
+\item[(b)] Extend the code to support type inference for the new features.
+      \marks{15}
+\end{enumerate}
+
+Please delimit any code you add as follows.
+\begin{verbatim}
+-- begin
+-- end
+\end{verbatim}
+
+\end{enumerate}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% End of your exam text.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\end{document}
diff --git a/tspl/tspl.agda-lib b/tspl/tspl.agda-lib
new file mode 100644
index 00000000..8c72811e
--- /dev/null
+++ b/tspl/tspl.agda-lib
@@ -0,0 +1,3 @@
+name: tspl
+depend: standard-library plfa
+include: .