Advent of proof submissions.HEADmaster

Completed all problems save 12, where I had to postulate two lemma.

27 files changed, 2858 insertions, 0 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..a485625
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+/_build
diff --git a/Everything.agda b/Everything.agda
new file mode 100644
index 0000000..477429a
--- /dev/null
+++ b/Everything.agda
@@ -0,0 +1,26 @@
+module Everything where
+
+import Problem1
+import Problem10
+import Problem11
+import Problem12
+import Problem13
+import Problem14
+import Problem15
+import Problem16
+import Problem17
+import Problem18
+import Problem19
+import Problem2
+import Problem20
+import Problem21
+import Problem22
+import Problem23
+import Problem24
+import Problem3
+import Problem4
+import Problem5
+import Problem6
+import Problem7
+import Problem8
+import Problem9
diff --git a/advent-of-proof.agda-lib b/advent-of-proof.agda-lib
new file mode 100644
index 0000000..c647589
--- /dev/null
+++ b/advent-of-proof.agda-lib
@@ -0,0 +1,4 @@
+name: advent-of-proof
+depend: standard-library
+include: src
+flags: --without-K
diff --git a/src/Problem1.agda b/src/Problem1.agda
new file mode 100644
index 0000000..3aab789
--- /dev/null
+++ b/src/Problem1.agda
@@ -0,0 +1,87 @@
+{-# OPTIONS --safe #-}
+
+module Problem1 where
+
+open import Data.Nat
+open import Relation.Binary.PropositionalEquality
+
+open ≡-Reasoning
+
+data 𝔹 : Set where
+    T F : 𝔹
+
+iterate : (n : ℕ) (f : 𝔹 → 𝔹) (x : 𝔹) → 𝔹
+iterate zero f x = x
+iterate (suc n) f x = f (iterate n f x)
+
+twice = iterate (suc (suc zero))
+
+-- There are exactly four functions 𝔹 → 𝔹: the two constant functions, the
+-- identiy and the inversion.
+--
+-- We can decide (extensionally) which function we have.
+
+data OneOf (f : 𝔹 → 𝔹) : Set where
+  is-const : (∀ x y → f x ≡ f y) → OneOf f
+  is-id    : (∀ x → f x ≡ x) → OneOf f
+  is-not   : f T ≡ F → f F ≡ T → OneOf f
+
+which-one? : (f : 𝔹 → 𝔹) → OneOf f
+which-one? f with f T in prfT | f F in prfF
+... | T | T = is-const λ
+  { T T → refl
+  ; T F → begin
+    f T ≡⟨ prfT ⟩
+    T   ≡⟨ sym prfF ⟩
+    f F ∎
+  ; F T → begin
+    f F ≡⟨ prfF ⟩
+    T   ≡⟨ sym prfT ⟩
+    f T ∎
+  ; F F → refl
+  }
+... | T | F = is-id    λ { T → prfT ; F → prfF }
+... | F | T = is-not   prfT prfF
+... | F | F = is-const λ
+  { T T → refl
+  ; T F → begin
+    f T ≡⟨ prfT ⟩
+    F   ≡⟨ sym prfF ⟩
+    f F ∎
+  ; F T → begin
+    f F ≡⟨ prfF ⟩
+    F   ≡⟨ sym prfT ⟩
+    f T ∎
+  ; F F → refl
+  }
+
+-- First, we show that applying a function thrice is equal to a single
+-- application. We do this by splitting on the exact function.
+
+thrice-is-once : (f : 𝔹 → 𝔹) → iterate 3 f ≗ f
+thrice-is-once f with which-one? f
+... | is-const prf = λ b → prf (f (f b)) b
+... | is-id    prf = λ b →
+  begin
+    f (f (f b)) ≡⟨ prf (f (f b)) ⟩
+    f (f b)     ≡⟨ prf (f b) ⟩
+    f b         ∎
+... | is-not   prfT prfF = λ
+  { T → begin
+    f (f (f T)) ≡⟨ cong (twice f) prfT ⟩
+    f (f F)     ≡⟨ cong f prfF ⟩
+    f T         ∎
+  ; F → begin
+    f (f (f F)) ≡⟨ cong (twice f) prfF ⟩
+    f (f T)     ≡⟨ cong f prfT ⟩
+    f F         ∎
+  }
+
+-- We prove the theorem by induction on n.
+
+goal : ∀ (f : 𝔹 → 𝔹) (b : 𝔹) (n : ℕ) → iterate n (twice f) (f b) ≡ f b
+goal f b zero    = refl
+goal f b (suc n) = begin
+  f (f (iterate n (twice f) (f b))) ≡⟨ cong (twice f) (goal f b n) ⟩
+  f (f (f b))                       ≡⟨ thrice-is-once f b ⟩
+  f b                               ∎
diff --git a/src/Problem10.agda b/src/Problem10.agda
new file mode 100644
index 0000000..0e465d6
--- /dev/null
+++ b/src/Problem10.agda
@@ -0,0 +1,89 @@
+module Problem10 where
+
+open import Relation.Binary.PropositionalEquality
+
+open ≡-Reasoning
+
+infixl 15 _⋆_
+
+postulate
+  C : Set
+  _⋆_ : C → C → C
+  _ᵒ : C → C
+  assoc : ∀ a b c → (a ⋆ b) ⋆ c ≡ a ⋆ (b ⋆ c)
+  ᵒ-prop : ∀ a → a ⋆ a ᵒ ⋆ a ≡ a
+
+_ᶜ : C → C
+x ᶜ = x ᵒ ⋆ x ⋆ x ᵒ
+
+prop₁ : ∀ a → a ⋆ a ᶜ ⋆ a ≡ a
+prop₁ a = begin
+  a ⋆ (a ᵒ ⋆ a ⋆ a ᵒ) ⋆ a ≡˘⟨ cong (_⋆ a) (assoc a (a ᵒ ⋆ a) (a ᵒ)) ⟩
+  a ⋆ (a ᵒ ⋆ a) ⋆ a ᵒ ⋆ a ≡˘⟨ cong (λ - → - ⋆ a ᵒ ⋆ a) (assoc a (a ᵒ) a) ⟩
+  a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ⋆ a   ≡⟨ cong (λ - → - ⋆ a ᵒ ⋆ a) (ᵒ-prop a) ⟩
+  a ⋆ a ᵒ ⋆ a             ≡⟨ ᵒ-prop a ⟩
+  a                       ∎
+prop₂ : ∀ a → a ᶜ ⋆ a ⋆ a ᶜ ≡ a ᶜ
+prop₂ a = begin
+  a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a ⋆ a ᵒ) ≡˘⟨ assoc (a ᵒ ⋆ a ⋆ a ᵒ ⋆ a) (a ᵒ ⋆ a) (a ᵒ) ⟩
+  a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a) ⋆ a ᵒ ≡˘⟨ cong (_⋆ a ᵒ) (assoc (a ᵒ ⋆ a ⋆ a ᵒ ⋆ a) (a ᵒ) a) ⟩
+  a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ   ≡⟨ cong (λ - → - ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) a (a ᵒ)) ⟩
+  a ᵒ ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → - ⋆ a ᵒ ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) (a ⋆ a ᵒ) a) ⟩
+  a ᵒ ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ a ᵒ ⋆ a ⋆ a ᵒ ≡⟨ cong (λ - → a ᵒ ⋆ - ⋆ a ᵒ ⋆ a ⋆ a ᵒ) (ᵒ-prop a) ⟩
+  a ᵒ ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ             ≡⟨ cong (λ - → - ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) a (a ᵒ)) ⟩
+  a ᵒ ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ a ᵒ           ≡⟨ cong (_⋆ (a ᵒ)) (assoc (a ᵒ) (a ⋆ a ᵒ) a) ⟩
+  a ᵒ ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ a ᵒ           ≡⟨ cong (λ - → a ᵒ ⋆ - ⋆ a ᵒ) (ᵒ-prop a) ⟩
+  a ᵒ ⋆ a ⋆ a ᵒ                       ∎
+
+postulate
+  commute : ∀ a b → a ⋆ a ≡ a → b ⋆ b ≡ b → a ⋆ b ≡ b ⋆ a
+
+uniqueness : ∀ a z →  a ⋆ z ⋆ a ≡ a
+                   →  z ⋆ a ⋆ z ≡ z
+                   →  z ≡ a ᶜ
+uniqueness a z aza≡a zaz≡z = begin
+  z                         ≡˘⟨ zaz≡z ⟩
+  z ⋆ a ⋆ z                 ≡˘⟨ cong (λ - → z ⋆ - ⋆ z) (ᵒ-prop a) ⟩
+  z ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ z     ≡˘⟨ cong (_⋆ z) (assoc z (a ⋆ a ᵒ) a) ⟩
+  z ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ z     ≡⟨ assoc (z ⋆ (a ⋆ a ᵒ)) a z ⟩
+  z ⋆ (a ⋆ a ᵒ) ⋆ (a ⋆ z)   ≡⟨ assoc z (a ⋆ a ᵒ) (a ⋆ z) ⟩
+  z ⋆ ((a ⋆ a ᵒ) ⋆ (a ⋆ z)) ≡⟨ cong (z ⋆_) (commute (a ⋆ a ᵒ) (a ⋆ z) aaᵒaaᵒ≡aaᵒ azaz≡az) ⟩
+  z ⋆ ((a ⋆ z) ⋆ (a ⋆ a ᵒ)) ≡˘⟨ assoc z (a ⋆ z) (a ⋆ a ᵒ) ⟩
+  z ⋆ (a ⋆ z) ⋆ (a ⋆ a ᵒ)   ≡˘⟨ cong (_⋆ (a ⋆ a ᵒ)) (assoc z a z) ⟩
+  z ⋆ a ⋆ z ⋆ (a ⋆ a ᵒ)     ≡⟨ cong (_⋆ (a ⋆ a ᵒ)) zaz≡z ⟩
+  z ⋆ (a ⋆ a ᵒ)             ≡˘⟨ assoc z a (a ᵒ) ⟩
+  z ⋆ a ⋆ a ᵒ               ≡˘⟨ cong (λ - → z ⋆ - ⋆ (a ᵒ)) (ᵒ-prop a) ⟩
+  z ⋆ (a ⋆ a ᵒ ⋆ a) ⋆ a ᵒ   ≡˘⟨ cong (_⋆ a ᵒ) (assoc z (a ⋆ a ᵒ) a) ⟩
+  z ⋆ (a ⋆ a ᵒ) ⋆ a ⋆ a ᵒ   ≡˘⟨ cong (λ - → - ⋆ a ⋆ a ᵒ) (assoc z a (a ᵒ)) ⟩
+  z ⋆ a ⋆ a ᵒ ⋆ a ⋆ a ᵒ     ≡⟨ cong (_⋆ a ᵒ) (assoc (z ⋆ a) (a ᵒ) a) ⟩
+  z ⋆ a ⋆ (a ᵒ ⋆ a) ⋆ a ᵒ   ≡⟨ cong (_⋆ a ᵒ) (commute (z ⋆ a) (a ᵒ ⋆ a) zaza≡za aᵒaaᵒa≡aᵒa) ⟩
+  a ᵒ ⋆ a ⋆ (z ⋆ a) ⋆ a ᵒ   ≡˘⟨ cong (_⋆ a ᵒ) (assoc (a ᵒ ⋆ a) z a) ⟩
+  a ᵒ ⋆ a ⋆ z ⋆ a ⋆ a ᵒ     ≡⟨ cong (λ - → - ⋆ a ⋆ a ᵒ) (assoc (a ᵒ) a z) ⟩
+  a ᵒ ⋆ (a ⋆ z) ⋆ a ⋆ a ᵒ   ≡⟨ cong (_⋆ a ᵒ) (assoc (a ᵒ) (a ⋆ z) a) ⟩
+  a ᵒ ⋆ (a ⋆ z ⋆ a) ⋆ a ᵒ   ≡⟨ cong (λ - → a ᵒ ⋆ - ⋆ a ᵒ) aza≡a ⟩
+  a ᵒ ⋆ a ⋆ a ᵒ             ∎
+  where
+  zaza≡za : z ⋆ a ⋆ (z ⋆ a) ≡ z ⋆ a
+  zaza≡za = begin
+    z ⋆ a ⋆ (z ⋆ a) ≡˘⟨ assoc (z ⋆ a) z a ⟩
+    z ⋆ a ⋆ z ⋆ a   ≡⟨ cong (_⋆ a) zaz≡z ⟩
+    z ⋆ a           ∎
+
+  azaz≡az : a ⋆ z ⋆ (a ⋆ z) ≡ a ⋆ z
+  azaz≡az = begin
+    a ⋆ z ⋆ (a ⋆ z) ≡˘⟨ assoc (a ⋆ z) a z ⟩
+    a ⋆ z ⋆ a ⋆ z   ≡⟨ cong (_⋆ z) aza≡a ⟩
+    a ⋆ z           ∎
+
+  aᵒaaᵒa≡aᵒa : a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a) ≡ a ᵒ ⋆ a
+  aᵒaaᵒa≡aᵒa = begin
+    a ᵒ ⋆ a ⋆ (a ᵒ ⋆ a)   ≡⟨ assoc (a ᵒ) a (a ᵒ ⋆ a) ⟩
+    a ᵒ ⋆ (a ⋆ (a ᵒ ⋆ a)) ≡˘⟨ cong (a ᵒ ⋆_) (assoc a (a ᵒ) a) ⟩
+    a ᵒ ⋆ (a ⋆ a ᵒ ⋆ a)   ≡⟨ cong (a ᵒ ⋆_) (ᵒ-prop a) ⟩
+    a ᵒ ⋆ a               ∎
+
+  aaᵒaaᵒ≡aaᵒ : a ⋆ a ᵒ ⋆ (a ⋆ a ᵒ) ≡ a ⋆ a ᵒ
+  aaᵒaaᵒ≡aaᵒ = begin
+    a ⋆ a ᵒ ⋆ (a ⋆ a ᵒ) ≡˘⟨ assoc (a ⋆ a ᵒ) a (a ᵒ) ⟩
+    a ⋆ a ᵒ ⋆ a ⋆ a ᵒ   ≡⟨ cong (_⋆ a ᵒ) (ᵒ-prop a) ⟩
+    a ⋆ a ᵒ             ∎
diff --git a/src/Problem11.agda b/src/Problem11.agda
new file mode 100644
index 0000000..686f645
--- /dev/null
+++ b/src/Problem11.agda
@@ -0,0 +1,69 @@
+{-# OPTIONS --safe #-}
+
+module Problem11 where
+
+data Term : Set where
+  Ref : Term
+  Sop : Term
+  Kop : Term
+  App : Term → Term → Term
+
+variable M N P M₁ M₂ M₃ N₁ N₂ : Term
+
+data _↦_ : Term → Term → Set where
+  red-S : (App (App (App Sop M) N) P) ↦ (App (App M P) (App N P))
+  red-K : (App (App Kop M) N) ↦ M
+  red-left : M₁ ↦ M₂ → App M₁ N ↦ App M₂ N
+  red-right : N₁ ↦ N₂ → App M N₁ ↦ App M N₂
+  red-trans : M ↦ N → N ↦ P → M ↦ P
+
+open import Relation.Binary.Reasoning.Base.Partial _↦_ red-trans
+
+ident : Term
+ident = App (App Sop Kop) Kop
+
+ident-red : App ident M ↦ M
+ident-red {M} = begin
+  App (App (App Sop Kop) Kop) M ∼⟨ red-S ⟩
+  App (App Kop M) (App Kop M)   ∼⟨ red-K ⟩
+  M                             ∎
+
+const-sop : Term
+const-sop = App Kop Sop
+
+const-sop-red : App const-sop M ↦ Sop
+const-sop-red = red-K
+
+const-kop : Term
+const-kop = App Kop Kop
+
+const-kop-red : App const-kop M ↦ Kop
+const-kop-red = red-K
+
+app-app : Term → Term → Term
+app-app M N = App (App Sop M) N
+
+app-app-red : App (app-app M₁ M₂) M₃ ↦ App (App M₁ M₃) (App M₂ M₃)
+app-app-red = red-S
+
+lambda : Term → Term
+lambda Ref = ident
+lambda Sop = App Kop Sop
+lambda Kop = App Kop Kop
+lambda (App M N) = app-app (lambda M) (lambda N)
+
+substitution : Term → Term → Term
+substitution Ref N = N
+substitution Sop N = Sop
+substitution Kop N = Kop
+substitution (App M₁ M₂) N = App (substitution M₁ N) (substitution M₂ N)
+
+beta : ∀ M N → (App (lambda M) N) ↦ (substitution M N)
+beta Ref N = ident-red
+beta Sop N = const-sop-red
+beta Kop N = const-kop-red
+beta (App M₁ M₂) N = begin
+  App (app-app (lambda M₁) (lambda M₂)) N     ∼⟨ app-app-red ⟩
+  App (App (lambda M₁) N) (App (lambda M₂) N) ∼⟨ red-left (beta M₁ N) ⟩
+  App (substitution M₁ N) (App (lambda M₂) N) ∼⟨ red-right (beta M₂ N) ⟩
+  App (substitution M₁ N) (substitution M₂ N) ∎
diff --git a/src/Problem12.agda b/src/Problem12.agda
new file mode 100644
index 0000000..5c147a2
--- /dev/null
+++ b/src/Problem12.agda
@@ -0,0 +1,459 @@
+module Problem12 where
+
+open import Axiom.UniquenessOfIdentityProofs using (UIP; module Decidable⇒UIP)
+open import Data.Bool  hiding (_≟_)
+open import Data.Empty using (⊥-elim)
+open import Data.Fin hiding (_+_)
+import Data.Fin.Properties as Fin
+open import Data.List
+open import Data.List.Membership.Propositional
+open import Data.List.Membership.Propositional.Properties
+open import Data.List.Properties
+open import Data.List.Relation.Unary.Any using (here; there; satisfied)
+open import Data.Nat using (ℕ;zero;suc;_*_; _+_)
+open import Data.Nat.Properties hiding (_≟_)
+open import Data.Product hiding (map)
+open import Data.Sum hiding (map)
+open import Function.Base using (_∘′_)
+open import Function.Bundles using (Injection; _↣_; _↔_; mk↣; mk↔′)
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+
+-- copied in here because latest stable stdlib doesn't have it??
+_⊎-dec_ : ∀{A B : Set} →  Dec A → Dec B → Dec (A ⊎ B)
+does  (a? ⊎-dec b?) = does a? ∨ does b?
+proof (a? ⊎-dec b?) with proof a?
+... | ofʸ p = ofʸ (inj₁ p)
+... | ofⁿ ¬p with proof b?
+... | ofʸ p = ofʸ (inj₂ p)
+... | ofⁿ ¬p₁ = ofⁿ (λ { (inj₁ q) → ¬p q; (inj₂ q) → ¬p₁ q })
+
+sum-0 : ∀ n → sum (tabulate {n = n} (λ _ → 0)) ≡ 0
+sum-0 zero = refl
+sum-0 (suc n) = sum-0 n
+
+record DisjointPair (A : Set) : Set where
+  field
+    from : A
+    to   : A
+    diff : from ≢ to
+
+record MultiGraph : Set where
+    field
+      #V : ℕ
+    Vertex = Fin #V
+    Edge = DisjointPair Vertex
+    field
+      E  : List Edge
+
+    V : List (Vertex)
+    V = allFin #V
+
+    VertexUIP : UIP Vertex
+    VertexUIP = Decidable⇒UIP.≡-irrelevant _≟_
+
+    Connects : Vertex → Edge → Set
+    Connects v e = DisjointPair.from e ≡ v ⊎ DisjointPair.to e ≡ v
+
+    connects : (v : Vertex) → (e : Edge) → Dec (Connects v e)
+    connects v e = (DisjointPair.from e ≟ v) ⊎-dec (DisjointPair.to e ≟ v)
+
+    connects′ : (e : Edge) → (v : Vertex) → Dec (Connects v e)
+    connects′ e v = connects v e
+
+    degree′ :  (E : List Edge) → Vertex → ℕ
+    degree′ E v = length (filter (connects v) E)
+
+    degree = degree′ E
+
+    open ≡-Reasoning
+
+    degree-split′ :
+      (e : Edge) (E : List Edge) (v : Vertex) →
+      degree′ (e ∷ E) v ≡ degree′ (e ∷ []) v + degree′ E v
+    degree-split′ e E v with does (connects v e)
+    ... | false = refl
+    ... | true  = refl
+
+    degree-split :
+      (e : Edge) (E : List Edge) (V : List Vertex) →
+      sum (map (degree′ (e ∷ E)) V) ≡ sum (map (degree′ (e ∷ [])) V) + sum (map (degree′ E) V)
+    degree-split e E [] = refl
+    degree-split e E (v ∷ V) = begin
+      degree′ (e ∷ E) v + sum (map (degree′ (e ∷ E)) V)                                               ≡⟨ cong₂ _+_ {x = degree′ (e ∷ E) v} {y = degree′ (e ∷ []) v + degree′ E v} (degree-split′ e E v) (degree-split e E V) ⟩
+      (degree′ (e ∷ []) v + degree′ E v) + (sum (map (degree′ (e ∷ [])) V) + sum (map (degree′ E) V)) ≡˘⟨ +-assoc (degree′ (e ∷ []) v + degree′ E v) (sum (map (degree′ (e ∷ [])) V)) (sum (map (degree′ E) V)) ⟩
+      degree′ (e ∷ []) v + degree′ E v + sum (map (degree′ (e ∷ [])) V) + sum (map (degree′ E) V)     ≡⟨ cong (_+ sum (map (degree′ E) V)) (+-assoc (degree′ (e ∷ []) v) (degree′ E v) (sum (map (degree′ (e ∷ [])) V))) ⟩
+      degree′ (e ∷ []) v + (degree′ E v + sum (map (degree′ (e ∷ [])) V)) + sum (map (degree′ E) V)   ≡⟨ cong (λ ◌ → degree′ (e ∷ []) v + ◌ + sum (map (degree′ E) V)) (+-comm (degree′ E v) (sum (map (degree′ (e ∷ [])) V))) ⟩
+      degree′ (e ∷ []) v + (sum (map (degree′ (e ∷ [])) V) + degree′ E v) + sum (map (degree′ E) V)   ≡˘⟨ cong (_+ sum (map (degree′ E) V)) (+-assoc (degree′ (e ∷ []) v) (sum (map (degree′ (e ∷ [])) V)) (degree′ E v)) ⟩
+      degree′ (e ∷ []) v + sum (map (degree′ (e ∷ [])) V) + degree′ E v + sum (map (degree′ E) V)     ≡⟨ +-assoc (degree′ (e ∷ []) v + sum (map (degree′ (e ∷ [])) V)) (degree′ E v) (sum (map (degree′ E) V)) ⟩
+      (degree′ (e ∷ []) v + sum (map (degree′ (e ∷ [])) V)) + (degree′ E v + sum (map (degree′ E) V)) ∎
+
+
+    degree-flip : (e : Edge) (V : List Vertex) → sum (map (degree′ (e ∷ [])) V) ≡ length (filter (connects′ e) V)
+    degree-flip e [] = refl
+    degree-flip e (v ∷ V) with does (connects v e)
+    ... | false = degree-flip e V
+    ... | true  = cong suc (degree-flip e V)
+
+    module _ where
+      degree-[_]′ : (e : Edge) → (∃[ k ] k ∈ filter (connects′ e) V) ↔ Fin 2
+      degree-[ e ]′ = mk↔′ from to from-to to-from
+        where
+        from : ∃[ k ] k ∈ filter (connects′ e) V → Fin 2
+        from (k , prf) with does (DisjointPair.from e ≟ k)
+        ... | true  = zero
+        ... | false = suc zero
+
+        to : Fin 2 → ∃[ k ] k ∈ filter (connects′ e) V
+        to zero = DisjointPair.from e , ∈-filter⁺ (connects′ e) (∈-allFin _) (inj₁ refl)
+        to (suc zero) = DisjointPair.to e , ∈-filter⁺ (connects′ e) (∈-allFin _) (inj₂ refl)
+
+        from-to : (x : Fin 2) → from (to x) ≡ x
+        from-to zero with DisjointPair.from e ≟ DisjointPair.from e
+        ... | yes _  = refl
+        ... | no x≢x = ⊥-elim (x≢x refl)
+        from-to (suc zero) with DisjointPair.from e ≟ DisjointPair.to e
+        ... | yes x≡y = ⊥-elim (DisjointPair.diff e x≡y)
+        ... | no _    = refl
+
+        open Injection using (injective) renaming (f to _⟨$⟩_)
+
+        -- The only use of axiom K
+        ∈-tabulate-unique :
+          {n : ℕ} {A : Set} (uip : UIP A) (f : Fin n ↣ A) {x : A} (p q : x ∈ tabulate (f ⟨$⟩_)) → p ≡ q
+        ∈-tabulate-unique {suc n} uip f (here p)    (here q)    = cong here (uip p q)
+        ∈-tabulate-unique {suc n} uip f (here refl) (there q)   = ⊥-elim (0≢1+n (cong toℕ (injective f (proj₂ (∈-tabulate⁻ q)))))
+        ∈-tabulate-unique {suc n} uip f (there p)   (here refl) = ⊥-elim (0≢1+n (cong toℕ (injective f (proj₂ (∈-tabulate⁻ p)))))
+        ∈-tabulate-unique {suc n} uip f (there p)   (there q)   = cong there (∈-tabulate-unique uip (mk↣ (Fin.suc-injective ∘′ injective f)) p q)
+
+        postulate
+          filter⁺-filter⁻ :
+            {A : Set} {P : A → Set} (P? : ∀ x → Dec (P x)) →
+            {v : A} (xs : List A) (i : v ∈ filter P? xs) →
+            uncurry (∈-filter⁺ P? {xs = xs}) (∈-filter⁻ P? i) ≡ i
+
+        to-from : (x : ∃[ k ] k ∈ filter (connects′ e) V) → to (from x) ≡ x
+        to-from (k , prf) with DisjointPair.from e ≟ k
+        to-from (k , prf) | yes refl  with ∈-filter⁻ (connects′ e) {xs = V} prf in filter⁻-eq
+        ... | k∈allFin , inj₁ p = cong (_ ,_) (begin
+          ∈-filter⁺ (connects′ e) (∈-allFin _) (inj₁ refl)                         ≡⟨ cong (λ ◌ → ∈-filter⁺ (connects′ e) ◌ (inj₁ refl)) (∈-tabulate-unique VertexUIP (mk↣ (λ eq → eq)) _ _) ⟩
+          ∈-filter⁺ (connects′ e) k∈allFin (inj₁ refl)                             ≡⟨ cong (∈-filter⁺ (connects′ e) k∈allFin ∘′ inj₁) (VertexUIP refl p) ⟩
+          ∈-filter⁺ (connects′ e) k∈allFin (inj₁ p)                                ≡˘⟨ cong (uncurry (∈-filter⁺ (connects′ e))) filter⁻-eq ⟩
+          uncurry (∈-filter⁺ (connects′ e) {xs = V}) (∈-filter⁻ (connects′ e) prf) ≡⟨ filter⁺-filter⁻ (connects′ e) V prf ⟩
+          prf                                                                      ∎)
+        ... | k∈allFin , inj₂ k≡to = ⊥-elim (DisjointPair.diff e (sym k≡to))
+        to-from (k , prf) | no k≢from with ∈-filter⁻ (connects′ e) {xs = V} prf in filter⁻-eq
+        ... | k∈allFin , inj₁ k≡from = ⊥-elim (k≢from k≡from)
+        ... | k∈allFin , inj₂ refl = cong (_ ,_) (begin
+          ∈-filter⁺ (connects′ e) (∈-allFin _) (inj₂ refl)                         ≡⟨ cong (λ ◌ → ∈-filter⁺ (connects′ e) ◌ (inj₂ refl)) (∈-tabulate-unique VertexUIP (mk↣ (λ eq → eq)) _ _) ⟩
+          ∈-filter⁺ (connects′ e) k∈allFin (inj₂ refl)                             ≡˘⟨ cong (uncurry (∈-filter⁺ (connects′ e))) filter⁻-eq ⟩
+          uncurry (∈-filter⁺ (connects′ e) {xs = V}) (∈-filter⁻ (connects′ e) prf) ≡⟨ filter⁺-filter⁻ (connects′ e) V prf ⟩
+          prf                                                                      ∎)
+
+    postulate
+      degree-[_] : (e : Edge) → sum (map (degree′ (e ∷ [])) V) ≡ 2
+
+    handshaking′ : (E : List Edge) → sum (map (degree′ E) V) ≡ 2 * length E
+    handshaking′ [] = begin
+      sum (map (λ i → 0) V)             ≡⟨ cong sum (map-tabulate {n = #V} (λ i → i) (λ _ → 0)) ⟩
+      sum (tabulate {n = #V} (λ i → 0)) ≡⟨ sum-0 #V ⟩
+      0                        ∎
+    handshaking′ (e ∷ E) = begin
+      sum (map (degree′ (e ∷ E)) V)                            ≡⟨ degree-split e E V ⟩
+      sum (map (degree′ (e ∷ [])) V) + sum (map (degree′ E) V) ≡⟨ cong₂ _+_ degree-[ e ] (handshaking′ E) ⟩
+      2 + 2 * length E                                         ≡˘⟨ *-distribˡ-+ 2 1 (length E) ⟩
+      2 * (1 + length E)                                       ∎
+
+    handshaking : sum (map degree V) ≡ 2 * length E
+    handshaking = handshaking′ E
+
+-- open import Data.Bool using (_∨_)
+-- open import Data.Empty using (⊥-elim)
+-- open import Data.Fin as Fin hiding (_+_)
+-- import Data.Fin.Properties as Fin
+-- open import Data.List as List hiding (map)
+-- open import Data.List.Properties
+-- open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; []; _∷_)
+-- import Data.List.Relation.Binary.Permutation.Setoid as Permutation
+-- import Data.List.Relation.Binary.Permutation.Setoid.Properties as Permutation′
+-- open import Data.Nat using (ℕ; zero; suc; s≤s; _*_; _+_)
+-- open import Data.Nat.Properties hiding (_≟_)
+-- open import Data.Product hiding (map)
+-- open import Data.Sum hiding (map)
+-- open import Data.Vec as Vec using (Vec; []; _∷_)
+
+-- open import Function.Base using (_∘′_; _|>_)
+-- open import Function.Bundles using (Injection; _↣_; mk↣)
+
+-- -- open import Relation.Binary.Consequences u
+-- open import Relation.Binary.Bundles using (Setoid)
+-- open import Relation.Binary.Definitions using (Irreflexive; Trichotomous; tri<; tri≈; tri>)
+-- open import Relation.Binary.PropositionalEquality
+-- open import Relation.Nullary
+
+-- -- copied in here because latest stable stdlib doesn't have it??
+-- _⊎-dec_ : ∀{A B : Set} →  Dec A → Dec B → Dec (A ⊎ B)
+-- does  (a? ⊎-dec b?) = does a? ∨ does b?
+-- proof (a? ⊎-dec b?) with proof a?
+-- ... | ofʸ p = ofʸ (inj₁ p)
+-- ... | ofⁿ ¬p with proof b?
+-- ... | ofʸ p = ofʸ (inj₂ p)
+-- ... | ofⁿ ¬p₁ = ofⁿ (λ { (inj₁ q) → ¬p q; (inj₂ q) → ¬p₁ q })
+
+-- infix 6 _⨾_⨾_
+
+-- record DisjointPair (A : Set) : Set where
+--   constructor _⨾_⨾_
+--   field
+--     from : A
+--     to   : A
+--     diff : from ≢ to
+
+-- data _≐_ {A : Set} : DisjointPair A → DisjointPair A → Set where
+--   refl      : ∀ {x y diff diff′} → (x ⨾ y ⨾ diff) ≐ (x ⨾ y ⨾ diff′)
+--   transpose : ∀ {x y diff diff′} → (x ⨾ y ⨾ diff) ≐ (y ⨾ x ⨾ diff′)
+
+-- ≐-setoid : (A : Set) → Setoid _ _
+-- ≐-setoid A = record
+--   { Carrier = DisjointPair A
+--   ; _≈_     = _≐_
+--   ; isEquivalence = record
+--     { refl  = refl
+--     ; sym   = (λ { refl → refl ; transpose → transpose })
+--     ; trans = λ
+--       { refl      refl      → refl
+--       ; refl      transpose → transpose
+--       ; transpose refl      → transpose
+--       ; transpose transpose → refl
+--       }
+--     }
+--   }
+
+-- -- Variant of DisjointPair for forcing an order
+
+-- record OrderedPair (A : Set) (_<_ : A → A → Set) : Set where
+--   constructor _⨾_⨾_
+--   field
+--     from : A
+--     to   : A
+--     ord  : from < to
+
+-- module Pair where
+--   open DisjointPair
+--   open Injection renaming (f to _⟨$⟩_)
+
+--   map : {A B : Set} → A ↣ B → DisjointPair A → DisjointPair B
+--   map f p .from = f ⟨$⟩ p .from
+--   map f p .to   = f ⟨$⟩ p .to
+--   map f p .diff = p .diff ∘′ injective f
+
+--   order :
+--     {A : Set} {_<_ : A → A → Set} →
+--     Trichotomous _≡_ _<_ → DisjointPair A → OrderedPair A _<_
+--   order compare (from ⨾ to ⨾ diff) with compare from to
+--   ... | tri< f<t _   _   = from ⨾ to ⨾ f<t
+--   ... | tri≈ _   f≡t _   = ⊥-elim (diff f≡t)
+--   ... | tri> _   _   f>t = to ⨾ from ⨾ f>t
+
+--   forget :
+--     {A : Set} {_<_ : A → A → Set} →
+--     Irreflexive _≡_ _<_ → OrderedPair A _<_ → DisjointPair A
+--   forget irrefl (from ⨾ to ⨾ ord) = from ⨾ to ⨾ λ eq → irrefl eq ord
+
+--   forget∘order :
+--     {A : Set} {_<_ : A → A → Set} →
+--     (cmp : Trichotomous _≡_ _<_) (irrefl : Irreflexive _≡_ _<_) (p : DisjointPair A) →
+--     forget irrefl (order cmp p) ≐ p
+--   forget∘order cmp irrefl (from ⨾ to ⨾ diff) with cmp from to
+--   ... | tri< f<t _   _   = refl
+--   ... | tri≈ _   f≡t _   = ⊥-elim (diff f≡t)
+--   ... | tri> _   _   f>t = transpose
+
+-- -- Multigraphs built inductively
+
+-- private
+--   variable n : ℕ
+
+--   Vertex : ℕ → Set
+--   Vertex = Fin
+
+--   Edge : ℕ → Set
+--   Edge n = DisjointPair (Vertex n)
+
+--   OEdge : ℕ → Set
+--   OEdge n = OrderedPair (Vertex n) _<_
+
+--   open module ↭′ n = Permutation (≐-setoid (Vertex n)) using () renaming (_↭_ to [_]_↭_)
+--   open module ↭′′ {n} = Permutation (≐-setoid (Vertex n)) hiding (_↭_)
+--   module ↭ {n} = Permutation′ (≐-setoid (Vertex n))
+
+-- module Graph where
+--   data Graph : ℕ → Set where
+--     []  : Graph 0
+--     _∷_ : Vec ℕ n → Graph n → Graph (suc n)
+
+--   -- Empty graph
+--   empty : (n : ℕ) → Graph n
+--   empty zero = []
+--   empty (suc n) = Vec.replicate 0 ∷ empty n
+
+--   -- Obtain list of edges
+
+--   edges′′ : ∀ {k} → Vec ℕ n → Vec (Vertex k) n → List (Edge (suc k))
+--   edges′′ es is =
+--     Vec.zipWith (λ n i → replicate n (zero ⨾ suc i ⨾ λ ())) es is |>
+--     Vec.toList |>
+--     concat
+
+--   edges′ : Vec ℕ n → List (Edge (suc n))
+--   edges′ es = edges′′ es (Vec.allFin _)
+
+--   step-edges : List (Edge n) → List (Edge (suc n))
+--   step-edges = List.map (Pair.map (mk↣ Fin.suc-injective))
+
+--   edges : Graph n → List (Edge n)
+--   edges [] = []
+--   edges (es ∷ g) = edges′ es ++ step-edges (edges g)
+
+--   -- Degree of a node
+
+--   degree : Graph n → Vertex n → ℕ
+--   degree (es ∷ g) zero    = Vec.sum es
+--   degree (es ∷ g) (suc i) = Vec.lookup es i + degree g i
+
+--   -- Easy version of handshaking
+
+--   Handshake : Graph n → Set
+--   Handshake {n} g = sum (List.map (degree g) (allFin n)) ≡ 2 * length (edges g)
+
+--   handshaking-empty : (n : ℕ) → Handshake (empty n)
+--   handshaking-empty zero = refl
+--   handshaking-empty (suc n) = {!begin
+--     Vec.sum ? + sum (List.map (degree (Vec.replicate 0))) ≡⟨ ? ⟩
+--     ? ∎!}
+--     where open ≡-Reasoning
+--   -- handshaking : (g : Graph n) → sum (List.map (degree g) (allFin n)) ≡ 2 * length (edges g)
+--   -- handshaking [] = refl
+--   -- handshaking (es ∷ g) = {!begin
+--   --   Vec.sum es + sum (List.map (degree (es ∷ g) ))!}
+--   --   where open ≡-Reasoning
+
+--   -- Add an edge to a graph
+
+--   infixr 5 _∷ᵉ_
+
+--   _∷ᵉ_ : OEdge n → Graph n → Graph n
+--   (zero ⨾ suc to ⨾ ord) ∷ᵉ (xs ∷ g) = xs Vec.[ to ]%= suc ∷ g
+--   (suc from ⨾ suc to ⨾ s≤s ord) ∷ᵉ (xs ∷ g) = xs ∷ (from ⨾ to ⨾ ord ∷ᵉ g)
+
+--   -- Construction from edges
+
+--   private
+--     order′ : Edge n → OEdge n
+--     order′ = Pair.order Fin.<-cmp
+
+--     forget′ : OEdge n → Edge n
+--     forget′ = Pair.forget Fin.<-irrefl
+
+--     forget′∘order′ : (e : Edge n) → forget′ (order′ e) ≐ e
+--     forget′∘order′ = Pair.forget∘order Fin.<-cmp Fin.<-irrefl
+
+--   fromEdges : List (Edge n) → Graph n
+--   fromEdges es = foldr (λ e g → order′ e ∷ᵉ g) (empty _) es
+
+--   step-edges-↭ :
+--     {es es′ : List (Edge n)} →
+--     [ n ] es ↭ es′ → [ suc n ] step-edges es ↭ step-edges es′
+--   step-edges-↭ es↭es′ =
+--     ↭.map⁺ (≐-setoid (Vertex (suc _))) (λ { refl → refl ; transpose → transpose }) es↭es′
+
+--   edges′′⁻¹-[] : ∀ {k n} (is : Vec (Vertex n) k) → edges′′ (Vec.replicate 0) is ≡ []
+--   edges′′⁻¹-[] [] = refl
+--   edges′′⁻¹-[] (i ∷ is) = edges′′⁻¹-[] is
+
+--   edges′′⁻¹-∷ : ∀ {k n} (es : Vec ℕ k) (is : Vec (Vertex n) k) (j : Fin k) →
+--     [ suc n ]
+--       edges′′ (es Vec.[ j ]%= suc) is
+--     ↭
+--       (zero ⨾ suc (Vec.lookup is j) ⨾ λ ()) ∷ edges′′ es is
+--   edges′′⁻¹-∷ (e ∷ es) (i ∷ is) zero    = ↭-refl
+--   edges′′⁻¹-∷ (e ∷ es) (i ∷ is) (suc j) = begin
+--     edges′′ (e ∷ es Vec.[ j ]%= suc) (i ∷ is)                                ≡⟨⟩
+--     replicate e (zero ⨾ suc i ⨾ λ ()) ++ edges′′ (es Vec.[ j ]%= suc) is      ↭⟨ ↭.++⁺ˡ (replicate e (zero ⨾ suc i ⨾ λ ())) (edges′′⁻¹-∷ es is j) ⟩
+--     replicate e (zero ⨾ suc i ⨾ λ ()) ++ (zero ⨾ suc k ⨾ λ ()) ∷ edges′′ es is ↭⟨ ↭.↭-shift (replicate e (zero ⨾ suc i ⨾ λ ())) (edges′′ es is) ⟩
+--     (zero ⨾ suc k ⨾ λ ()) ∷ replicate e (zero ⨾ suc i ⨾ λ ()) ++ edges′′ es is ≡⟨⟩
+--     (zero ⨾ suc k ⨾ λ ()) ∷ edges′′ (e ∷ es) (i ∷ is) ∎
+--     where
+--     open PermutationReasoning
+--     k = Vec.lookup is j
+
+--   edges′⁻¹-[] : (n : ℕ) → edges′ {n} (Vec.replicate 0) ≡ []
+--   edges′⁻¹-[] n = edges′′⁻¹-[] (Vec.allFin n)
+
+--   edges′⁻¹-∷ :
+--     (es : Vec ℕ n) (to : Vertex n) →
+--     [ suc n ] edges′ (es Vec.[ to ]%= suc) ↭ (zero ⨾ suc to ⨾ λ ()) ∷ edges′ es
+--   edges′⁻¹-∷ es to = begin
+--     edges′ (es Vec.[ to ]%= suc)                                  ↭⟨ edges′′⁻¹-∷ es (Vec.allFin _) to ⟩
+--     (zero ⨾ suc (Vec.lookup (Vec.allFin _) to) ⨾ λ ()) ∷ edges′ es ≡⟨ cong (λ ◌ → (zero ⨾ suc ◌ ⨾ (λ ())) ∷ edges′ es) (Vec-lookup-tabulate (λ i → i) to) ⟩
+--     (zero ⨾ suc to ⨾ λ ()) ∷ edges′ es                             ∎
+--     where
+--     open PermutationReasoning
+--     Vec-lookup-tabulate :
+--       {A : Set} (f : Fin n → A) (i : Fin n) → Vec.lookup (Vec.tabulate f) i ≡ f i
+--     Vec-lookup-tabulate f zero    = refl
+--     Vec-lookup-tabulate f (suc i) = Vec-lookup-tabulate (f ∘′ suc) i
+
+--   edges⁻¹-[] : (n : ℕ) → edges (empty n) ≡ []
+--   edges⁻¹-[] zero = refl
+--   edges⁻¹-[] (suc n) = cong₂ (λ ◌ᵃ ◌ᵇ → ◌ᵃ ++ step-edges ◌ᵇ) (edges′⁻¹-[] n) (edges⁻¹-[] n)
+
+--   edges⁻¹-∷ : (e : OEdge n) (g : Graph n) → [ n ] edges (e ∷ᵉ g) ↭ forget′ e ∷ edges g
+--   edges⁻¹-∷ (zero ⨾ suc to ⨾ ord)         (xs ∷ g) = ↭.++⁺ʳ (step-edges (edges g)) (begin
+--     edges′ (xs Vec.[ to ]%= suc)   ↭⟨ edges′⁻¹-∷ xs to ⟩
+--     (zero ⨾ suc to ⨾ _ ∷ edges′ xs) ≋⟨ refl ∷ Pointwise.refl refl ⟩
+--     zero ⨾ suc to ⨾ _ ∷ edges′ xs   ∎)
+--     where open PermutationReasoning
+--   edges⁻¹-∷ (suc from ⨾ suc to ⨾ s≤s ord) (xs ∷ g) = begin
+--     edges′ xs ++ step-edges (edges (from ⨾ to ⨾ ord ∷ᵉ g))      ↭⟨ ↭.++⁺ˡ (edges′ xs) (step-edges-↭ (edges⁻¹-∷ (from ⨾ to ⨾ ord) g)) ⟩
+--     edges′ xs ++ step-edges (from ⨾ to ⨾ diff ∷ edges g)        ≡⟨⟩
+--     edges′ xs ++ (suc from ⨾ suc to ⨾ _) ∷ step-edges (edges g) ↭⟨ ↭.↭-shift (edges′ xs) (step-edges (edges g)) ⟩
+--     (suc from ⨾ suc to ⨾ _ ∷ edges′ xs ++ step-edges (edges g)) ≋⟨ refl ∷ Pointwise.refl refl ⟩
+--     suc from ⨾ suc to ⨾ _ ∷ edges′ xs ++ step-edges (edges g)   ∎
+--     where
+--     open PermutationReasoning
+--     diff = λ eq → Fin.<-irrefl eq ord
+
+--   edges⁻¹ : (es : List (Edge n)) → [ n ] edges (fromEdges es) ↭ es
+--   edges⁻¹ [] = ↭-reflexive (edges⁻¹-[] _)
+--   edges⁻¹ (e ∷ es) = begin
+--     edges (order′ e ∷ᵉ fromEdges es)            ↭⟨ edges⁻¹-∷ (order′ e) (fromEdges es) ⟩
+--     (forget′ (order′ e) ∷ edges (fromEdges es)) ≋⟨ forget′∘order′ e ∷ Pointwise.refl refl ⟩
+--     e ∷ edges (fromEdges es)                    <⟨ edges⁻¹ es ⟩
+--     e ∷ es                                      ∎
+--     where open PermutationReasoning
+
+-- -- Multigraphs as defined by the problem
+-- -- I've rearranged the definitions to make things easier to prove
+
+-- Connects : Vertex n → Edge n → Set
+-- Connects v e = DisjointPair.from e ≡ v ⊎ DisjointPair.to e ≡ v
+
+-- connects : (v : Vertex n) → (e : Edge n) → Dec (Connects v e)
+-- connects v e = (DisjointPair.from e ≟ v) ⊎-dec (DisjointPair.to e ≟ v)
+
+-- degree′ :  (E : List (Edge n)) → Vertex n → ℕ
+-- degree′ E v = length (filter (connects v) E)
+
+-- record MultiGraph : Set where
+--     field
+--       #V : ℕ
+--       E  : List (Edge #V)
+
+--     V : List (Vertex #V)
+--     V = allFin #V
+
+--     degree = degree′ E
+
+--     handshaking : sum (List.map degree V) ≡ 2 * length E
+--     handshaking = {!!}
diff --git a/src/Problem13.agda b/src/Problem13.agda
new file mode 100644
index 0000000..53cc178
--- /dev/null
+++ b/src/Problem13.agda
@@ -0,0 +1,93 @@
+{-# OPTIONS --safe #-}
+
+module Problem13 where
+
+open import Data.Empty using (⊥-elim)
+open import Data.Fin hiding (_≟_; _+_; _<_; _>_; _≤_)
+open import Data.Fin.Properties hiding (_≟_; ≤-trans)
+open import Data.Nat
+open import Data.Nat.DivMod
+open import Data.Nat.Properties
+open import Data.Product
+open import Data.Unit using (tt)
+open import Data.Vec
+open import Function.Base using (_$′_)
+open import Relation.Nullary.Decidable
+open import Relation.Binary.PropositionalEquality
+
+open ≤-Reasoning renaming (begin_ to begin-≤_)
+
+okToDivide : ∀ n → n > 1 → False (n ≟ 0)
+okToDivide (suc n) p = tt
+
+toRadix : (n : ℕ)(nz : n > 1) → (f : ℕ) → ℕ → Vec (Fin n) f
+toRadix n nz zero k = []
+toRadix n nz (suc f) k with (k divMod n) {okToDivide _ nz}
+... | result q r prf₂ = r ∷ toRadix n nz f q
+
+fromRadix : (n : ℕ) {f : ℕ} → Vec (Fin n) f → ℕ
+fromRadix n [] = 0
+fromRadix n (x ∷ xs) = toℕ x + n * fromRadix n xs
+
+goal₁ : (n : ℕ)(nz : n > 1){f : ℕ}(num : Vec (Fin n) f)
+      → toRadix n nz f (fromRadix n num) ≡ num
+goal₁ n nz [] = refl
+goal₁ n nz (x ∷ xs) with ((toℕ x + n * fromRadix n xs) divMod n) {okToDivide _ nz}
+... | result q r prf =
+  let (prf₁ , prf₂) = invertProof x r (fromRadix n xs) q prf in
+  cong₂ _∷_ (sym prf₁) (trans (sym (cong (toRadix n nz _) prf₂)) (goal₁ n nz xs))
+  where
+  invertProof : (x y : Fin n) (p q : ℕ) → toℕ x + n * p ≡ toℕ y + q * n → x ≡ y × p ≡ q
+  invertProof x y zero zero    prf .proj₁ =
+    toℕ-injective $′ +-cancelʳ-≡ (toℕ x) (toℕ y) $′ begin-equality
+      toℕ x + n * zero ≡⟨  prf ⟩
+      toℕ y + zero     ≡˘⟨ cong (toℕ y +_) (*-zeroʳ n) ⟩
+      toℕ y + n * zero ∎
+  invertProof x y zero zero    prf .proj₂ = refl
+  invertProof x y zero (suc q) prf =
+    ⊥-elim $′ <⇒≱ (toℕ<n x) $′ begin-≤
+               n          ≤⟨  m≤m+n n (q * n) ⟩
+               n + q * n  ≤⟨  m≤n+m (n + q * n) (toℕ y) ⟩
+      toℕ y + (n + q * n) ≡˘⟨ prf ⟩
+      toℕ x + n * zero    ≡⟨  cong (toℕ x +_) (*-zeroʳ n) ⟩
+      toℕ x + zero        ≡⟨  +-identityʳ (toℕ x) ⟩
+      toℕ x               ∎
+  invertProof x y (suc p) zero    prf =
+    ⊥-elim $′ <⇒≱ (toℕ<n y) $′ begin-≤
+               n          ≤⟨ m≤m+n n (p * n) ⟩
+               n + p * n  ≡⟨ *-comm (suc p) n ⟩
+               n * suc p  ≤⟨ m≤n+m (n * suc p) (toℕ x) ⟩
+      toℕ x + (n * suc p) ≡⟨ prf ⟩
+      toℕ y + zero        ≡⟨ +-identityʳ (toℕ y) ⟩
+      toℕ y               ∎
+  invertProof x y (suc p) (suc q) prf =
+    map₂ (cong suc) $′
+    invertProof x y p q $′
+    +-cancelʳ-≡ (toℕ x + n * p) (toℕ y + q * n) $′ begin-equality
+      toℕ x +  n * p + n  ≡⟨  +-assoc (toℕ x) (n * p) n ⟩
+      toℕ x + (n * p + n) ≡⟨  cong (λ ◌ → toℕ x + (◌ + n)) (*-comm n p) ⟩
+      toℕ x + (p * n + n) ≡⟨  cong (toℕ x +_) (+-comm (p * n) n) ⟩
+      toℕ x + (n + p * n) ≡⟨  cong (toℕ x +_) (*-comm (suc p) n) ⟩
+      toℕ x + (n * suc p) ≡⟨  prf ⟩
+      toℕ y + (n + q * n) ≡⟨  cong (toℕ y +_) (+-comm n (q * n)) ⟩
+      toℕ y + (q * n + n) ≡˘⟨ +-assoc (toℕ y) (q * n) n ⟩
+      toℕ y +  q * n + n  ∎
+
+
+goal₂ : (n : ℕ)(nz : n > 1)(f : ℕ)(k : ℕ)(p : k < n ^ f)
+      → fromRadix n (toRadix n nz f k) ≡ k
+goal₂ n nz zero    k k<n^0   = sym $′ n<1⇒n≡0 k<n^0
+goal₂ n nz (suc f) k k<n*n^f with (k divMod n) {okToDivide _ nz}
+... | result q r prf = begin-equality
+  toℕ r + n * fromRadix n (toRadix n nz f q) ≡⟨  cong (λ ◌ → toℕ r + n * ◌) (goal₂ n nz f q q<n^f) ⟩
+  toℕ r + n * q                              ≡⟨  cong (toℕ r +_) (*-comm n q) ⟩
+  toℕ r + q * n                              ≡˘⟨ prf ⟩
+  k                                          ∎
+  where
+  q<n^f : q < n ^ f
+  q<n^f = *-cancelˡ-< n $′ begin-strict
+            n * q ≡⟨  *-comm n q ⟩
+            q * n ≤⟨  m≤n+m (q * n) (toℕ r) ⟩
+    toℕ r + q * n ≡˘⟨ prf ⟩
+    k             <⟨  k<n*n^f ⟩
+    n * n ^ f     ∎
diff --git a/src/Problem14.agda b/src/Problem14.agda
new file mode 100644
index 0000000..d6a9309
--- /dev/null
+++ b/src/Problem14.agda
@@ -0,0 +1,123 @@
+module Problem14 where
+
+open import Relation.Binary.PropositionalEquality
+open import Data.Product
+open import Data.Sum
+open import Data.Nat
+open import Data.Nat.Properties
+open import Data.List
+open import Data.Bool
+
+open ≡-Reasoning
+
+postulate A : Set
+postulate _⋆_ : A → A → A
+postulate ι : A
+infixl 50 _⋆_
+postulate ⋆-assoc : ∀ a b c → a ⋆ (b ⋆ c) ≡ a ⋆ b ⋆ c
+postulate ⋆-identityʳ : ∀ y → y ⋆ ι ≡ y
+postulate ⋆-identityˡ : ∀ y → ι ⋆ y ≡ y
+
+_⋆⋆_ : A → ℕ → A
+n ⋆⋆ zero = ι
+n ⋆⋆ suc k = n ⋆ (n ⋆⋆ k)
+
+⋆⋆-homoʳ : (x : A) (n k : ℕ) → x ⋆⋆ (n + k) ≡ (x ⋆⋆ n) ⋆ (x ⋆⋆ k)
+⋆⋆-homoʳ x zero    k = sym (⋆-identityˡ (x ⋆⋆ k))
+⋆⋆-homoʳ x (suc n) k = begin
+  x ⋆ (x ⋆⋆ (n + k))        ≡⟨ cong (x ⋆_) (⋆⋆-homoʳ x n k) ⟩
+  x ⋆ ((x ⋆⋆ n) ⋆ (x ⋆⋆ k)) ≡⟨ ⋆-assoc x (x ⋆⋆ n) (x ⋆⋆ k) ⟩
+  x ⋆  (x ⋆⋆ n) ⋆ (x ⋆⋆ k)  ∎
+
+⋆⋆-comm : (x : A) (k : ℕ) → (x ⋆⋆ k) ⋆ x ≡ x ⋆ (x ⋆⋆ k)
+⋆⋆-comm x k = begin
+  (x ⋆⋆ k) ⋆ x        ≡˘⟨ cong ((x ⋆⋆ k) ⋆_) (⋆-identityʳ x) ⟩
+  (x ⋆⋆ k) ⋆ (x ⋆⋆ 1) ≡˘⟨ ⋆⋆-homoʳ x k 1 ⟩
+  x ⋆⋆ (k + 1)        ≡⟨  cong (x ⋆⋆_) (+-comm k 1) ⟩
+  x ⋆⋆ (1 + k)        ∎
+
+fromBits : List Bool → ℕ
+fromBits [] = 0
+fromBits (false ∷ bs) = 2 * fromBits bs
+fromBits (true ∷ bs) = 1 + 2 * fromBits bs
+
+expBySquare : A → A → List Bool → A
+expBySquare y x [] = y
+expBySquare y x (false ∷ n) = expBySquare y (x ⋆ x) n
+expBySquare y x (true ∷ n)  = expBySquare (y ⋆ x) (x ⋆ x) n
+
+expBySquare-homoˡ :
+  (x y z : A) (n : List Bool) →
+  expBySquare (x ⋆ y) z n ≡ x ⋆ expBySquare y z n
+expBySquare-homoˡ x y z []          = refl
+expBySquare-homoˡ x y z (false ∷ n) = expBySquare-homoˡ x y (z ⋆ z) n
+expBySquare-homoˡ x y z (true  ∷ n) = begin
+  expBySquare (x ⋆  y ⋆ z)  (z ⋆ z) n ≡˘⟨ cong (λ ◌ → expBySquare ◌ (z ⋆ z) n) (⋆-assoc x y z) ⟩
+  expBySquare (x ⋆ (y ⋆ z)) (z ⋆ z) n ≡⟨  expBySquare-homoˡ x (y ⋆ z) (z ⋆ z) n ⟩
+  x  ⋆ expBySquare (y ⋆ z)  (z ⋆ z) n ∎
+
+-- Special case of commutativity
+expBySquare-comm :
+  (x : A) (k : ℕ) (n : List Bool) →
+  expBySquare ι (x ⋆⋆ k) n ⋆ x ≡ expBySquare x (x ⋆⋆ k) n
+expBySquare-comm x k []          = ⋆-identityˡ x
+expBySquare-comm x k (false ∷ n) = begin
+  expBySquare ι ((x ⋆⋆ k) ⋆ (x ⋆⋆ k)) n ⋆ x ≡˘⟨ cong (λ ◌ → expBySquare ι ◌ n ⋆ x) (⋆⋆-homoʳ x k k) ⟩
+  expBySquare ι (x ⋆⋆ (k + k))        n ⋆ x ≡⟨  expBySquare-comm x (k + k) n ⟩
+  expBySquare x (x ⋆⋆ (k + k))        n     ≡⟨  cong (λ ◌ → expBySquare x ◌ n) (⋆⋆-homoʳ x k k) ⟩
+  expBySquare x ((x ⋆⋆ k) ⋆ (x ⋆⋆ k)) n     ∎
+expBySquare-comm x k (true  ∷ n) = begin
+  expBySquare (ι ⋆ (x ⋆⋆ k)) ((x ⋆⋆ k) ⋆ (x ⋆⋆ k)) n ⋆ x  ≡⟨  cong (λ ◌ → expBySquare ◌ ((x ⋆⋆ k) ⋆ (x ⋆⋆ k)) n ⋆ x) (⋆-identityˡ (x ⋆⋆ k)) ⟩
+  expBySquare (x ⋆⋆ k)       ((x ⋆⋆ k) ⋆ (x ⋆⋆ k)) n ⋆ x  ≡˘⟨ cong₂ (λ ◌ᵃ ◌ᵇ → expBySquare ◌ᵃ ◌ᵇ n ⋆ x) (⋆-identityʳ (x ⋆⋆ k)) (⋆⋆-homoʳ x k k) ⟩
+  expBySquare ((x ⋆⋆ k) ⋆ ι) (x ⋆⋆ (k + k))        n ⋆ x  ≡⟨  cong (_⋆ x) (expBySquare-homoˡ (x ⋆⋆ k) ι (x ⋆⋆ (k + k)) n) ⟩
+  (x ⋆⋆ k) ⋆   expBySquare ι (x ⋆⋆ (k + k))        n ⋆ x  ≡˘⟨ ⋆-assoc (x ⋆⋆ k) (expBySquare ι (x ⋆⋆ (k + k)) n) x ⟩
+  (x ⋆⋆ k) ⋆  (expBySquare ι (x ⋆⋆ (k + k))        n ⋆ x) ≡⟨  cong ((x ⋆⋆ k) ⋆_) (expBySquare-comm x (k + k) n) ⟩
+  (x ⋆⋆ k) ⋆   expBySquare x (x ⋆⋆ (k + k))        n      ≡˘⟨ expBySquare-homoˡ (x ⋆⋆ k) x (x ⋆⋆ (k + k)) n ⟩
+  expBySquare ((x ⋆⋆ k) ⋆ x) (x ⋆⋆ (k + k))        n      ≡⟨  cong₂ (λ ◌ᵃ ◌ᵇ → expBySquare ◌ᵃ ◌ᵇ n) (⋆⋆-comm x k) (⋆⋆-homoʳ x k k) ⟩
+  expBySquare (x ⋆ (x ⋆⋆ k)) ((x ⋆⋆ k) ⋆ (x ⋆⋆ k)) n      ∎
+
+-- Special case of homomorphism because multiplication isn't commutative
+expBySquare-homoʳ :
+  (x y : A) (n : List Bool) →
+  expBySquare x (y ⋆ y) n ≡ expBySquare x y n ⋆ expBySquare ι y n
+expBySquare-homoʳ x y []          = sym (⋆-identityʳ x)
+expBySquare-homoʳ x y (false ∷ n) = expBySquare-homoʳ x (y ⋆ y) n
+expBySquare-homoʳ x y (true  ∷ n) = begin
+  expBySquare (x ⋆ (y ⋆ y)) (y ⋆ y ⋆ (y ⋆ y)) n                      ≡⟨ expBySquare-homoʳ (x ⋆ (y ⋆ y)) (y ⋆ y) n ⟩
+  expBySquare (x ⋆ (y ⋆ y)) (y ⋆ y) n ⋆ expBySquare ι (y ⋆ y) n      ≡⟨  cong (λ ◌ → expBySquare ◌ (y ⋆ y) n ⋆ expBySquare ι (y ⋆ y) n) (⋆-assoc x y y) ⟩
+  expBySquare ((x ⋆ y) ⋆ y) (y ⋆ y) n ⋆ expBySquare ι (y ⋆ y) n      ≡⟨  cong (_⋆ expBySquare ι (y ⋆ y) n) (expBySquare-homoˡ (x ⋆ y) y (y ⋆ y) n) ⟩
+  (x ⋆ y) ⋆ expBySquare y (y ⋆ y) n ⋆ expBySquare ι (y ⋆ y) n        ≡˘⟨ cong (λ ◌ → x ⋆ y ⋆ expBySquare y (y ⋆ ◌) n ⋆ expBySquare ι (y ⋆ y) n) (⋆-identityʳ y) ⟩
+  (x ⋆ y) ⋆ expBySquare y (y ⋆⋆ 2) n ⋆ expBySquare ι (y ⋆ y) n       ≡˘⟨ cong (λ ◌ → x ⋆ y ⋆ ◌ ⋆ expBySquare ι (y ⋆ y) n) (expBySquare-comm y 2 n) ⟩
+  (x ⋆ y) ⋆ (expBySquare ι (y ⋆⋆ 2) n ⋆ y) ⋆ expBySquare ι (y ⋆ y) n ≡⟨  cong (λ ◌ → x ⋆ y ⋆ (expBySquare ι (y ⋆ ◌) n ⋆ y) ⋆ expBySquare ι (y ⋆ y) n) (⋆-identityʳ y) ⟩
+  (x ⋆ y) ⋆ (expBySquare ι (y ⋆ y) n ⋆ y) ⋆ expBySquare ι (y ⋆ y) n  ≡⟨  cong (_⋆ expBySquare ι (y ⋆ y) n) (⋆-assoc (x ⋆ y) (expBySquare ι (y ⋆ y) n) y) ⟩
+  (x ⋆ y) ⋆ expBySquare ι (y ⋆ y) n ⋆ y ⋆ expBySquare ι (y ⋆ y) n    ≡˘⟨ cong (λ ◌ → ◌ ⋆ y ⋆ expBySquare ι (y ⋆ y) n) (expBySquare-homoˡ (x ⋆ y) ι (y ⋆ y) n) ⟩
+  expBySquare ((x ⋆ y) ⋆ ι) (y ⋆ y) n ⋆ y ⋆ expBySquare ι (y ⋆ y) n  ≡⟨  cong (λ ◌ → expBySquare ◌ (y ⋆ y) n ⋆ y ⋆ expBySquare ι (y ⋆ y) n) (⋆-identityʳ (x ⋆ y)) ⟩
+  expBySquare (x ⋆ y) (y ⋆ y) n ⋆ y ⋆ expBySquare ι (y ⋆ y) n        ≡˘⟨ ⋆-assoc (expBySquare (x ⋆ y) (y ⋆ y) n) y (expBySquare ι (y ⋆ y) n) ⟩
+  expBySquare (x ⋆ y) (y ⋆ y) n ⋆ (y ⋆ expBySquare ι (y ⋆ y) n)      ≡˘⟨ cong (expBySquare (x ⋆ y) (y ⋆ y) n ⋆_) (expBySquare-homoˡ y ι (y ⋆ y) n) ⟩
+  expBySquare (x ⋆ y) (y ⋆ y) n ⋆ expBySquare (y ⋆ ι) (y ⋆ y) n      ≡⟨  cong (λ ◌ → expBySquare (x ⋆ y) (y ⋆ y) n ⋆ expBySquare ◌ (y ⋆ y) n) (⋆-identityʳ y) ⟩
+  expBySquare (x ⋆ y) (y ⋆ y) n ⋆ expBySquare y       (y ⋆ y) n      ≡˘⟨ cong (λ ◌ → expBySquare (x ⋆ y) (y ⋆ y) n ⋆ expBySquare ◌ (y ⋆ y) n) (⋆-identityˡ y) ⟩
+  expBySquare (x ⋆ y) (y ⋆ y) n ⋆ expBySquare (ι ⋆ y) (y ⋆ y) n      ∎
+
+_⋆⋆ᵇ_ : A → List Bool → A
+x ⋆⋆ᵇ n = expBySquare ι x n
+
+⋆⋆ᵇ-homoˡ : (x : A) (n : List Bool) → (x ⋆ x) ⋆⋆ᵇ n ≡ (x ⋆⋆ᵇ n) ⋆ (x ⋆⋆ᵇ n)
+⋆⋆ᵇ-homoˡ x n = expBySquare-homoʳ ι x n
+
+proof-lemma : ∀ x n → x ⋆⋆ᵇ n ≡ x ⋆⋆ fromBits n → (x ⋆ x) ⋆⋆ᵇ n ≡ x ⋆⋆ (2 * fromBits n)
+proof-lemma x n prf = begin
+  (x ⋆ x) ⋆⋆ᵇ n                         ≡⟨  ⋆⋆ᵇ-homoˡ x n ⟩
+  (x ⋆⋆ᵇ n)         ⋆ (x ⋆⋆ᵇ n)         ≡⟨  cong₂ _⋆_ prf prf ⟩
+  (x ⋆⋆ fromBits n) ⋆ (x ⋆⋆ fromBits n) ≡˘⟨ ⋆⋆-homoʳ x (fromBits n) (fromBits n) ⟩
+  x ⋆⋆ (fromBits n + fromBits n)        ≡˘⟨ cong (λ ◌ → x ⋆⋆ (fromBits n + ◌)) (+-identityʳ (fromBits n)) ⟩
+  x ⋆⋆ (2 * fromBits n)                 ∎
+
+proof : ∀ n k → n ⋆⋆ᵇ k ≡ n ⋆⋆ (fromBits k)
+proof x []          = refl
+proof x (false ∷ n) = proof-lemma x n (proof x n)
+proof x (true  ∷ n) = begin
+  expBySquare (ι ⋆ x) (x ⋆ x) n ≡⟨  cong (λ ◌ → expBySquare ◌ (x ⋆ x) n) (⋆-identityˡ x) ⟩
+  expBySquare x       (x ⋆ x) n ≡˘⟨ cong (λ ◌ → expBySquare ◌ (x ⋆ x) n) (⋆-identityʳ x) ⟩
+  expBySquare (x ⋆ ι) (x ⋆ x) n ≡⟨  expBySquare-homoˡ x ι (x ⋆ x) n ⟩
+  x ⋆ ((x ⋆ x) ⋆⋆ᵇ n)           ≡⟨  cong (x ⋆_) (proof-lemma x n (proof x n)) ⟩
+  x ⋆ (x ⋆⋆ (2 * fromBits n))   ∎
diff --git a/src/Problem15.agda b/src/Problem15.agda
new file mode 100644
index 0000000..6e0e89c
--- /dev/null
+++ b/src/Problem15.agda
@@ -0,0 +1,154 @@
+module Problem15 where
+
+open import Data.Vec as Vec
+open import Data.Fin
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Product hiding (map)
+open import Relation.Binary.PropositionalEquality
+open import Data.Vec.Properties
+open import Relation.Nullary
+open import Function
+
+open ≡-Reasoning
+
+variable n : ℕ
+variable A B : Set
+
+-- Useful properties not in stdlib 1.7.3
+
+map-tabulate : (g : A → B) (f : Fin n → A) → map g (tabulate f) ≡ tabulate (g ∘′ f)
+map-tabulate g f = begin
+  map g (tabulate f)       ≡⟨  cong (map g) (tabulate-allFin f) ⟩
+  map g (map f (allFin _)) ≡˘⟨ map-∘ g f (allFin _) ⟩
+  map (g ∘′ f) (allFin _)  ≡˘⟨ tabulate-allFin (g ∘′ f) ⟩
+  tabulate (g ∘′ f)        ∎
+
+Sur : ∀(v : Vec (Fin n) n) → Set
+Sur {n} v = ∀(x : Fin n) → ∃[ i ] lookup v i ≡ x
+
+Inj : ∀(v : Vec A n ) → Set
+Inj {_}{n} v = (a b : Fin n) → lookup v a ≡ lookup v b → a ≡ b
+
+record Perm (n : ℕ) : Set where
+    constructor P
+    field indices : Vec (Fin n) n
+    field surjective : Sur indices
+    field injective  : Inj indices
+
+    _⟨$⟩_ : Fin n → Fin n
+    _⟨$⟩_ = lookup indices
+
+open Perm
+
+-- Agda's proof irrelevance is too janky to work here
+-- And we'd need functional extensionality + UIP to prove this directly
+postulate cong-Perm : ∀ (p q : Perm n) → Perm.indices p ≡ Perm.indices q →  p ≡ q
+
+permute : Perm n → Vec A n → Vec A n
+permute (P p _ _) v = map (lookup v) p
+
+_⊡_ : Perm n → Perm n → Perm n
+(p ⊡ r) .indices    = tabulate ((p ⟨$⟩_) ∘ (r ⟨$⟩_))
+(p ⊡ r) .surjective x .proj₁ = r .surjective (p .surjective x .proj₁) .proj₁
+(p ⊡ r) .surjective x .proj₂ =
+  let (i , prf₁) = p .surjective x in
+  let (j , prf₂) = r .surjective i in
+  begin
+    lookup (tabulate ((p ⟨$⟩_) ∘ (r ⟨$⟩_))) j ≡⟨ lookup∘tabulate _ j ⟩
+    p ⟨$⟩ (r ⟨$⟩ j)                           ≡⟨ cong (p ⟨$⟩_) prf₂ ⟩
+    p ⟨$⟩ i                                   ≡⟨ prf₁ ⟩
+    x                                         ∎
+(p ⊡ r) .injective x y prf  =
+  r .injective x y $′
+  p .injective (r ⟨$⟩ x) (r ⟨$⟩ y) $′
+  begin
+    p ⟨$⟩ (r ⟨$⟩ x)                           ≡˘⟨ lookup∘tabulate _ x ⟩
+    lookup (tabulate ((p ⟨$⟩_) ∘ (r ⟨$⟩_))) x ≡⟨  prf ⟩
+    lookup (tabulate ((p ⟨$⟩_) ∘ (r ⟨$⟩_))) y ≡⟨  lookup∘tabulate _ y ⟩
+    p ⟨$⟩ (r ⟨$⟩ y)                           ∎
+
+infixl 20 _⊡_
+
+composition : (v : Vec A n)(p q : Perm n) → permute (p ⊡ q) v ≡ permute q (permute p v)
+composition v p q = begin
+  map (lookup v) ((p ⊡ q) .indices)                           ≡⟨⟩
+  map (lookup v) (tabulate ((p ⟨$⟩_) ∘′ (q ⟨$⟩_)))            ≡⟨  map-tabulate (lookup v) ((p ⟨$⟩_) ∘′ (q ⟨$⟩_)) ⟩
+  tabulate (lookup v ∘′ (p ⟨$⟩_) ∘′ (q ⟨$⟩_))                 ≡⟨⟩
+  tabulate (lookup v ∘′ (p ⟨$⟩_) ∘′ lookup (q .indices))      ≡˘⟨ tabulate-cong (λ i → lookup-map i (lookup v ∘′ (p ⟨$⟩_)) (q .indices)) ⟩
+  tabulate (lookup (map (lookup v ∘′ (p ⟨$⟩_)) (q .indices))) ≡⟨  tabulate∘lookup (map (lookup v ∘′ (p ⟨$⟩_)) (q .indices)) ⟩
+  map (lookup v ∘′ (p ⟨$⟩_)) (q .indices)                     ≡⟨⟩
+  map (lookup v ∘′ lookup (p .indices)) (q .indices)          ≡˘⟨  map-cong (λ i → lookup-map i (lookup v) (p .indices)) (q .indices) ⟩
+  map (lookup (map (lookup v) (p .indices))) (q .indices)     ∎
+
+assoc : ∀ (p q r : Perm n) → p ⊡ (q ⊡ r) ≡ p ⊡ q ⊡ r
+assoc p q r =
+  cong-Perm (p ⊡ (q ⊡ r)) (p ⊡ q ⊡ r) $′
+  begin
+    tabulate ((p ⟨$⟩_) ∘′ ((q ⊡ r) ⟨$⟩_))       ≡⟨  tabulate-cong (λ i → cong (p ⟨$⟩_) (lookup∘tabulate ((q ⟨$⟩_) ∘′ (r ⟨$⟩_)) i)) ⟩
+    tabulate ((p ⟨$⟩_) ∘′ (q ⟨$⟩_) ∘′ (r ⟨$⟩_)) ≡˘⟨ tabulate-cong (λ i → lookup∘tabulate ((p ⟨$⟩_) ∘′ (q ⟨$⟩_)) (r ⟨$⟩ i)) ⟩
+    tabulate (((p ⊡ q) ⟨$⟩_) ∘′ (r ⟨$⟩_))       ∎
+
+ι : Perm n
+ι {n} .indices = allFin n
+ι {n} .surjective x = x , lookup-allFin x
+ι {n} .injective x y prf = begin
+  x                   ≡˘⟨ lookup-allFin x ⟩
+  lookup (allFin n) x ≡⟨  prf ⟩
+  lookup (allFin n) y ≡⟨  lookup-allFin y ⟩
+  y                   ∎
+
+
+identityˡ : ∀(p : Perm n) → ι ⊡ p ≡ p
+identityˡ p =
+  cong-Perm (ι ⊡ p) p $′
+  begin
+    tabulate (lookup (allFin _) ∘′ (p ⟨$⟩_)) ≡⟨ tabulate-cong (λ i → lookup-allFin (p ⟨$⟩ i)) ⟩
+    tabulate (p ⟨$⟩_)                        ≡⟨ tabulate∘lookup (p .indices) ⟩
+    p .indices                               ∎
+
+
+identityʳ : ∀(p : Perm n) → p ⊡ ι ≡ p
+identityʳ {n} p =
+  cong-Perm (p ⊡ ι) p $′
+  begin
+    tabulate ((p ⟨$⟩_) ∘′ lookup (allFin n)) ≡⟨ tabulate-cong (λ i → cong (p ⟨$⟩_) (lookup-allFin i)) ⟩
+    tabulate (p ⟨$⟩_)                        ≡⟨ tabulate∘lookup (p .indices) ⟩
+    p .indices                               ∎
+
+
+_⁻¹ : Perm n → Perm n
+(p ⁻¹) .indices = tabulate (proj₁ ∘ p .surjective)
+(p ⁻¹) .surjective x .proj₁ = p ⟨$⟩ x
+(p ⁻¹) .surjective x .proj₂ =
+  p .injective (lookup (tabulate (proj₁ ∘ p .surjective)) (p ⟨$⟩ x)) x $′
+  begin
+    p ⟨$⟩ lookup (tabulate (proj₁ ∘ p .surjective)) (p ⟨$⟩ x) ≡⟨ cong (p ⟨$⟩_) (lookup∘tabulate (proj₁ ∘ p .surjective) (p ⟨$⟩ x)) ⟩
+    p ⟨$⟩ p .surjective (p ⟨$⟩ x) .proj₁                      ≡⟨ p .surjective (p ⟨$⟩ x) .proj₂ ⟩
+    p ⟨$⟩ x                                                   ∎
+(p ⁻¹) .injective x y prf =
+  begin
+    x                                                 ≡˘⟨ p .surjective x .proj₂ ⟩
+    p ⟨$⟩ p .surjective x .proj₁                      ≡˘⟨ cong (p ⟨$⟩_) (lookup∘tabulate (proj₁ ∘ p .surjective) x) ⟩
+    p ⟨$⟩ lookup (tabulate (proj₁ ∘ p .surjective)) x ≡⟨  cong (p ⟨$⟩_) prf ⟩
+    p ⟨$⟩ lookup (tabulate (proj₁ ∘ p .surjective)) y ≡⟨  cong (p ⟨$⟩_) (lookup∘tabulate (proj₁ ∘ p .surjective) y) ⟩
+    p ⟨$⟩ p .surjective y .proj₁                      ≡⟨  p .surjective y .proj₂ ⟩
+    y                                                 ∎
+
+infixl 30 _⁻¹
+
+
+inverseˡ : ∀(p : Perm n) → p ⁻¹ ⊡ p ≡ ι
+inverseˡ p =
+  cong-Perm (p ⁻¹ ⊡ p) ι $′
+  begin
+    tabulate ((p ⁻¹ ⟨$⟩_) ∘′ (p ⟨$⟩_))          ≡⟨ tabulate-cong (λ i → lookup∘tabulate (proj₁ ∘ p .surjective) (p ⟨$⟩ i)) ⟩
+    tabulate (proj₁ ∘ p .surjective ∘ (p ⟨$⟩_)) ≡⟨ tabulate-cong (λ i → p .injective _ i (p .surjective (p ⟨$⟩ i) .proj₂)) ⟩
+    tabulate id                                 ∎
+
+inverseʳ : ∀(p : Perm n) → p ⊡ p ⁻¹ ≡ ι
+inverseʳ p =
+  cong-Perm (p ⊡ p ⁻¹) ι $′
+  begin
+    tabulate ((p ⟨$⟩_) ∘′ (p ⁻¹ ⟨$⟩_))          ≡⟨ tabulate-cong (λ i → cong (p ⟨$⟩_) (lookup∘tabulate (proj₁ ∘ p .surjective) i)) ⟩
+    tabulate ((p ⟨$⟩_) ∘ proj₁ ∘ p .surjective) ≡⟨ tabulate-cong (λ i → p .surjective i .proj₂) ⟩
+    tabulate id                                 ∎
diff --git a/src/Problem16.agda b/src/Problem16.agda
new file mode 100644
index 0000000..d327602
--- /dev/null
+++ b/src/Problem16.agda
@@ -0,0 +1,46 @@
+{-# OPTIONS --safe #-}
+
+module Problem16 where
+
+open import Data.Fin
+open import Data.Nat using (ℕ; zero; suc)
+open import Data.Nat.Properties using (0≢1+n)
+open import Data.Fin.Properties
+open import Data.Product hiding (map)
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+open import Function
+
+variable n : ℕ
+
+open ≡-Reasoning
+
+Inj : (Fin n → Fin n) → Set
+Inj f = ∀ i j → f i ≡ f j → i ≡ j
+
+Sur : (Fin n → Fin n) → Set
+Sur f = ∀ x → ∃[ y ] f y ≡ x
+
+goal : ∀ n (f : Fin n → Fin n) → Inj f → Sur f
+goal (suc n) f inj x with f zero ≟ x
+... | yes prf = zero , prf
+... | no f0≢x =
+  let (z , prf) = goal n f′ f′-inj (punchOut f0≢x) in
+  suc z ,
+  (begin
+    f (suc z)                                 ≡˘⟨ punchIn-punchOut (f0≢f[1+i] z) ⟩
+    punchIn (f zero) (punchOut (f0≢f[1+i] z)) ≡⟨ cong (punchIn (f zero)) prf ⟩
+    punchIn (f zero) (punchOut (f0≢x))        ≡⟨ punchIn-punchOut f0≢x ⟩
+    x                                         ∎)
+  where
+  f0≢f[1+i] : ∀ i → f zero ≢ f (suc i)
+  f0≢f[1+i] i prf = 0≢1+n (cong toℕ (inj zero (suc i) prf))
+
+  f′ : Fin n → Fin n
+  f′ = punchOut ∘ f0≢f[1+i]
+
+  f′-inj : Inj f′
+  f′-inj i j prf =
+    suc-injective $′
+    inj (suc i) (suc j) $′
+    punchOut-injective (f0≢f[1+i] i) (f0≢f[1+i] j) prf
diff --git a/src/Problem17.agda b/src/Problem17.agda
new file mode 100644
index 0000000..d02502e
--- /dev/null
+++ b/src/Problem17.agda
@@ -0,0 +1,116 @@
+{-# OPTIONS --safe #-}
+
+module Problem17 (Act : Set) where
+
+open import Data.Empty
+open import Data.List
+open import Data.List.Membership.Propositional
+open import Data.List.Membership.Propositional.Properties
+open import Data.List.Relation.Unary.Any using (here; there)
+open import Data.Product hiding (map)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.Unit
+open import Function.Base using (id)
+open import Relation.Binary.PropositionalEquality hiding ([_])
+
+data Process : Set where
+  ⟨_⟩   : Act → Process
+  skip  : Process
+  abort : Process
+  -- not the normal semicolon, use \; and choose the correct option..
+  _;_   : Process → Process → Process
+  _+_   : Process → Process → Process
+  _∥_   : Process → Process → Process
+
+infixr 60 _;_
+infixr 70 _+_
+infixr 80 _∥_
+variable P P′ Q Q′ : Process
+variable a b c x : Act
+variable xs : List Act
+
+NoPar : Process → Set
+NoPar (P ; Q) = NoPar P × NoPar Q
+NoPar (P + Q) = NoPar P × NoPar Q
+NoPar (P ∥ Q) = ⊥
+NoPar ⟨ _ ⟩   = ⊤
+NoPar skip    = ⊤
+NoPar abort   = ⊤
+
+interleave : List Act → List Act → List (List Act)
+interleave [] ys = [ ys ]
+interleave xs [] = [ xs ]
+interleave (x ∷ xs) (y ∷ ys) = map (x ∷_) (interleave xs (y ∷ ys)) ++ map (y ∷_) (interleave (x ∷ xs) ys)
+
+⟦_⟧ : Process → List (List Act)
+⟦ ⟨ a ⟩ ⟧ = [ [ a ] ]
+⟦ skip  ⟧ = [ [] ]
+⟦ abort ⟧ = []
+⟦ P + Q ⟧ = ⟦ P ⟧ ++ ⟦ Q ⟧
+⟦ P ; Q ⟧ = concatMap (λ p → map (p ++_) ⟦ Q ⟧) ⟦ P ⟧
+⟦ P ∥ Q ⟧ = concatMap (λ p → concatMap (interleave p) ⟦ Q ⟧) ⟦ P ⟧
+
+_≈_ : Process → Process → Set
+P ≈ Q = ∀ xs → (xs ∈ ⟦ P ⟧ → xs ∈ ⟦ Q ⟧) × (xs ∈ ⟦ Q ⟧ → xs ∈ ⟦ P ⟧)
+
+-- Helpers for dealing with sequential traces
+
+;-trace : ∀ (P Q : Process) {xs ys} → xs ∈ ⟦ P ⟧ → ys ∈ ⟦ Q ⟧ → xs ++ ys ∈ ⟦ P ; Q ⟧
+;-trace P Q {xs} xs∈⟦P⟧ ys∈⟦Q⟧ =
+  ∈-concat⁺′ (∈-map⁺ (xs ++_) ys∈⟦Q⟧) (∈-map⁺ (λ p → map (p ++_) ⟦ Q ⟧) xs∈⟦P⟧)
+
+;-trace⁻¹ :
+  ∀ (P Q : Process) {xs} →
+  xs ∈ ⟦ P ; Q ⟧ → ∃₂ λ ys zs → xs ≡ ys ++ zs × ys ∈ ⟦ P ⟧ × zs ∈ ⟦ Q ⟧
+;-trace⁻¹ P Q {xs} xs∈⟦P;Q⟧ with ∈-concat⁻′ (map (λ p → map (p ++_) ⟦ Q ⟧) ⟦ P ⟧) xs∈⟦P;Q⟧
+... | xss , xs∈xss , xss∈⟦P⟧++⟦Q⟧ with ∈-map⁻ (λ p → map (p ++_) ⟦ Q ⟧) xss∈⟦P⟧++⟦Q⟧
+... | ys , ys∈⟦P⟧ , refl with ∈-map⁻ (ys ++_) xs∈xss
+... | zs , zs∈⟦Q⟧ , refl = ys , zs , refl , ys∈⟦P⟧ , zs∈⟦Q⟧
+
+-- Idea
+-- Each trace has a canonical process---the list of actions. We can map a list
+-- of possible traces to a canonical process by taking the sum of all individual
+-- traces.
+--
+-- We show the canonical process for list of traces is correct (contains all
+-- traces) and unique (contains only the desired traces).
+
+canonical₁ : List Act → Process
+canonical₁ []       = skip
+canonical₁ (a ∷ as) = ⟨ a ⟩ ; canonical₁ as
+
+canonical : List (List Act) → Process
+canonical []         = abort
+canonical (as ∷ ass) = canonical₁ as + canonical ass
+
+canonical₁-correct : ∀ as → as ∈ ⟦ canonical₁ as ⟧
+canonical₁-correct []       = here refl
+canonical₁-correct (a ∷ as) = ;-trace ⟨ a ⟩ (canonical₁ as) (here refl) (canonical₁-correct as)
+
+canonical₁-unique : ∀ as {xs} → xs ∈ ⟦ canonical₁ as ⟧ → xs ≡ as
+canonical₁-unique []       (here prf) = prf
+canonical₁-unique (a ∷ as) prf with ;-trace⁻¹ ⟨ a ⟩ (canonical₁ as) prf
+... | .([ a ]) , xs , refl , here refl , prf = cong (a ∷_) (canonical₁-unique as prf)
+
+canonical₁-NoPar : ∀ as → NoPar (canonical₁ as)
+canonical₁-NoPar []       = _
+canonical₁-NoPar (a ∷ as) = _ , canonical₁-NoPar as
+
+canonical-correct : ∀ ass {as} → as ∈ ass → as ∈ ⟦ canonical ass ⟧
+canonical-correct (as ∷ ass) (here refl) = ∈-++⁺ˡ (canonical₁-correct as)
+canonical-correct (as ∷ ass) (there prf) = ∈-++⁺ʳ ⟦ canonical₁ as ⟧ (canonical-correct ass prf)
+
+canonical-unique : ∀ ass {as} → as ∈ ⟦ canonical ass ⟧ → as ∈ ass
+canonical-unique (as ∷ ass) prf with ∈-++⁻ ⟦ canonical₁ as ⟧ prf
+... | inj₁ prf with refl ← canonical₁-unique as prf = here refl
+... | inj₂ prf = there (canonical-unique ass prf)
+
+canonical-NoPar : ∀ ass → NoPar (canonical ass)
+canonical-NoPar []         = _
+canonical-NoPar (as ∷ ass) = canonical₁-NoPar as , canonical-NoPar ass
+
+goal : ∀ (P : Process) → ∃[ P′ ] (P′ ≈ P) × NoPar P′
+goal P =
+    canonical ⟦ P ⟧
+  , (λ as → canonical-unique ⟦ P ⟧ , canonical-correct ⟦ P ⟧)
+  , canonical-NoPar ⟦ P ⟧
diff --git a/src/Problem18.agda b/src/Problem18.agda
new file mode 100644
index 0000000..e71dcb9
--- /dev/null
+++ b/src/Problem18.agda
@@ -0,0 +1,113 @@
+{-# OPTIONS --safe #-}
+
+module Problem18 (Symbol : Set) where
+
+open import Data.Nat
+open import Data.Vec
+open import Relation.Binary.PropositionalEquality
+open import Data.Product
+
+open ≡-Reasoning
+
+variable n m a b c d : ℕ
+
+data Patch : ℕ → ℕ → Set where
+  end : Patch 0 0
+  skp : Patch n m → Patch (suc n) (suc m)
+  del : Patch n m → Patch (suc n) m
+  ins : Symbol → Patch n m → Patch n (suc m)
+
+apply : Patch n m → Vec Symbol n → Vec Symbol m
+apply end  []  = []
+apply (ins x p) xs = x ∷ apply p xs
+apply (skp p) (x ∷ xs) = x ∷ apply p xs
+apply (del p) (x ∷ xs) = apply p xs
+
+infixl 50 _·_
+_·_ : Patch a b → Patch b c → Patch a c
+end      · p₂        = p₂
+skp p₁   · skp p₂    = skp (p₁ · p₂)
+skp p₁   · del p₂    = del (p₁ · p₂)
+skp p₁   · ins x p₂  = ins x (skp p₁ · p₂)
+ins x p₁ · ins x₂ p₂ = ins x₂ (ins x p₁ · p₂)
+del p₁   · ins x₂ p₂ = ins x₂ (del p₁ · p₂)
+del p₁   · p₂        = del (p₁ · p₂)
+ins x p₁ · skp p₂    = ins x (p₁ · p₂)
+ins x p₁ · del p₂    = p₁ · p₂
+
+_≈_ : (x y : Patch a b) → Set
+x ≈ y = ∀ d → apply x d ≡ apply y d
+
+compose-correct : ∀ (p₁ : Patch a b) (p₂ : Patch b c) (d : Vec Symbol a)
+                → apply (p₁ · p₂) d ≡ apply p₂ (apply p₁ d)
+compose-correct end        p₂         []      = refl
+compose-correct (skp p₁)   (skp p₂)   (x ∷ d) = cong (x ∷_) (compose-correct p₁ p₂ d)
+compose-correct (skp p₁)   (del p₂)   (x ∷ d) = compose-correct p₁ p₂ d
+compose-correct (skp p₁)   (ins y p₂) (x ∷ d) = cong (y ∷_) (compose-correct (skp p₁) p₂ (x ∷ d))
+compose-correct (del p₁)   end        (x ∷ d) = compose-correct p₁ end d
+compose-correct (del p₁)   (skp p₂)   (x ∷ d) = compose-correct p₁ (skp p₂) d
+compose-correct (del p₁)   (del p₂)   (x ∷ d) = compose-correct p₁ (del p₂) d
+compose-correct (del p₁)   (ins y p₂) (x ∷ d) = cong (y ∷_) (compose-correct (del p₁) p₂ (x ∷ d))
+compose-correct (ins y p₁) (skp p₂)   d       = cong (y ∷_) (compose-correct p₁ p₂ d)
+compose-correct (ins y p₁) (del p₂)   d       = compose-correct p₁ p₂ d
+compose-correct (ins y p₁) (ins z p₂) d       = cong (z ∷_) (compose-correct (ins y p₁) p₂ d)
+
+compose-assoc : ∀ (p₁ : Patch a b) (p₂ : Patch b c) (p₃ : Patch c d)
+              → (p₁ · p₂) · p₃ ≈ p₁ · (p₂ · p₃)
+compose-assoc p₁ p₂ p₃ d = begin
+  apply (p₁ · p₂ · p₃) d           ≡⟨  compose-correct (p₁ · p₂) p₃ d ⟩
+  apply p₃ (apply (p₁ · p₂) d)     ≡⟨  cong (apply p₃) (compose-correct p₁ p₂ d) ⟩
+  apply p₃ (apply p₂ (apply p₁ d)) ≡˘⟨ compose-correct p₂ p₃ (apply p₁ d) ⟩
+  apply (p₂ · p₃) (apply p₁ d)     ≡˘⟨ compose-correct p₁ (p₂ · p₃) d ⟩
+  apply (p₁ · (p₂ · p₃)) d         ∎
+
+
+record Merge (p₁ : Patch a b)(p₂ : Patch a c) : Set where
+    constructor M
+    field size : ℕ
+    field p₁′ : Patch b size
+    field p₂′ : Patch c size
+
+
+merge : ∀(p₁ : Patch a b)(p₂ : Patch a c) → Merge p₁ p₂
+merge end end = M 0 end end
+merge p₁ (ins x p₂)     = let m = merge p₁ p₂ in M (suc (Merge.size m)) (ins x (Merge.p₁′ m)) (skp (Merge.p₂′ m))
+merge (ins x p₁) p₂     = let m = merge p₁ p₂ in M (suc (Merge.size m)) (skp (Merge.p₁′ m))   (ins x (Merge.p₂′ m))
+merge (del p₁) (skp p₂) = let m = merge p₁ p₂ in M (Merge.size m)       (Merge.p₁′ m)         (del (Merge.p₂′ m))
+merge (skp p₁) (del p₂) = let m = merge p₁ p₂ in M (Merge.size m)       (del (Merge.p₁′ m))   (Merge.p₂′ m)
+merge (del p₁) (del p₂) = let m = merge p₁ p₂ in M (Merge.size m)       (Merge.p₁′ m)         (Merge.p₂′ m)
+merge (skp p₁) (skp p₂) = let m = merge p₁ p₂ in M (suc (Merge.size m)) (skp (Merge.p₁′ m))   (skp (Merge.p₂′ m))
+
+merge-pushout :
+  (p₁ : Patch a b) (p₂ : Patch a c) →
+  p₁ · Merge.p₁′ (merge p₁ p₂) ≈ p₂ · Merge.p₂′ (merge p₁ p₂)
+merge-pushout end        end        d       = refl
+merge-pushout end        (ins z p₂) d       = cong (z ∷_) (merge-pushout end p₂ d)
+merge-pushout (skp p₁)   (skp p₂)   (x ∷ d) = cong (x ∷_) (merge-pushout p₁ p₂ d)
+merge-pushout (skp p₁)   (del p₂)   (x ∷ d) = begin
+  apply (p₁ · Merge.p₁′ (merge p₁ p₂)) d                   ≡⟨  merge-pushout p₁ p₂ d ⟩
+  apply (p₂ · Merge.p₂′ (merge p₁ p₂)) d                   ≡⟨  compose-correct p₂ (Merge.p₂′ (merge p₁ p₂)) d ⟩
+  apply (Merge.p₂′ (merge p₁ p₂)) (apply p₂ d)             ≡⟨⟩
+  apply (Merge.p₂′ (merge p₁ p₂)) (apply (del p₂) (x ∷ d)) ≡˘⟨ compose-correct (del p₂) (Merge.p₂′ (merge p₁ p₂)) (x ∷ d) ⟩
+  apply (del p₂ · Merge.p₂′ (merge p₁ p₂)) (x ∷ d)         ∎
+merge-pushout (skp p₁)   (ins z p₂) d       = cong (z ∷_) (merge-pushout (skp p₁) p₂ d )
+merge-pushout (del p₁)   (skp p₂)   (x ∷ d) = begin
+  apply (del p₁ · Merge.p₁′ (merge p₁ p₂)) (x ∷ d)         ≡⟨  compose-correct (del p₁) (Merge.p₁′ (merge p₁ p₂)) (x ∷ d) ⟩
+  apply (Merge.p₁′ (merge p₁ p₂)) (apply (del p₁) (x ∷ d)) ≡⟨⟩
+  apply (Merge.p₁′ (merge p₁ p₂)) (apply p₁ d)             ≡˘⟨ compose-correct p₁ (Merge.p₁′ (merge p₁ p₂)) d ⟩
+  apply (p₁ · Merge.p₁′ (merge p₁ p₂)) d                   ≡⟨  merge-pushout p₁ p₂ d ⟩
+  apply (p₂ · Merge.p₂′ (merge p₁ p₂)) d                   ∎
+merge-pushout (del p₁)   (del p₂)   (x ∷ d) = begin
+  apply (del p₁ · Merge.p₁′ (merge p₁ p₂)) (x ∷ d)         ≡⟨  compose-correct (del p₁) (Merge.p₁′ (merge p₁ p₂)) (x ∷ d) ⟩
+  apply (Merge.p₁′ (merge p₁ p₂)) (apply (del p₁) (x ∷ d)) ≡⟨⟩
+  apply (Merge.p₁′ (merge p₁ p₂)) (apply p₁ d)             ≡˘⟨ compose-correct p₁ (Merge.p₁′ (merge p₁ p₂)) d ⟩
+  apply (p₁ · Merge.p₁′ (merge p₁ p₂)) d                   ≡⟨  merge-pushout p₁ p₂ d ⟩
+  apply (p₂ · Merge.p₂′ (merge p₁ p₂)) d                   ≡⟨  compose-correct p₂ (Merge.p₂′ (merge p₁ p₂)) d ⟩
+  apply (Merge.p₂′ (merge p₁ p₂)) (apply p₂ d)             ≡⟨⟩
+  apply (Merge.p₂′ (merge p₁ p₂)) (apply (del p₂) (x ∷ d)) ≡˘⟨ compose-correct (del p₂) (Merge.p₂′ (merge p₁ p₂)) (x ∷ d) ⟩
+  apply (del p₂ · Merge.p₂′ (merge p₁ p₂)) (x ∷ d)         ∎
+merge-pushout (del p₁)   (ins z p₂) d       = cong (z ∷_) (merge-pushout (del p₁) p₂ d)
+merge-pushout (ins y p₁) end        d       = cong (y ∷_) (merge-pushout p₁ end d)
+merge-pushout (ins y p₁) (skp p₂)   d       = cong (y ∷_) (merge-pushout p₁ (skp p₂) d)
+merge-pushout (ins y p₁) (del p₂)   d       = cong (y ∷_) (merge-pushout p₁ (del p₂) d)
+merge-pushout (ins y p₁) (ins z p₂) d       = cong (z ∷_) (merge-pushout (ins y p₁) p₂ d)
diff --git a/src/Problem19.agda b/src/Problem19.agda
new file mode 100644
index 0000000..130d46e
--- /dev/null
+++ b/src/Problem19.agda
@@ -0,0 +1,159 @@
+{-# OPTIONS --safe #-}
+
+module Problem19 where
+
+open import Data.List hiding ([_])
+open import Data.Product
+open import Data.Empty
+open import Data.List.Properties
+open import Data.Sum
+open import Data.Unit hiding (_≟_)
+open import Data.Char
+open import Data.Maybe
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality hiding ([_])
+
+data Regex : Set where
+    ∅ : Regex
+    ε : Regex
+    [_] : Char → Regex
+    _∘_ : Regex → Regex → Regex
+    _∪_ : Regex → Regex → Regex
+    _⋆  : Regex → Regex
+
+variable c : Char
+variable R S : Regex
+variable s t : List Char
+
+data Matches : Regex → List Char → Set where
+   empty : Matches ε []
+   char  : Matches [ c ] (c ∷ [])
+   comp  : Matches R s → Matches S t → Matches (R ∘ S) (s ++ t)
+   un₁   : Matches R s → Matches (R ∪ S) s
+   un₂   : Matches S s → Matches (R ∪ S) s
+   starₑ : Matches (R ⋆) []
+   starₛ : Matches R s → Matches (R ⋆) t → Matches (R ⋆) (s ++ t)
+
+comp⁻¹ : Matches (R ∘ S) s → ∃₂ λ t₁ t₂ → t₁ ++ t₂ ≡ s × Matches R t₁ × Matches S t₂
+comp⁻¹ (comp prf prf₁) = _ , _ , refl , prf , prf₁
+
+star⁻¹′ : Matches (R ⋆) s → s ≡ [] ⊎ ∃[ c ] ∃[ t₁ ] ∃[ t₂ ] c ∷ t₁ ++ t₂ ≡ s × Matches R (c ∷ t₁) × Matches (R ⋆) t₂
+star⁻¹′ starₑ = inj₁ refl
+star⁻¹′ (starₛ {s = []} prf prf₁) = star⁻¹′ prf₁
+star⁻¹′ (starₛ {s = x ∷ s} prf prf₁) = inj₂ (x , s , _ , refl , prf , prf₁)
+
+Nullable : Regex → Set
+Nullable ∅ = ⊥
+Nullable ε = ⊤
+Nullable [ x ] = ⊥
+Nullable (r ∘ r₁) = Nullable r × Nullable r₁
+Nullable (r ∪ r₁) = Nullable r ⊎ Nullable r₁
+Nullable (r ⋆) = ⊤
+
+nullable? : (r : Regex) → Dec (Nullable r)
+nullable? ∅ = no (λ x → x)
+nullable? ε = yes tt
+nullable? [ x ] = no (λ x → x)
+nullable? (r ∘ r₁) with nullable? r | nullable? r₁
+... | no p  | _     = no λ (a , b) → p a
+... | _     | no p  = no λ (a , b) → p b
+... | yes p | yes q = yes (p , q)
+nullable? (r ∪ r₁)  with nullable? r | nullable? r₁
+... | yes p | _     = yes (inj₁ p)
+... | _     | yes p = yes (inj₂ p)
+... | no p  | no q  = no λ { (inj₁ a) → p a ; (inj₂ b) → q b }
+nullable? (r ⋆) = yes tt
+
+nullable-correct₁ : ∀ R → Nullable R → Matches R []
+nullable-correct₁ ε        _               = empty
+nullable-correct₁ (r ∘ r₁) (null₁ , null₂) = comp (nullable-correct₁ r null₁) (nullable-correct₁ r₁ null₂)
+nullable-correct₁ (r ∪ r₁) (inj₁ null)     = un₁ (nullable-correct₁ r null)
+nullable-correct₁ (r ∪ r₁) (inj₂ null)     = un₂ (nullable-correct₁ r₁ null)
+nullable-correct₁ (r ⋆)    _               = starₑ
+
+st≡[]⇒s≡[] : s ++ t ≡ [] → s ≡ []
+st≡[]⇒s≡[] {[]} {t} prf = refl
+
+st≡[]⇒t≡[] : s ++ t ≡ [] → t ≡ []
+st≡[]⇒t≡[] {[]} {t} prf = prf
+
+nullable-correct₂′ : ∀ {R} → Matches R s → s ≡ [] → Nullable R
+nullable-correct₂′ empty            s≡[]  = _
+nullable-correct₂′ (comp s∈r t∈r₁)  st≡[] = nullable-correct₂′ s∈r (st≡[]⇒s≡[] st≡[]) , nullable-correct₂′ t∈r₁ (st≡[]⇒t≡[] st≡[])
+nullable-correct₂′ (un₁ s∈r)        s≡[]  = inj₁ (nullable-correct₂′ s∈r s≡[])
+nullable-correct₂′ (un₂ s∈r)        s≡[]  = inj₂ (nullable-correct₂′ s∈r s≡[])
+nullable-correct₂′ starₑ            s≡[]  = _
+nullable-correct₂′ (starₛ s∈r s∈r₁) s≡[]  = _
+
+nullable-correct₂ : ∀ R → Matches R [] → Nullable R
+nullable-correct₂ r []∈r = nullable-correct₂′ []∈r refl
+
+step : Regex → Char → Regex
+step ∅ c = ∅
+step ε c = ∅
+step [ x ] c with c ≟ x
+... |  yes p = ε
+... |  no  p = ∅
+step (r ∘ r₁) c with nullable? r
+... | yes p = (step r c ∘ r₁) ∪ step r₁ c
+... | no  p = step r c ∘ r₁
+step (r ∪ r₁) c = step r c ∪ step r₁ c
+step (r ⋆) c = step r c ∘ (r ⋆)
+
+steps : Regex → List Char → Regex
+steps R (x ∷ xs) = steps (step R x) xs
+steps R [] = R
+
+step-correct₁ : ∀ R c s → Matches (step R c) s → Matches R (c ∷ s)
+step-correct₁ [ x ]    c s   prf   with c ≟ x
+step-correct₁ [ x ]    c s empty | yes refl = char
+step-correct₁ [ x ]    c s ()    | no p
+
+step-correct₁ (R ∘ R₁) c s prf                   with nullable? R
+step-correct₁ (R ∘ R₁) c s (un₁ (comp prf prf₁)) | yes p = comp (step-correct₁ R c _ prf) prf₁
+step-correct₁ (R ∘ R₁) c s (un₂ prf)             | yes p = comp (nullable-correct₁ R p) (step-correct₁ R₁ c _ prf)
+step-correct₁ (R ∘ R₁) c s (comp prf prf₁)       | no p  = comp (step-correct₁ R c _ prf) prf₁
+
+step-correct₁ (R ∪ R₁) c s (un₁ prf) = un₁ (step-correct₁ R c s prf)
+step-correct₁ (R ∪ R₁) c s (un₂ prf) = un₂ (step-correct₁ R₁ c s prf)
+
+step-correct₁ (R ⋆)    c s (comp prf prf₁) = starₛ (step-correct₁ R c _ prf) prf₁
+
+step-correct₂ : ∀ R c s → Matches R (c ∷ s) → Matches (step R c) s
+step-correct₂ [ x ]    c s char with x ≟ x
+... | yes p = empty
+... | no  p = ⊥-elim (p refl)
+step-correct₂ (R ∘ R₁) c s prf with nullable? R | comp⁻¹ prf
+... | yes p | []     , t₂ , refl , prf , prf₁ = un₂ (step-correct₂ R₁ c s prf₁)
+... | yes p | x ∷ t₁ , t₂ , eq   , prf , prf₁ =
+  un₁ (subst₂ Matches (cong (λ - → step R - ∘ R₁) (∷-injectiveˡ eq)) (∷-injectiveʳ eq)
+    (comp (step-correct₂ R x t₁ prf) prf₁))
+... | no p  | []     , t₂ , eq   , prf , prf₁ = ⊥-elim (p (nullable-correct₂ R prf))
+... | no p  | x ∷ t₁ , t₂ , eq   , prf , prf₁ =
+  subst₂ Matches (cong (λ - → step R - ∘ R₁) (∷-injectiveˡ eq)) (∷-injectiveʳ eq)
+    (comp (step-correct₂ R x t₁ prf) prf₁)
+step-correct₂ (R ∪ R₁) c s (un₁ prf) = un₁ (step-correct₂ R c s prf)
+step-correct₂ (R ∪ R₁) c s (un₂ prf) = un₂ (step-correct₂ R₁ c s prf)
+step-correct₂ (R ⋆)    c s prf with star⁻¹′ prf
+... | inj₂ (x , t₁ , t₂ , eq , prf , prf₁) =
+  subst₂ Matches (cong (λ - → step R - ∘ (R ⋆)) (∷-injectiveˡ eq)) (∷-injectiveʳ eq)
+    (comp (step-correct₂ R x t₁ prf) prf₁)
+
+steps-correct₁ : ∀ R s → Matches (steps R s) [] → Matches R s
+steps-correct₁ R []      prf = prf
+steps-correct₁ R (x ∷ s) prf = step-correct₁ R x s (steps-correct₁ (step R x) s prf)
+
+steps-correct₂ : ∀ R s → Matches R s → Matches (steps R s) []
+steps-correct₂ R []      prf = prf
+steps-correct₂ R (x ∷ s) prf = steps-correct₂ (step R x) s (step-correct₂ R x s prf)
+
+check-lemma₁ : ∀ R s → Nullable (steps R s) → Matches R s
+check-lemma₁ R s null = steps-correct₁ R s (nullable-correct₁ (steps R s) null)
+
+check-lemma₂ : ∀ R s → Matches R s → Nullable (steps R s)
+check-lemma₂ R s prf = nullable-correct₂ (steps R s) (steps-correct₂ R s prf)
+
+check : (R : Regex) (s : List Char) → Dec (Matches R s)
+check R s with nullable? (steps R s)
+... | yes p = yes (check-lemma₁ R s p)
+... | no p = no λ m → p (check-lemma₂ R s m)
diff --git a/src/Problem2.agda b/src/Problem2.agda
new file mode 100644
index 0000000..aaf35bc
--- /dev/null
+++ b/src/Problem2.agda
@@ -0,0 +1,55 @@
+{-# OPTIONS --safe #-}
+
+module Problem2 (T : Set) where
+open import Data.List
+open import Data.Nat
+open import Data.Product
+
+Relation = T → T → Set
+
+Commutes : Relation → Relation → Set
+Commutes R1 R2 = ∀{x y z} → R1 x y →  R2 x z → ∃[ t ] (R2 y t × R1 z t)
+
+Diamond : Relation → Set
+Diamond R = Commutes R R
+
+data Star (R : Relation) : Relation where
+  rule  : ∀{x y} → R x y → Star R x y
+  refl  : ∀{x} → Star R x x
+  trans : ∀{x y z} → Star R x y → Star R y z → Star R x z
+
+-- We prove by induction on the transitive closure proof rs. The three cases
+-- are given diagrammatically:
+--
+-- rs = rule r′
+-- We have the following diagram by assumption.
+-- x - r′ → y
+-- |        |
+-- r        s
+-- ↓        ↓
+-- z - s′ → t
+--
+-- rs = refl
+-- The diagram commutes.
+-- x == x
+-- |    |
+-- r    r
+-- ↓    ↓
+-- z == z
+--
+-- rs = trans rs₁ rs₂
+-- The diagram commutes, with each square derived by induction.
+-- x - rs₁ → y₁ - rs₂ → y₂
+-- |         |          |
+-- r         s₁         s₂
+-- ↓         ↓          ↓
+-- z - ss₁ → t₁ - ss₂ → t₂
+strip : ∀{R} → Diamond R → Commutes (Star R) R
+strip commutes (rule r′) r =
+  let (t , s , s′) = commutes r′ r in
+  t , s , rule s′
+strip commutes refl r = -, r , refl
+strip commutes (trans rs₁ rs₂) r =
+  let (t₁ , s₁ , ss₁) = strip commutes rs₁ r in
+  let (t₂ , s₂ , ss₂) = strip commutes rs₂ s₁ in
+  t₂ , s₂ , trans ss₁ ss₂
diff --git a/src/Problem20.agda b/src/Problem20.agda
new file mode 100644
index 0000000..364534d
--- /dev/null
+++ b/src/Problem20.agda
@@ -0,0 +1,105 @@
+{-# OPTIONS --safe #-}
+
+module Problem20 where
+
+open import Data.Maybe as Maybe hiding (_>>=_; map)
+open import Function
+open import Relation.Binary.PropositionalEquality
+
+open ≡-Reasoning
+
+data Expr (V : Set) : Set where
+   λ′_ : Expr (Maybe V) → Expr V
+   _·_ : Expr V → Expr V → Expr V
+   var : V → Expr V
+
+variable V A B C D : Set
+
+map : (A → B) → Expr A → Expr B
+map f (λ′ e)  = λ′ map (Maybe.map f) e
+map f (e · a) = map f e · map f a
+map f (var x) = var (f x)
+
+_>>=_ : Expr A → (A → Expr B) → Expr B
+(λ′ e)   >>= f = λ′ (e >>= maybe (map just ∘ f) (var nothing))
+(e · e₁) >>= f = (e >>= f) · (e₁ >>= f)
+var x    >>= f = f x
+
+-- Lean users have the advantage of functional extensionality, but Agda users don't
+-- So I have provided these congruence lemmas so that Agda users are at no axiomatic disadvantage.
+
+map-cong : ∀{f g : A → B}(ma : Expr A) → (∀ x → f x ≡ g x) → map f ma ≡ map g ma
+map-cong (λ′ ma) eq = cong λ′_ (map-cong ma λ { nothing → refl ; (just x) → cong just (eq x) })
+map-cong (ma · ma₁) eq = cong₂ _·_ (map-cong ma eq) (map-cong ma₁ eq)
+map-cong (var x) eq = cong var (eq x)
+
+>>=-cong : ∀{f g : A → Expr B}(ma : Expr A) → (∀ x → f x ≡ g x) → ma >>= f ≡ ma >>= g
+>>=-cong (λ′ ma) eq = cong λ′_ (>>=-cong ma λ { nothing → refl ; (just x) → cong (map just) (eq x) })
+>>=-cong (ma · ma₁) eq = cong₂ _·_ (>>=-cong ma eq) (>>=-cong ma₁ eq)
+>>=-cong (var x) eq = eq x
+
+-- Functor Laws
+
+map-id : (ma : Expr A) → map id ma ≡ ma
+map-id (λ′ ma) = cong λ′_ (begin
+  map (Maybe.map id) ma ≡⟨ map-cong ma (λ { (just a) → refl ; nothing → refl }) ⟩
+  map id ma             ≡⟨ map-id ma ⟩
+  ma                    ∎)
+map-id (ma · ma₁) = cong₂ _·_ (map-id ma) (map-id ma₁)
+map-id (var x) = refl
+
+map-homo : (f : B → C) (g : A → B) (ma : Expr A) → map f (map g ma) ≡ map (f ∘ g) ma
+map-homo f g (λ′ ma) = cong λ′_ (begin
+  map (Maybe.map f) (map (Maybe.map g) ma) ≡⟨ map-homo (Maybe.map f) (Maybe.map g) ma ⟩
+  map (Maybe.map f ∘ Maybe.map g) ma       ≡⟨ map-cong ma (λ { (just a) → refl ; nothing → refl }) ⟩
+  map (Maybe.map (f ∘ g)) ma               ∎)
+map-homo f g (ma · ma₁) = cong₂ _·_ (map-homo f g ma) (map-homo f g ma₁)
+map-homo f g (var x) = refl
+
+-- Bind-var is map
+
+>>=-var : (f : A → B) (ma : Expr A) → ma >>= (var ∘ f) ≡ map f ma
+>>=-var f (λ′ ma) = cong λ′_ (begin
+  ma >>= maybe (var ∘ just ∘ f) (var nothing) ≡⟨ >>=-cong ma (λ { (just a) → refl ; nothing → refl }) ⟩
+  ma >>= (var ∘ Maybe.map f)                  ≡⟨ >>=-var (Maybe.map f) ma ⟩
+  map (Maybe.map f) ma                       ∎)
+>>=-var f (ma · ma₁) = cong₂ _·_ (>>=-var f ma) (>>=-var f ma₁)
+>>=-var f (var x) = refl
+
+>>=-assoc : (g : B → C) (f : A → Expr B) (ma : Expr A) → map g (ma >>= f) ≡ ma >>= (map g ∘ f)
+>>=-assoc g f (λ′ ma) = cong λ′_ (begin
+  map (Maybe.map g) (ma >>= maybe (map just ∘ f) (var nothing))   ≡⟨  >>=-assoc (Maybe.map g) (maybe (map just ∘ f) (var nothing)) ma ⟩
+  ma >>= (map (Maybe.map g) ∘ maybe (map just ∘ f) (var nothing)) ≡⟨  >>=-cong ma (λ { (just a) → map-homo (Maybe.map g) just (f a) ; nothing → refl }) ⟩
+  ma >>= maybe (map (Maybe.map g ∘ just) ∘ f) (var nothing)       ≡˘⟨ >>=-cong ma (λ { (just a) → map-homo just g (f a) ; nothing → refl }) ⟩
+  ma >>= maybe (map just ∘ map g ∘ f) (var nothing)               ∎)
+>>=-assoc g f (ma · ma₁) = cong₂ _·_ (>>=-assoc g f ma) (>>=-assoc g f ma₁)
+>>=-assoc g f (var x) = refl
+
+>>=-lift : (f : A → B) (g : B → Expr C) (h : A → Expr C) → g ∘ f ≗ h → (ma : Expr A) → map f ma >>= g ≡ ma >>= h
+>>=-lift f g h gf≗h (λ′ ma) = cong λ′_ (>>=-lift _ _ _ (λ { (just a) → cong (map just) (gf≗h a) ; nothing → refl }) ma)
+>>=-lift f g h gf≗h (ma · ma₁) = cong₂ _·_ (>>=-lift f g h gf≗h ma) (>>=-lift f g h gf≗h ma₁)
+>>=-lift f g h gf≗h (var x) = gf≗h x
+
+assoc : ∀(g : A → Expr B)(h : B → Expr C)(a : Expr A)
+      → a >>= (λ a′ → g a′ >>= h) ≡ (a >>= g) >>= h
+assoc g h (λ′ ma) = cong λ′_ (begin
+  ma >>= maybe (λ a → map just (g a >>= h)) (var nothing)                                      ≡⟨ >>=-cong ma (λ { (just a) → lemma a ; nothing → refl }) ⟩
+  (ma >>= (λ a → maybe (map just ∘ g) (var nothing) a >>= maybe (map just ∘ h) (var nothing))) ≡⟨ assoc (maybe (map just ∘ g) (var nothing)) (maybe (map just ∘ h) (var nothing)) ma ⟩
+  (ma >>= maybe (map just ∘ g) (var nothing)) >>= maybe (map just ∘ h) (var nothing)           ∎)
+  where
+  lemma : (a : _) → map just (g a >>= h) ≡ map just (g a) >>= maybe (map just ∘ h) (var nothing)
+  lemma a = begin
+    map just (g a >>= h)                                  ≡⟨  >>=-assoc just h (g a) ⟩
+    g a >>= (map just ∘ h)                                ≡˘⟨ >>=-lift just (maybe (map just ∘ h) (var nothing)) (map just ∘ h) (λ _ → refl) (g a) ⟩
+    map just (g a) >>= maybe (map just ∘ h) (var nothing) ∎
+assoc g h (ma · ma₁) = cong₂ _·_ (assoc g h ma) (assoc g h ma₁)
+assoc g h (var x) = refl
+
+identₗ : ∀(f : A → Expr B)(x : A) → var x >>= f ≡ f x
+identₗ _ _ = refl
+
+identᵣ : ∀(e : Expr A) → e >>= var ≡ e
+identᵣ e = begin
+  e >>= var ≡⟨ >>=-var id e ⟩
+  map id e  ≡⟨ map-id e ⟩
+  e         ∎
diff --git a/src/Problem21.agda b/src/Problem21.agda
new file mode 100644
index 0000000..e5d27e2
--- /dev/null
+++ b/src/Problem21.agda
@@ -0,0 +1,80 @@
+{-# OPTIONS --safe #-}
+
+module Problem21 (Atom : Set) where
+
+open import Data.List
+open import Relation.Binary.PropositionalEquality hiding ([_])
+open import Data.Empty
+open import Data.Nat
+open import Data.Fin
+open import Data.Fin.Patterns
+open import Data.Product
+
+data L : Set where
+    ⟨_⟩ : Atom → L
+    ⟨_⟩ᶜ : Atom → L
+    _⊗_ : L → L → L
+    _⅋_ : L → L → L
+    ⊥' : L
+    𝟙  : L
+
+variable A B C : L
+variable Δ Γ : List L
+variable α β η : Atom
+
+_ᶜ : L → L
+⟨ A ⟩   ᶜ = ⟨ A ⟩ᶜ
+⟨ A ⟩ᶜ  ᶜ = ⟨ A ⟩
+(A ⊗ B) ᶜ = (A ᶜ) ⅋ (B ᶜ)
+(A ⅋ B) ᶜ = (A ᶜ) ⊗ (B ᶜ)
+𝟙       ᶜ = ⊥'
+⊥'      ᶜ = 𝟙
+
+_⊸_ : L → L → L
+A ⊸ B = (A ᶜ) ⅋ B
+
+infixl 2 ⊢_
+data ⊢_ : List L → Set where
+    one      : ⊢ [ 𝟙 ]
+    identity : ⊢ ⟨ α ⟩ ∷ ⟨ α ⟩ᶜ ∷ []
+    exch     :  (n : Fin (length Δ))
+             → ⊢ lookup Δ n ∷ (Δ ─ n)
+             → ⊢ Δ
+    times    : (n : ℕ)
+             → ⊢ A ∷ take n Δ
+             → ⊢ B ∷ drop n Δ
+             → ⊢ A ⊗ B ∷ Δ
+    par      : ⊢ A ∷ B ∷ Δ
+             → ⊢ A ⅋ B ∷ Δ
+    bottom   : ⊢ Δ
+             → ⊢ ⊥' ∷ Δ
+
+    cut      : ⊢ A ∷ Δ
+             → ⊢ A ᶜ ∷ Γ
+             → ⊢ Δ ++ Γ
+
+id : {A : L} → ⊢ A ∷ A ᶜ ∷ []
+id {⟨ x ⟩} = identity
+id {⟨ x ⟩ᶜ} = exch 1F identity
+id {A ⊗ B} = exch 1F (par (exch 2F (times 1 (id {A}) (id {B}))))
+id {A ⅋ B} = par (exch 2F (times 1 (exch 1F (id {A})) (exch 1F (id {B}))))
+id {⊥'} = bottom one
+id {𝟙} = exch 1F (bottom one)
+
+id′ : {A : L} → ⊢ A ᶜ ∷ A ∷ []
+id′ = exch 1F id
+
+_≈_ : L → L → Set
+A ≈ B = (⊢ [ A ] → ⊢ [ B ]) × (⊢ [ B ] → ⊢ [ A ])
+
+lem₁ : ((A ⊗ B) ⊸ C) ≈ (A ⊸ (B ⊸ C))
+lem₁ .proj₁ prf = cut prf (exch 1F (par (exch 1F (par (exch 2F (exch 3F (times 2 (times 1 id′ id′) id′)))))))
+lem₁ .proj₂ prf = cut prf (exch 1F (par (par (exch 3F (times 1 id′ (times 1 id′ id′))))))
+
+lem₂ : (A ⊸ (B ⅋ C)) ≈ ((A ⊸ B) ⅋ C)
+lem₂ .proj₁ prf = cut prf (exch 1F (par (par (exch 3F (times 1 id′ (times 1 id′ id′))))))
+lem₂ .proj₂ prf = cut prf (exch 1F (par (exch 1F (par (exch 2F (exch 3F (times 2 (times 1 id′ id′) id′)))))))
+
+lem₃ : (A ⊸ B) ≈ ((B ᶜ) ⊸ (A ᶜ))
+lem₃ .proj₁ prf = cut prf (exch 1F (par (exch 1F (exch 2F (times 1 id′ id)))))
+lem₃ .proj₂ prf = cut prf (exch 1F (par (exch 1F (exch 2F (times 1 (exch 1F (cut id′ id)) id′)))))
diff --git a/src/Problem22.agda b/src/Problem22.agda
new file mode 100644
index 0000000..a4befd8
--- /dev/null
+++ b/src/Problem22.agda
@@ -0,0 +1,87 @@
+{-# OPTIONS --safe #-}
+
+module Problem22
+    (Act : Set)
+    (State : Set)
+    (_─⟨_⟩→_ : State → Act → State → Set) where
+
+open import Data.Empty
+open import Data.Product
+open import Data.Unit
+open import Function.Base using (_∘′_)
+open import Level
+open import Relation.Binary.PropositionalEquality
+
+variable ℓ : Level
+variable α β γ : Act
+variable x x′ y y′ z : State
+
+record Bisimulation(R : State → State → Set ℓ) : Set ℓ where
+  constructor B
+  field
+    left  : R x y → x ─⟨ α ⟩→ x′ → ∃[ y′ ] (y ─⟨ α ⟩→ y′ × R x′ y′)
+    right : R x y → y ─⟨ α ⟩→ y′ → ∃[ x′ ] (x ─⟨ α ⟩→ x′ × R x′ y′)
+
+open Bisimulation
+
+_≈_ : State → State → Set₁
+x ≈ y = ∃[ R ] (Bisimulation R × R x y)
+
+reflexive : x ≈ x
+reflexive .proj₁ = _≡_
+reflexive .proj₂ .proj₁ .left  refl step = _ , step , refl
+reflexive .proj₂ .proj₁ .right refl step = _ , step , refl
+reflexive .proj₂ .proj₂ = refl
+
+symmetric : x ≈ y → y ≈ x
+symmetric x≈y .proj₁ x y = x≈y .proj₁ y x
+symmetric x≈y .proj₂ .proj₁ .left  = x≈y .proj₂ .proj₁ .right
+symmetric x≈y .proj₂ .proj₁ .right = x≈y .proj₂ .proj₁ .left
+symmetric x≈y .proj₂ .proj₂ = x≈y .proj₂ .proj₂
+
+transitive : x ≈ y → y ≈ z → x ≈ z
+transitive x≈y y≈z .proj₁ x z = ∃[ y ] x≈y .proj₁ x y × y≈z .proj₁ y z
+transitive x≈y y≈z .proj₂ .proj₁ .left  (_ , rel₁ , rel₂) stepˡ =
+  let _ , stepᵐ , rel₁′ = x≈y .proj₂ .proj₁ .left rel₁ stepˡ in
+  let _ , stepʳ , rel₂′ = y≈z .proj₂ .proj₁ .left rel₂ stepᵐ in
+  _ , stepʳ , _ , rel₁′ , rel₂′
+transitive x≈y y≈z .proj₂ .proj₁ .right (_ , rel₁ , rel₂) stepʳ =
+  let _ , stepᵐ , rel₂′ = y≈z .proj₂ .proj₁ .right rel₂ stepʳ in
+  let _ , stepˡ , rel₁′ = x≈y .proj₂ .proj₁ .right rel₁ stepᵐ in
+  _ , stepˡ , _ , rel₁′ , rel₂′
+transitive x≈y y≈z .proj₂ .proj₂ = _ , x≈y .proj₂ .proj₂ , y≈z .proj₂ .proj₂
+
+bisim-is-bisim : Bisimulation _≈_
+bisim-is-bisim .left (R , bisim , x≈y) stepˡ =
+  let (y′ , stepʳ , x′≈y′) = bisim .left x≈y stepˡ in
+  y′ , stepʳ , R , bisim , x′≈y′
+bisim-is-bisim .right (R , bisim , x≈y) stepʳ =
+  let (x′ , stepˡ , x′≈y′) = bisim .right x≈y stepʳ in
+  x′ , stepˡ , R , bisim , x′≈y′
+
+data HML : Set where
+    ⟪_⟫_ : Act → HML → HML
+    ⟦_⟧_ : Act → HML → HML
+    _∧_  : HML → HML → HML
+    ⊤′  : HML
+    ¬′_  : HML → HML
+
+variable ϕ ψ : HML
+infixl 10 _⊧_
+_⊧_ : State → HML → Set
+σ ⊧ ⊤′ = ⊤
+σ ⊧ ¬′ ϕ = σ ⊧ ϕ → ⊥
+σ ⊧ ϕ ∧ ψ = (σ ⊧ ϕ) × (σ ⊧ ψ)
+σ ⊧ ⟪ α ⟫ ϕ = ∃[ σ′ ] σ ─⟨ α ⟩→ σ′ × σ′ ⊧ ϕ
+σ ⊧ ⟦ α ⟧ ϕ = ∀ σ′ → σ ─⟨ α ⟩→ σ′ → σ′ ⊧ ϕ
+
+hml-bisim : ∀ ϕ → x ≈ y → x ⊧ ϕ → y ⊧ ϕ
+hml-bisim ⊤′        (R , bisim , x≈y) prf = prf
+hml-bisim (¬′ ϕ)    (R , bisim , x≈y) prf = prf ∘′ hml-bisim ϕ (symmetric (R , bisim , x≈y))
+hml-bisim (ϕ ∧ ψ)   (R , bisim , x≈y) (prf , prf₁) = hml-bisim ϕ (R , bisim , x≈y) prf , hml-bisim ψ (R , bisim , x≈y) prf₁
+hml-bisim (⟪ a ⟫ ϕ) (R , bisim , x≈y) (x′ , stepˡ , prf) =
+  let (y′ , stepʳ , x′≈y′) = bisim .left x≈y stepˡ in
+  y′ , stepʳ , hml-bisim ϕ (R , bisim , x′≈y′) prf
+hml-bisim (⟦ a ⟧ ϕ) (R , bisim , x≈y) prf y′ stepʳ =
+  let (x′ , stepˡ , x′≈y′) = bisim .right x≈y stepʳ in
+  hml-bisim ϕ (R , bisim , x′≈y′) (prf x′ stepˡ)
diff --git a/src/Problem23.agda b/src/Problem23.agda
new file mode 100644
index 0000000..6ee5faf
--- /dev/null
+++ b/src/Problem23.agda
@@ -0,0 +1,136 @@
+{-# OPTIONS --safe #-}
+
+module Problem23 where
+
+open import Data.List
+open import Data.List.Properties
+open import Data.Fin using (fromℕ<)
+open import Data.Fin.Properties using (fromℕ<-cong)
+open import Data.Empty
+open import Data.Nat
+open import Data.Nat.Properties
+open import Data.Product
+open import Function
+open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+open import Relation.Nullary.Negation
+
+open ≡-Reasoning
+
+
+variable State : Set
+variable f : State → State
+
+Assertion : Set → Set₁
+Assertion State = State → Set
+variable ϕ ϕ′ ψ ψ′ π g : Assertion State
+
+_∧_ : Assertion State → Assertion State → Assertion State
+ϕ ∧ ψ = λ σ → ϕ σ × ψ σ
+
+¬'_ : Assertion State → Assertion State
+¬' ϕ = λ σ → (ϕ σ → ⊥)
+
+_⇒_ : Assertion State → Assertion State → Set
+ϕ ⇒ ψ = ∀ σ → ϕ σ → ψ σ
+
+data Program (State : Set) : Set₁ where
+    SKIP : Program State
+    IF_THEN_ELSE_FI : Assertion State → Program State → Program State → Program State
+    WHILE_DO_OD     : Assertion State → Program State → Program State
+    _∶_ : Program State → Program State → Program State
+    UPD : (State → State) → Program State
+
+infixl 5 _∶_
+
+variable P Q : Program State
+
+data ⟨_⟩_⟨_⟩ {State : Set} : Assertion State → Program State → Assertion State → Set₁ where
+    skipₕ : ⟨ ϕ ⟩ SKIP ⟨ ϕ ⟩
+    ifₕ : ⟨ ϕ ∧ g ⟩ P ⟨ ψ ⟩ → ⟨ ϕ ∧ (¬' g) ⟩ Q ⟨ ψ ⟩ → ⟨ ϕ ⟩ IF g THEN P ELSE Q FI ⟨ ψ ⟩
+    whileₕ : ⟨ ϕ ∧ g ⟩ P ⟨ ϕ ⟩ → ⟨ ϕ ⟩ WHILE g DO P OD ⟨ ϕ ∧ (¬' g) ⟩
+    seqₕ : ⟨ ϕ ⟩ P ⟨ π ⟩ → ⟨ π ⟩ Q ⟨ ψ ⟩ → ⟨ ϕ ⟩ P ∶ Q ⟨ ψ ⟩
+    updₕ : ⟨ ϕ ∘ f ⟩ UPD f ⟨ ϕ ⟩
+    conseqₕ : ϕ ⇒ ϕ′ → ⟨ ϕ′ ⟩ P ⟨ ψ′ ⟩ → ψ′ ⇒ ψ → ⟨ ϕ ⟩ P ⟨ ψ ⟩
+
+
+record ListSum : Set where
+    field
+        A : List ℕ
+        s : ℕ
+        i : ℕ
+
+lookup' : List ℕ → ℕ → ℕ
+lookup' V n with n <? length V
+... | yes p = lookup V (fromℕ< p)
+... | no p = 0
+
+open ListSum
+prog : Program ListSum
+prog = UPD (λ σ → record σ { s = 0 })
+     ∶ UPD (λ σ → record σ { i = 0 })
+     ∶ WHILE (λ σ → σ .i ≢ length (σ .A)) DO
+         UPD (λ σ → record σ { s = σ .s + lookup' (σ .A) (σ .i) })
+       ∶ UPD (λ σ → record σ { i = suc (σ .i) })
+       OD
+
+
+goal : ∀ A₀ → ⟨ (λ σ → A₀ ≡ σ .A) ⟩ prog ⟨ (λ σ → σ .s ≡ sum A₀) ⟩
+goal A₀ =
+  conseqₕ
+    (λ σ eq → trans (+-identityʳ (sum (σ .A))) (cong sum (sym eq)) , z≤n)
+    (seqₕ (seqₕ updₕ updₕ)
+      (whileₕ {ϕ = λ σ → sum (drop (σ .i) (σ .A)) + σ .s ≡ sum A₀ × σ .i ≤ length (σ .A)}
+        (conseqₕ
+          (λ σ ((prf , i≤length) , i≢length) →
+            let
+              1+i≤length = ≤∧≢⇒< i≤length i≢length
+
+              prf′ = begin
+                sum (drop (suc (σ .i)) (σ .A)) + (σ .s + lookup' (σ .A) (σ .i)) ≡˘⟨ +-assoc (sum (drop (suc (σ .i)) (σ .A))) _ _ ⟩
+                sum (drop (suc (σ .i)) (σ .A)) + σ .s + lookup' (σ .A) (σ .i)   ≡⟨ +-comm _ (lookup' (σ .A) (σ .i)) ⟩
+                lookup' (σ .A) (σ .i) + (sum (drop (suc (σ .i)) (σ .A)) + σ .s) ≡˘⟨ +-assoc (lookup' (σ .A) (σ .i)) _ _ ⟩
+                lookup' (σ .A) (σ .i) + sum (drop (suc (σ .i)) (σ .A)) + σ .s   ≡⟨ cong (_+ σ .s) (sum-drop-suc (σ .i) (σ .A) 1+i≤length) ⟩
+                sum (drop (σ .i) (σ .A)) + σ .s                                 ≡⟨ prf ⟩
+                sum A₀                                                          ∎
+            in
+            prf′ , 1+i≤length)
+          (seqₕ updₕ updₕ)
+          (λ σ → id))))
+    (λ σ ((prf , i≤length) , ¬i≢length) →
+      let
+        i≡length : σ .i ≡ length (σ .A)
+        i≡length = decidable-stable (σ .i ≟ length (σ .A)) ¬i≢length
+
+        dropᵢ[A]≡[] : drop (σ .i) (σ .A) ≡ []
+        dropᵢ[A]≡[] = length⁻¹ (begin
+          length (drop (σ .i) (σ .A)) ≡⟨  length-drop (σ .i) (σ .A) ⟩
+          length (σ .A) ∸ σ .i        ≡˘⟨ cong (_∸ σ .i) i≡length ⟩
+          σ .i ∸ σ .i                 ≡⟨  n∸n≡0 (σ .i) ⟩
+          0                           ∎)
+      in
+      begin
+        σ .s                            ≡⟨⟩
+        sum [] + σ .s                   ≡˘⟨ cong (λ ◌ → sum ◌ + σ .s) dropᵢ[A]≡[] ⟩
+        sum (drop (σ .i) (σ .A)) + σ .s ≡⟨ prf ⟩
+        sum A₀                          ∎)
+    where
+    length⁻¹ : ∀ {xs : List ℕ} → length xs ≡ 0 → xs ≡ []
+    length⁻¹ {[]} prf = refl
+
+    lookup'-suc : (n x : ℕ) (xs : List ℕ) → lookup' (x ∷ xs) (suc n) ≡ lookup' xs n
+    lookup'-suc n x xs with n <? length xs | suc n <? suc (length xs)
+    ... | yes p₁ | yes p₂ = cong (lookup xs) (fromℕ<-cong n n refl (≤-pred p₂) p₁)
+    ... | yes p₁ | no  p₂ = ⊥-elim (p₂ (s≤s p₁))
+    ... | no  p₁ | yes p₂ = ⊥-elim (p₁ (≤-pred p₂))
+    ... | no  p₁ | no  p₂ = refl
+
+    sum-drop-suc :
+      (n : ℕ) (xs : List ℕ) →
+      .(n < length xs) →
+      lookup' xs n + sum (drop (suc n) xs) ≡ sum (drop n xs)
+    sum-drop-suc zero    (x ∷ xs) _        = refl
+    sum-drop-suc (suc n) (x ∷ xs) n<length = begin
+      lookup' (x ∷ xs) (suc n) + sum (drop (suc n) xs) ≡⟨ cong (_+ sum (drop (suc n) xs)) (lookup'-suc n x xs) ⟩
+      lookup' xs n + sum (drop (suc n) xs)             ≡⟨ sum-drop-suc n xs (≤-pred n<length) ⟩
+      sum (drop n xs)                                  ∎
diff --git a/src/Problem24.agda b/src/Problem24.agda
new file mode 100644
index 0000000..a451432
--- /dev/null
+++ b/src/Problem24.agda
@@ -0,0 +1,155 @@
+{-# OPTIONS --safe #-}
+
+module Problem24 where
+
+open import Data.Bool using (true; false)
+open import Data.Empty using (⊥-elim)
+open import Data.List
+open import Data.List.Properties
+open import Data.List.Relation.Unary.All hiding (toList)
+open import Data.Nat
+open import Data.Nat.Properties
+open import Data.Product
+open import Data.Product.Properties
+open import Relation.Binary.PropositionalEquality hiding ([_])
+open import Relation.Nullary
+
+open ≡-Reasoning
+
+data Tree : Set where
+    Leaf : Tree
+    Branch : Tree → Tree → Tree
+
+toList : ℕ → Tree → List ℕ
+toList d Leaf = [ d ]
+toList d (Branch t₁ t₂) = toList (suc d) t₁ ++ toList (suc d) t₂
+
+-- We write a parser for lists into forests with a labelled root depth, from
+-- right to left.
+--
+-- The empty list is an empty forest.
+--
+-- For a given natural `n` and forest `ts`, we try and merge the labelled tree
+-- `(n , Leaf)` into the forest.
+--
+-- Merging a tree `(n , t)` into a forest `ts` is again done by induction.
+
+LabelledTree : Set
+LabelledTree = ℕ × Tree
+
+Forest : Set
+Forest = List LabelledTree
+
+addTree : LabelledTree → Forest → Forest
+addTree (n , t) []              = [ (n , t) ]
+addTree (n , t) ((k , t′) ∷ ts) with n ≟ k
+... | yes p = addTree (pred n , Branch t t′) ts
+... | no  p = (n , t) ∷ (k , t′) ∷ ts
+
+parseList : List ℕ → Forest
+parseList []       = []
+parseList (x ∷ xs) = addTree (x , Leaf) (parseList xs)
+
+-- Properties ------------------------------------------------------------------
+
+private
+  variable
+    k d : ℕ
+    xs ys : List ℕ
+    t t′ : Tree
+    ts : Forest
+
+-- A forest blocks at `d` if trying to add any `1+n+d` tree fails.
+
+data Blocking (d : ℕ) : (ts : Forest) → Set where
+  empty : Blocking d []
+  cons  : {ts : Forest} → k ≤ d → Blocking d ((k , t) ∷ ts)
+
+-- Adding a tree at a lower depth is blocking, even if it is merged into existing trees.
+
+blocking-addTree :
+  (d≥k : d ≥ k) (t : Tree) (ts : Forest) → Blocking d (addTree (k , t) ts)
+blocking-addTree         d≥k t []              = cons d≥k
+blocking-addTree {k = k} d≥k t ((n , t′) ∷ ts) with k ≟ n
+... | yes refl = blocking-addTree (≤-trans pred[n]≤n d≥k) (Branch t t′) ts
+... | no  p    = cons d≥k
+
+-- Blocking is closed for higher depths
+
+blocking-suc : Blocking d ts → Blocking (suc d) ts
+blocking-suc empty      = empty
+blocking-suc (cons k≤d) = cons (≤-step k≤d)
+
+-- The fundamental theorem of blocking:
+-- if a forest blocks at `d`, adding a tree with depth `1+d` conses the tree
+-- onto the forest.
+
+addTree-blocking[1+n] :
+  (d : ℕ) (t : Tree) {ts : Forest} → Blocking d ts →
+  addTree (suc d , t) ts ≡ (suc d , t) ∷ ts
+addTree-blocking[1+n] d t empty          = refl
+addTree-blocking[1+n] d t (cons {k} k≤d) with suc d ≟ k
+... | yes 1+d≡k = ⊥-elim (≤⇒≯ k≤d (≤-reflexive 1+d≡k))
+... | no  _     = refl
+
+-- Adding two trees of depth `1+n` onto a forest blocking at `n` is equivalent
+-- to adding their composite.
+
+addTree-branch′ :
+  (n : ℕ) (t₁ t₂ : Tree) (ts : Forest) →
+  addTree (suc n , t₁) ((suc n , t₂) ∷ ts) ≡ addTree (n , Branch t₁ t₂) ts
+addTree-branch′ n t₁ t₂ ts with suc n ≟ suc n
+... | yes _ = refl
+... | no  p = ⊥-elim (p refl)
+
+addTree-branch :
+  (n : ℕ) (t₁ t₂ : Tree) {ts : Forest} → Blocking n ts →
+  addTree (suc n , t₁) (addTree (suc n , t₂) ts) ≡ addTree (n , Branch t₁ t₂) ts
+addTree-branch n t₁ t₂ {ts} block = begin
+  addTree (suc n , t₁) (addTree (suc n , t₂) ts) ≡⟨ cong (addTree (suc n , t₁)) (addTree-blocking[1+n] n t₂ block) ⟩
+  addTree (suc n , t₁) ((suc n , t₂) ∷ ts)       ≡⟨ addTree-branch′ n t₁ t₂ ts ⟩
+  addTree (n , Branch t₁ t₂) ts                  ∎
+
+-- Main result of parse: parsing inverts conversion to lists, as long as the
+-- tail blocks.
+--
+-- We prove a blocking lemma at the same time. Using the correctness proof
+-- significantly reduces the amount of work.
+
+blocking-parseList :
+  (d : ℕ) (t : Tree) {xs : List ℕ} → Blocking d (parseList xs) →
+  Blocking d (parseList (toList d t ++ xs))
+parseList-++ :
+  (d : ℕ) (t : Tree) {xs : List ℕ} → Blocking d (parseList xs) →
+  parseList (toList d t ++ xs) ≡ addTree (d , t) (parseList xs)
+
+blocking-parseList d t {xs} block =
+  subst (Blocking d)
+    (sym (parseList-++ d t block))
+    (blocking-addTree ≤-refl t (parseList xs))
+
+parseList-++ d Leaf                block = refl
+parseList-++ d (Branch t₁ t₂) {xs} block = begin
+  parseList ((toList (suc d) t₁ ++ toList (suc d) t₂) ++ xs) ≡⟨ cong parseList (++-assoc (toList (suc d) t₁) (toList (suc d) t₂) xs) ⟩
+  parseList (toList (suc d) t₁ ++ toList (suc d) t₂ ++ xs)   ≡⟨ parseList-++ (suc d) t₁ (blocking-parseList (suc d) t₂ (blocking-suc block)) ⟩
+  addTree (suc d , t₁) (parseList (toList (suc d) t₂ ++ xs)) ≡⟨ cong (addTree (suc d , t₁)) (parseList-++ (suc d) t₂ (blocking-suc block)) ⟩
+  addTree (suc d , t₁) (addTree (suc d , t₂) (parseList xs)) ≡⟨ addTree-branch d t₁ t₂ block ⟩
+  addTree (d , Branch t₁ t₂) (parseList xs)                  ∎
+
+-- Proof that parse is an inverse of `toList` (modulo some wrapping)
+
+parse-correct : (d : ℕ) (t : Tree) → parseList (toList d t) ≡ [ d , t ]
+parse-correct d t = begin
+  parseList (toList d t)       ≡˘⟨ cong parseList (++-identityʳ (toList d t)) ⟩
+  parseList (toList d t ++ []) ≡⟨  parseList-++ d t empty ⟩
+  addTree (d , t) []           ≡⟨⟩
+  [ d , t ]                    ∎
+
+-- Goal
+
+toList-injective : ∀{n} t t′ → toList n t ≡ toList n t′ → t ≡ t′
+toList-injective {n} t t′ eq = ,-injectiveʳ (∷-injectiveˡ (begin
+  [ n , t ]               ≡˘⟨ parse-correct n t ⟩
+  parseList (toList n t)  ≡⟨  cong parseList eq ⟩
+  parseList (toList n t′) ≡⟨  parse-correct n t′ ⟩
+  [ n , t′ ]              ∎))
diff --git a/src/Problem3.agda b/src/Problem3.agda
new file mode 100644
index 0000000..b340df9
--- /dev/null
+++ b/src/Problem3.agda
@@ -0,0 +1,56 @@
+{-# OPTIONS --safe #-}
+
+module Problem3 where
+
+open import Data.List
+open import Relation.Binary.PropositionalEquality
+open import Data.Nat
+open import Data.Empty
+open import Data.Nat.Properties using (≤-step; n<1+n; <⇒≢; module ≤-Reasoning)
+
+data _⊑_ {A : Set} : List A → List A → Set where
+  ⊑-nil  : [] ⊑ []
+  ⊑-cons : ∀{x}{xs ys} → xs ⊑ ys → (x ∷ xs) ⊑ (x ∷ ys)
+  ⊑-skip : ∀{x}{xs ys} → xs ⊑ ys → xs ⊑ (x ∷ ys)
+
+⊑-refl : ∀{A : Set}(xs : List A) → xs ⊑ xs
+⊑-refl []       = ⊑-nil
+⊑-refl (x ∷ xs) = ⊑-cons (⊑-refl xs)
+
+-- Induct on the second relation, then the first.
+⊑-trans : ∀{A : Set}{xs ys zs : List A} → xs ⊑ ys → ys ⊑ zs → xs ⊑ zs
+⊑-trans xs⊑ys          (⊑-skip ys⊑zs) = ⊑-skip (⊑-trans xs⊑ys ys⊑zs)
+⊑-trans ⊑-nil          ⊑-nil          = ⊑-nil
+⊑-trans (⊑-cons xs⊑ys) (⊑-cons ys⊑zs) = ⊑-cons (⊑-trans xs⊑ys ys⊑zs)
+⊑-trans (⊑-skip xs⊑ys) (⊑-cons ys⊑zs) = ⊑-skip (⊑-trans xs⊑ys ys⊑zs)
+
+⊑-len : ∀{A : Set}{xs ys : List A} → xs ⊑ ys → length xs ≤ length ys
+⊑-len ⊑-nil          = z≤n
+⊑-len (⊑-cons xs⊑ys) = s≤s (⊑-len xs⊑ys)
+⊑-len (⊑-skip xs⊑ys) = ≤-step (⊑-len xs⊑ys)
+
+∷-injectiveᵣ : {A : Set} {x y : A} {xs ys : List A} → x ∷ xs ≡ y ∷ ys → xs ≡ ys
+∷-injectiveᵣ refl = refl
+
+private
+  lemma : {A : Set} {w : A} {xs ys zs ws : List A} → xs ≡ w ∷ ws → xs ⊑ ys → ys ≡ zs → zs ⊑ ws → ⊥
+  lemma {w = w} {xs} {ys} {zs} {ws} xs≡w∷ws xs⊑ys ys≡zs zs⊑ws = <⇒≢ prf (cong length (xs≡w∷ws))
+    where
+    open ≤-Reasoning
+    prf : length xs < length (w ∷ ws)
+    prf = begin-strict
+      length xs       ≤⟨ ⊑-len xs⊑ys ⟩
+      length ys       ≡⟨ cong length ys≡zs ⟩
+      length zs       ≤⟨ ⊑-len zs⊑ws ⟩
+      length ws       <⟨ n<1+n (length ws) ⟩
+      length (w ∷ ws) ∎
+
+⊑-antisym-no-K :
+  ∀{A : Set}{xs ys zs ws : List A} → xs ⊑ zs → ws ⊑ ys → xs ≡ ys → zs ≡ ws → xs ≡ zs
+⊑-antisym-no-K ⊑-nil          ⊑-nil          []≡[]     []≡[]′    = refl
+⊑-antisym-no-K (⊑-cons xs⊑zs) (⊑-cons ws⊑ys) x∷xs≡y∷ys x∷zs≡y∷ws = cong (_ ∷_) (⊑-antisym-no-K xs⊑zs ws⊑ys (∷-injectiveᵣ x∷xs≡y∷ys) (∷-injectiveᵣ x∷zs≡y∷ws))
+⊑-antisym-no-K (⊑-skip xs⊑zs) ws⊑ys          xs≡ys     z∷zs≡ws   = ⊥-elim (lemma (sym z∷zs≡ws) ws⊑ys (sym xs≡ys) xs⊑zs)
+⊑-antisym-no-K xs⊑zs          (⊑-skip ws⊑ys) xs≡y∷ys   zs≡ws     = ⊥-elim (lemma xs≡y∷ys       xs⊑zs zs≡ws       ws⊑ys)
+
+⊑-antisym : ∀{A : Set}{xs ys : List A} → xs ⊑ ys → ys ⊑ xs → xs ≡ ys
+⊑-antisym xs⊑ys ys⊑xs = ⊑-antisym-no-K xs⊑ys ys⊑xs refl refl
diff --git a/src/Problem4.agda b/src/Problem4.agda
new file mode 100644
index 0000000..3215dd0
--- /dev/null
+++ b/src/Problem4.agda
@@ -0,0 +1,97 @@
+{-# OPTIONS --safe #-}
+
+module Problem4 where
+
+open import Data.Integer renaming (suc to sucℤ; pred to predℤ) hiding (_≤_)
+open import Data.Nat renaming (_+_ to _ℕ+_)
+open import Data.Nat.Properties using (  +-monoʳ-≤;  +-monoˡ-≤; +-suc; ≤-trans; module ≤-Reasoning )
+open import Data.Integer.Properties using ( +-inverseʳ )
+open import Data.Product
+open import Relation.Binary.PropositionalEquality
+-- The theorems explicitly imported above were useful to prove this!
+
+-- the below theorems are just used to prove the helpers
+open import Data.Integer.Properties using ( ∣m+n∣≤∣m∣+∣n∣; +-assoc; neg-distrib-+; +-comm; +-identityʳ )
+
+Point = ℤ × ℤ
+
+up : Point → Point
+up (x , y) = (x , sucℤ y)
+down : Point → Point
+down (x , y) = (x , predℤ y)
+left : Point → Point
+left (x , y) = (predℤ x , y)
+right : Point → Point
+right (x , y) = (sucℤ x , y)
+
+data OrthoPath (p : Point) : Point → Set where
+   move-up : ∀ {q} → OrthoPath (up p) q → OrthoPath p q
+   move-down : ∀ {q} → OrthoPath (down p) q → OrthoPath p q
+   move-left : ∀ {q} → OrthoPath (left p) q → OrthoPath p q
+   move-right : ∀ {q} → OrthoPath (right p) q → OrthoPath p q
+   stop : OrthoPath p p
+
+path-length : ∀{p q} → OrthoPath p q → ℕ
+path-length (move-up p) = suc (path-length p)
+path-length (move-down p) = suc (path-length p)
+path-length (move-left p) = suc (path-length p)
+path-length (move-right p) = suc (path-length p)
+path-length stop = 0
+
+manhattan : Point → Point → ℕ
+manhattan (x₁ , y₁) (x₂ , y₂) = ∣ (x₂ - x₁) ∣ ℕ+ ∣ (y₂ - y₁) ∣
+
+helper-sucℤ : ∀(a b : ℤ) → ∣ (a - b) ∣ ≤ suc ∣ (a - sucℤ b) ∣
+helper-sucℤ a b rewrite
+    sym (+-identityʳ (- b))
+  | sym (+-assoc (- b) (- 1ℤ) 1ℤ)
+  | sym (+-comm (- 1ℤ) (- b))
+  | sym (neg-distrib-+ 1ℤ b)
+  | sym (+-assoc a (- sucℤ b) 1ℤ)
+  | +-comm (a - sucℤ b) 1ℤ
+  = ∣m+n∣≤∣m∣+∣n∣ (1ℤ) (a - sucℤ b)
+
+helper-predℤ : ∀(a b : ℤ) → ∣ (a - b) ∣ ≤ suc ∣ (a - predℤ b) ∣
+helper-predℤ a b rewrite
+    sym (+-identityʳ (- b))
+  | sym (+-assoc (- b) 1ℤ -1ℤ)
+  | sym (+-comm 1ℤ (- b))
+  | sym (neg-distrib-+ -1ℤ b)
+  | sym (+-assoc a (- predℤ b) -1ℤ )
+  | +-comm (a - predℤ b) -1ℤ
+  = ∣m+n∣≤∣m∣+∣n∣ (-1ℤ) (a - predℤ b)
+
+open ≤-Reasoning
+
+goal : ∀(p q : Point) → (path : OrthoPath p q) → manhattan p q ≤ path-length path
+goal p@(px , py) q@(qx , qy) (move-up path) = begin
+  manhattan p q                           ≡⟨⟩
+  ∣ (qx - px) ∣ ℕ+ ∣ (qy - py) ∣          ≤⟨ +-monoʳ-≤ ∣ (qx - px) ∣ (helper-sucℤ qy py) ⟩
+  ∣ (qx - px) ∣ ℕ+ suc ∣ (qy - sucℤ py) ∣ ≡⟨ +-suc ∣ (qx - px) ∣ ∣ (qy - sucℤ py) ∣ ⟩
+  suc ∣ (qx - px) ∣ ℕ+ ∣ (qy - sucℤ py) ∣ ≡⟨⟩
+  suc (manhattan (up p) q)                ≤⟨ s≤s (goal (up p) q path) ⟩
+  suc (path-length path)                  ∎
+goal p@(px , py) q@(qx , qy) (move-down path) = begin
+  manhattan p q                            ≡⟨⟩
+  ∣ (qx - px) ∣ ℕ+ ∣ (qy - py) ∣           ≤⟨ +-monoʳ-≤ ∣ (qx - px) ∣ (helper-predℤ qy py) ⟩
+  ∣ (qx - px) ∣ ℕ+ suc ∣ (qy - predℤ py) ∣ ≡⟨ +-suc ∣ (qx - px) ∣ ∣ (qy - predℤ py) ∣ ⟩
+  suc ∣ (qx - px) ∣ ℕ+ ∣ (qy - predℤ py) ∣ ≡⟨⟩
+  suc (manhattan (down p) q)               ≤⟨ s≤s (goal (down p) q path) ⟩
+  suc (path-length path)                   ∎
+goal p@(px , py) q@(qx , qy) (move-left path) = begin
+  manhattan p q                            ≡⟨⟩
+  ∣ (qx - px) ∣ ℕ+ ∣ (qy - py) ∣           ≤⟨ +-monoˡ-≤ ∣ (qy - py) ∣ (helper-predℤ qx px) ⟩
+  suc ∣ (qx - predℤ px) ∣ ℕ+ ∣ (qy - py) ∣ ≡⟨⟩
+  suc (manhattan (left p) q)               ≤⟨ s≤s (goal (left p) q path) ⟩
+  suc (path-length path)                   ∎
+goal p@(px , py) q@(qx , qy) (move-right path) = begin
+  manhattan p q                           ≡⟨⟩
+  ∣ (qx - px) ∣ ℕ+ ∣ (qy - py) ∣          ≤⟨ +-monoˡ-≤ ∣ (qy - py) ∣ (helper-sucℤ qx px) ⟩
+  suc ∣ (qx - sucℤ px) ∣ ℕ+ ∣ (qy - py) ∣ ≡⟨⟩
+  suc (manhattan (right p) q)             ≤⟨ s≤s (goal (right p) q path) ⟩
+  suc (path-length path)                  ∎
+goal p@(px , py) .p stop = begin
+  manhattan p p                  ≡⟨⟩
+  ∣ (px - px) ∣ ℕ+ ∣ (py - py) ∣ ≡⟨ cong₂ (λ ◌ᵃ ◌ᵇ → ∣ ◌ᵃ ∣ ℕ+ ∣ ◌ᵇ ∣) (+-inverseʳ px) (+-inverseʳ py) ⟩
+  0 ℕ+ 0                         ≡⟨⟩
+  0                              ∎
diff --git a/src/Problem5.agda b/src/Problem5.agda
new file mode 100644
index 0000000..b2ab10d
--- /dev/null
+++ b/src/Problem5.agda
@@ -0,0 +1,44 @@
+{-# OPTIONS --safe #-}
+
+module Problem5 where
+
+open import Data.List
+open import Data.List.Properties using (++-assoc; ++-identityʳ)
+open import Data.Product
+open import Relation.Binary.PropositionalEquality hiding ([_])
+
+data Symbol : Set where
+   ⟨ : Symbol
+   ⟩ : Symbol
+
+data M : List Symbol → Set where
+    M-empty : M []
+    M-juxt  : ∀{a b} → M a → M b → M (a ++ b)
+    M-nest  : ∀{a} → M a → M (⟨ ∷ a ++ [ ⟩ ])
+
+data ListOf (P : List Symbol → Set) : List Symbol → Set where
+    ListOf-empty : ListOf P []
+    ListOf-cons  : ∀{a b} → P a → ListOf P b → ListOf P (a ++ b)
+
+data N : List Symbol → Set where
+    N-nest : ∀{a} → ListOf N a → N (⟨ ∷ a ++ [ ⟩ ])
+
+L = ListOf N
+
+ListOf-++ : {P : List Symbol → Set} {xs ys : List Symbol} → ListOf P xs → ListOf P ys → ListOf P (xs ++ ys)
+ListOf-++ ListOf-empty pys = pys
+ListOf-++ {ys = ys} (ListOf-cons {xs₁} {xs₂} px pxs) pys =
+  subst (ListOf _) (sym (++-assoc xs₁ xs₂ ys)) (ListOf-cons px (ListOf-++ pxs pys))
+
+
+goal : ∀{s} → M s → L s
+goal M-empty        = ListOf-empty
+goal (M-juxt m₁ m₂) = ListOf-++ (goal m₁) (goal m₂)
+goal (M-nest m)     = subst L (++-assoc (⟨ ∷ _) [ ⟩ ] []) (ListOf-cons (N-nest (goal m)) ListOf-empty)
+
+-- The other direction is straightforward in Agda but extremely difficult in Lean!
+-- goal₁ : ∀{s} → L s → M s
+-- goal₂ : ∀{s} → N s → M s
+-- goal₁ ListOf-empty = M-empty
+-- goal₁ (ListOf-cons x l) = M-juxt (goal₂ x) (goal₁ l)
+-- goal₂ (N-nest x) = M-nest (goal₁ x)
diff --git a/src/Problem6.agda b/src/Problem6.agda
new file mode 100644
index 0000000..90e8526
--- /dev/null
+++ b/src/Problem6.agda
@@ -0,0 +1,239 @@
+{-# OPTIONS --safe #-}
+
+module Problem6 where
+
+open import Data.Nat
+open import Data.Nat.Properties using (1+n≢0; +-assoc; +-identityʳ)
+open import Data.Empty using (⊥-elim)
+open import Data.Fin using (Fin; suc; raise; inject+)
+open import Data.Fin.Patterns
+open import Data.Fin.Properties using (toℕ-injective; toℕ-inject+)
+open import Data.List
+open import Data.List.Properties using (++-assoc; ++-identityʳ)
+open import Data.Product using (_×_; _,_)
+open import Relation.Binary.PropositionalEquality hiding ([_])
+
+open ≡-Reasoning
+
+data Expr : Set where
+  Const : ℕ → Expr
+  _⊞_ : Expr → Expr → Expr
+  _⊠_ : Expr → Expr → Expr
+
+eval : Expr → ℕ
+eval (Const x) = x
+eval (p ⊞ q) = eval p + eval q
+eval (p ⊠ q) = eval p * eval q
+
+data Instr : Set where
+  Push : ℕ → Instr
+  Mult Add : Instr
+
+instr-semantics : Instr → List ℕ → List ℕ
+instr-semantics (Push x) s       = x ∷ s
+instr-semantics Mult (y ∷ x ∷ s) = x * y ∷ s
+instr-semantics Add  (y ∷ x ∷ s) = x + y ∷ s
+instr-semantics _ _ = []
+
+execute : List Instr → List ℕ → List ℕ
+execute []       s = s
+execute (i ∷ is) s = execute is (instr-semantics i s)
+
+compile : Expr → List Instr
+compile (Const x) = [ Push x ]
+compile (e₁ ⊞ e₂) = compile e₁ ++ compile e₂ ++ [ Add  ]
+compile (e₁ ⊠ e₂) = compile e₁ ++ compile e₂ ++ [ Mult ]
+
+-- Use difference lists because they are nicer to work with.
+
+compile′ : Expr → List Instr → List Instr
+compile′ (Const x) is = Push x ∷ is
+compile′ (e₁ ⊞ e₂) is = compile′ e₁ (compile′ e₂ (Add ∷ is))
+compile′ (e₁ ⊠ e₂) is = compile′ e₁ (compile′ e₂ (Mult ∷ is))
+
+compile≗compile′ : ∀ e is → compile e ++ is ≡ compile′ e is
+compile≗compile′ (Const x) is = refl
+compile≗compile′ (e₁ ⊞ e₂) is = begin
+  (compile e₁ ++ compile e₂ ++ [ Add ]) ++ is ≡⟨ ++-assoc (compile e₁) (compile e₂ ++ [ Add ]) is ⟩
+  compile e₁ ++ (compile e₂ ++ [ Add ]) ++ is ≡⟨ cong (compile e₁ ++_) (++-assoc (compile e₂) [ Add ] is) ⟩
+  compile e₁ ++ compile e₂ ++ Add ∷ is        ≡⟨ cong (compile e₁ ++_) (compile≗compile′ e₂ (Add ∷ is)) ⟩
+  compile e₁ ++ compile′ e₂ (Add ∷ is)        ≡⟨ compile≗compile′ e₁ (compile′ e₂ (Add ∷ is)) ⟩
+  compile′ e₁ (compile′ e₂ (Add ∷ is))        ∎
+compile≗compile′ (e₁ ⊠ e₂) is = begin
+  (compile e₁ ++ compile e₂ ++ [ Mult ]) ++ is ≡⟨ ++-assoc (compile e₁) (compile e₂ ++ [ Mult ]) is ⟩
+  compile e₁ ++ (compile e₂ ++ [ Mult ]) ++ is ≡⟨ cong (compile e₁ ++_) (++-assoc (compile e₂) [ Mult ] is) ⟩
+  compile e₁ ++ compile e₂ ++ Mult ∷ is        ≡⟨ cong (compile e₁ ++_) (compile≗compile′ e₂ (Mult ∷ is)) ⟩
+  compile e₁ ++ compile′ e₂ (Mult ∷ is)        ≡⟨ compile≗compile′ e₁ (compile′ e₂ (Mult ∷ is)) ⟩
+  compile′ e₁ (compile′ e₂ (Mult ∷ is))        ∎
+
+-- Generalise expressions to open terms
+
+data Expr′ (n : ℕ) : Set where
+  Var   : Fin n → Expr′ n
+  Const : ℕ → Expr′ n
+  _⊞_   : Expr′ n → Expr′ n → Expr′ n
+  _⊠_   : Expr′ n → Expr′ n → Expr′ n
+
+forget : Expr → Expr′ 0
+forget (Const x) = Const x
+forget (e₁ ⊞ e₂) = forget e₁ ⊞ forget e₂
+forget (e₁ ⊠ e₂) = forget e₁ ⊠ forget e₂
+
+eval′ : ∀ {n} → Expr′ n → (Fin n → ℕ) → ℕ
+eval′ (Var x)   γ = γ x
+eval′ (Const x) γ = x
+eval′ (e₁ ⊞ e₂) γ = eval′ e₁ γ + eval′ e₂ γ
+eval′ (e₁ ⊠ e₂) γ = eval′ e₁ γ * eval′ e₂ γ
+
+eval′-correct : (e : Expr) → eval′ (forget e) (λ ()) ≡ eval e
+eval′-correct (Const x) = refl
+eval′-correct (e₁ ⊞ e₂) = cong₂ _+_ (eval′-correct e₁) (eval′-correct e₂)
+eval′-correct (e₁ ⊠ e₂) = cong₂ _*_ (eval′-correct e₁) (eval′-correct e₂)
+
+-- We can substitute free variables.
+
+wkn : ∀ {k} n → Expr′ k → Expr′ (k + n)
+wkn n (Var x)   = Var (inject+ n x)
+wkn n (Const x) = Const x
+wkn n (e₁ ⊞ e₂) = wkn n e₁ ⊞ wkn n e₂
+wkn n (e₁ ⊠ e₂) = wkn n e₁ ⊠ wkn n e₂
+
+sub : ∀ {k n} → Expr′ k → Expr′ (suc n) → Expr′ (k + n)
+sub         e′ (Var 0F)      = wkn _ e′
+sub {k = k} e′ (Var (suc i)) = Var (raise k i)
+sub         e′ (Const x)     = Const x
+sub         e′ (e₁ ⊞ e₂)     = sub e′ e₁ ⊞ sub e′ e₂
+sub         e′ (e₁ ⊠ e₂)     = sub e′ e₁ ⊠ sub e′ e₂
+
+-- These facts generalise to `n` variables, but the types are nasty
+
+wkn0 : (e : Expr′ 0) → wkn 0 e ≡ e
+wkn0 (Const x) = refl
+wkn0 (e₁ ⊞ e₂) = cong₂ _⊞_ (wkn0 e₁) (wkn0 e₂)
+wkn0 (e₁ ⊠ e₂) = cong₂ _⊠_ (wkn0 e₁) (wkn0 e₂)
+
+wkn-assoc : ∀ k n (e : Expr′ 0) → wkn (k + n) e ≡ wkn n (wkn k e)
+wkn-assoc k n (Const x) = refl
+wkn-assoc k n (e₁ ⊞ e₂) = cong₂ _⊞_ (wkn-assoc k n e₁) (wkn-assoc k n e₂)
+wkn-assoc k n (e₁ ⊠ e₂) = cong₂ _⊠_ (wkn-assoc k n e₁) (wkn-assoc k n e₂)
+
+sub-wkn : (e′ : Expr′ 0) (e : Expr′ 0) → sub e′ (wkn 1 e) ≡ e
+sub-wkn e′ (Const x) = refl
+sub-wkn e′ (e₁ ⊞ e₂) = cong₂ _⊞_ (sub-wkn e′ e₁) (sub-wkn e′ e₂)
+sub-wkn e′ (e₁ ⊠ e₂) = cong₂ _⊠_ (sub-wkn e′ e₁) (sub-wkn e′ e₂)
+
+wkn-sub : ∀ {k} n (e′ : Expr′ 0) (e : Expr′ (suc k)) → sub e′ (wkn n e) ≡ wkn n (sub e′ e)
+wkn-sub n e′ (Const x) = refl
+wkn-sub n e′ (e₁ ⊞ e₂) = cong₂ _⊞_ (wkn-sub n e′ e₁) (wkn-sub n e′ e₂)
+wkn-sub n e′ (e₁ ⊠ e₂) = cong₂ _⊠_ (wkn-sub n e′ e₁) (wkn-sub n e′ e₂)
+wkn-sub n e′ (Var 0F)      = wkn-assoc _ n e′
+wkn-sub n e′ (Var (suc i)) = refl
+
+sub-assoc :
+  ∀ {m n} (e₁ : Expr′ 0) (e₂ : Expr′ (suc m)) (e₃ : Expr′ (suc n)) →
+  sub e₁ (sub e₂ e₃) ≡ sub (sub e₁ e₂) e₃
+sub-assoc e₁ e₂ (Const x) = refl
+sub-assoc e₁ e₂ (e₃ ⊞ e₄) = cong₂ _⊞_ (sub-assoc e₁ e₂ e₃) (sub-assoc e₁ e₂ e₄)
+sub-assoc e₁ e₂ (e₃ ⊠ e₄) = cong₂ _⊠_ (sub-assoc e₁ e₂ e₃) (sub-assoc e₁ e₂ e₄)
+sub-assoc e₁ e₂ (Var 0F)      = wkn-sub _ e₁ e₂
+sub-assoc e₁ e₂ (Var (suc i)) = refl
+
+-- I want to work only on well-formed instruction sequences. A sequence "eats"
+-- `n` arguments if correct execution requires `n` elements on the stack.
+--
+-- The arity of an instruction gives how many arguments it consumes.
+
+arity : Instr → ℕ
+arity (Push x) = 0
+arity Add      = 2
+arity Mult     = 2
+
+data WellFormed : List Instr → ℕ → Set where
+  []   : WellFormed [] 1
+  _∷_  : ∀ {is n} → (i : Instr) → WellFormed is (suc n) → WellFormed (i ∷ is) (arity i + n)
+
+-- Compilation only produces well-formed sequences that produce one element.
+
+compile′-wf : ∀ {n is} (e : Expr) → WellFormed is (suc n) → WellFormed (compile′ e is) n
+compile′-wf (Const x) wf = Push x ∷ wf
+compile′-wf (e₁ ⊞ e₂) wf = compile′-wf e₁ (compile′-wf e₂ (Add ∷ wf))
+compile′-wf (e₁ ⊠ e₂) wf = compile′-wf e₁ (compile′-wf e₂ (Mult ∷ wf))
+
+-- We can form open expressions from instruction sequences.
+
+decompile₁ : (i : Instr) → Expr′ (arity i)
+decompile₁ (Push x) = Const x
+decompile₁ Add      = Var 1F ⊞ Var 0F
+decompile₁ Mult     = Var 1F ⊠ Var 0F
+
+decompile : ∀ {n is} → WellFormed is n → Expr′ n
+decompile []       = Var 0F
+decompile (i ∷ wf) = sub (decompile₁ i) (decompile wf)
+
+-- Provide semantics for function environments
+
+instr-semantics′ : ∀ {n} (i : Instr) → (Fin (arity i + n) → ℕ) → Fin (suc n) → ℕ
+instr-semantics′ i        f (suc x) = f (raise (arity i) x)
+instr-semantics′ (Push x) f 0F      = x
+instr-semantics′ Add      f 0F      = f 1F + f 0F
+instr-semantics′ Mult     f 0F      = f 1F * f 0F
+
+instr-semantics-cong :
+  ∀ (i : Instr) {n xs} {f : Fin (arity i + n) → ℕ} →
+  xs ≡ tabulate f → instr-semantics i xs ≡ tabulate (instr-semantics′ i f)
+instr-semantics-cong (Push x) refl = refl
+instr-semantics-cong Add      refl = refl
+instr-semantics-cong Mult     refl = refl
+
+-- Prove decompilation is correct
+
+eval-sub :
+  ∀ (i : Instr) {n} (f : Fin (arity i + n) → ℕ) (e : Expr′ (suc n)) →
+  eval′ e (instr-semantics′ i f) ≡ eval′ (sub (decompile₁ i) e) f
+eval-sub i f (Const x)     = refl
+eval-sub i f (e₁ ⊞ e₂)     = cong₂ _+_ (eval-sub i f e₁) (eval-sub i f e₂)
+eval-sub i f (e₁ ⊠ e₂)     = cong₂ _*_ (eval-sub i f e₁) (eval-sub i f e₂)
+eval-sub i f (Var (suc x)) = refl
+eval-sub (Push x) f (Var 0F) = refl
+eval-sub Add      f (Var 0F) = refl
+eval-sub Mult     f (Var 0F) = refl
+
+eval-decompile :
+  ∀ {n is} (wf : WellFormed is n) (xs : List ℕ) (f : Fin n → ℕ) →
+  xs ≡ tabulate f → execute is xs ≡ [ eval′ (decompile wf) f ]
+eval-decompile [] xs f xs≡f = xs≡f
+eval-decompile {is = .i ∷ is} (i ∷ wf) xs f xs≡f = begin
+  execute is (instr-semantics i xs)               ≡⟨ eval-decompile wf (instr-semantics i xs) (instr-semantics′ i f) (instr-semantics-cong i xs≡f) ⟩
+  [ eval′ (decompile wf) (instr-semantics′ i f) ] ≡⟨ cong [_] (eval-sub i f (decompile wf)) ⟩
+  [ eval′ (sub (decompile₁ i) (decompile wf)) f ] ∎
+
+-- Prove decompilation is an inverse
+
+decompile-compile′ : ∀ {is n} (e : Expr) (wf : WellFormed is (suc n)) → decompile (compile′-wf e wf) ≡ sub (forget e) (decompile wf)
+decompile-compile′ (Const x) wf = refl
+decompile-compile′ (e₁ ⊞ e₂) wf = begin
+  decompile (compile′-wf e₁ (compile′-wf e₂ (Add ∷ wf)))                       ≡⟨ decompile-compile′ e₁ (compile′-wf e₂ (Add ∷ wf)) ⟩
+  sub (forget e₁) (decompile (compile′-wf e₂ (Add ∷ wf)))                      ≡⟨ cong (sub (forget e₁)) (decompile-compile′ e₂ (Add ∷ wf)) ⟩
+  sub (forget e₁) (sub (forget e₂) (sub (Var 1F ⊞ Var 0F) (decompile wf)))     ≡⟨ cong (sub (forget e₁)) (sub-assoc (forget e₂) (Var 1F ⊞ Var 0F) (decompile wf)) ⟩
+  sub (forget e₁) (sub (Var 0F ⊞ wkn 1 (forget e₂)) (decompile wf))            ≡⟨ sub-assoc (forget e₁) (Var 0F ⊞ wkn 1 (forget e₂)) (decompile wf) ⟩
+  sub (wkn 0 (forget e₁) ⊞ sub (forget e₁) (wkn 1 (forget e₂))) (decompile wf) ≡⟨ cong₂ (λ -₁ -₂ → sub (-₁ ⊞ -₂) (decompile wf)) (wkn0 (forget e₁)) (sub-wkn (forget e₁) (forget e₂)) ⟩
+  sub (forget e₁ ⊞ forget e₂) (decompile wf)                                   ∎
+decompile-compile′ (e₁ ⊠ e₂) wf = begin
+  decompile (compile′-wf e₁ (compile′-wf e₂ (Mult ∷ wf)))                      ≡⟨ decompile-compile′ e₁ (compile′-wf e₂ (Mult ∷ wf)) ⟩
+  sub (forget e₁) (decompile (compile′-wf e₂ (Mult ∷ wf)))                     ≡⟨ cong (sub (forget e₁)) (decompile-compile′ e₂ (Mult ∷ wf)) ⟩
+  sub (forget e₁) (sub (forget e₂) (sub (Var 1F ⊠ Var 0F) (decompile wf)))     ≡⟨ cong (sub (forget e₁)) (sub-assoc (forget e₂) (Var 1F ⊠ Var 0F) (decompile wf)) ⟩
+  sub (forget e₁) (sub (Var 0F ⊠ wkn 1 (forget e₂)) (decompile wf))            ≡⟨ sub-assoc (forget e₁) (Var 0F ⊠ wkn 1 (forget e₂)) (decompile wf) ⟩
+  sub (wkn 0 (forget e₁) ⊠ sub (forget e₁) (wkn 1 (forget e₂))) (decompile wf) ≡⟨ cong₂ (λ -₁ -₂ → sub (-₁ ⊠ -₂) (decompile wf)) (wkn0 (forget e₁)) (sub-wkn (forget e₁) (forget e₂)) ⟩
+  sub (forget e₁ ⊠ forget e₂) (decompile wf)                                   ∎
+
+-- Prove evaluation correct.
+
+compile-correct : ∀ e → execute (compile e) [] ≡ [ eval e ]
+compile-correct e = begin
+  execute (compile e) []                          ≡˘⟨ cong (λ - → execute - []) (++-identityʳ (compile e)) ⟩
+  execute (compile e ++ []) []                    ≡⟨ cong (λ - → execute - []) (compile≗compile′ e []) ⟩
+  execute (compile′ e []) []                      ≡⟨ eval-decompile (compile′-wf e []) [] (λ ()) refl ⟩
+  [ eval′ (decompile (compile′-wf e [])) (λ ()) ] ≡⟨ cong (λ - → [ eval′ - (λ ()) ]) (decompile-compile′ e []) ⟩
+  [ eval′ (wkn 0 (forget e)) (λ ()) ]             ≡⟨ cong (λ - → [ eval′ - (λ ()) ]) (wkn0 (forget e)) ⟩
+  [ eval′ (forget e) (λ ()) ]                     ≡⟨ cong [_] (eval′-correct e) ⟩
+  [ eval e ]                                      ∎
diff --git a/src/Problem7.agda b/src/Problem7.agda
new file mode 100644
index 0000000..4566abb
--- /dev/null
+++ b/src/Problem7.agda
@@ -0,0 +1,54 @@
+{-# OPTIONS --safe #-}
+
+module Problem7 where
+
+open import Data.Product
+open import Data.Nat
+open import Data.Nat.Properties using (+-comm)
+open import Function.Base using (_∘_)
+open import Relation.Binary.PropositionalEquality hiding ([_])
+open import Relation.Nullary
+
+repeat : ∀{A : Set}(f : A → A) → ℕ → A → A
+repeat f zero x = x
+repeat f (suc n) x = f (repeat f n x)
+
+-- `repeat f` commutes with `g` if `f` commutes with `g`
+
+repeat-comm :
+  {A : Set} (f g : A → A) (comm : f ∘ g ≗ g ∘ f) (n : ℕ) →
+   repeat f n ∘ g ≗ g ∘ repeat f n
+repeat-comm f g comm zero x = refl
+repeat-comm f g comm (suc n) x =
+  trans
+    (cong f (repeat-comm f g comm n x))
+    (comm (repeat f n x))
+
+module _ (T : Set)(f : T → T) where
+
+  hare tortoise : T × T → T × T
+  hare p  = ( proj₁ p , f (proj₂ p) )
+  tortoise p = ( f (proj₁ p) , proj₂ p )
+
+  data Run : T × T → (length : ℕ) → Set where
+    empty : ∀{c} → Run (c , c) 0
+    step  : ∀{n}{p} → Run (tortoise p) n → Run p (suc n)
+
+  Loop : ℕ → Set
+  Loop n = ∃[ i ] Run (i , i) n
+
+  race : T × T → T × T
+  race p = hare (hare (tortoise p))
+
+  -- The invariant for the race.
+
+  invariant : (x : T) (n : ℕ) → Run (repeat race n (x , x)) n
+  invariant x zero = empty
+  invariant x (suc n) =
+    let run = invariant (f (f x)) n in
+    step (subst (λ - → Run - n)
+      (repeat-comm race (tortoise ∘ race) (λ _ → refl) n (x , x))
+      run)
+
+  goal : ∀{x c : T} n → repeat race n (x , x) ≡ (c , c) → Loop n
+  goal {x} n prf = -, subst (λ - → Run - n) prf (invariant x n)
diff --git a/src/Problem8.agda b/src/Problem8.agda
new file mode 100644
index 0000000..9329964
--- /dev/null
+++ b/src/Problem8.agda
@@ -0,0 +1,109 @@
+{-# OPTIONS --safe #-}
+
+module Problem8 where
+
+open import Data.Nat hiding (_≟_)
+open import Data.Product hiding (map)
+open import Data.Bool
+open import Relation.Nullary
+open import Relation.Binary.PropositionalEquality hiding ([_])
+open import Data.Empty
+open import Data.Vec
+open import Data.Bool.Properties using (¬-not; not-¬)
+
+open ≡-Reasoning
+
+data CompressedString : ℕ → Set where
+    empty : CompressedString 0
+    one   : Bool → (n : ℕ) → CompressedString (suc n)
+    cons  : ∀{m} → (n : ℕ) → CompressedString (suc m) → CompressedString (suc (suc (n + m)))
+
+head-c : ∀{n} → CompressedString (suc n) → Bool
+head-c (one x n) = x
+head-c (cons n str) = not (head-c str)
+
+tail-c : ∀{n} → CompressedString (suc n) → CompressedString n
+tail-c (one x zero) = empty
+tail-c (one x (suc n)) = one x n
+tail-c (cons zero str) = str
+tail-c (cons (suc n) str) = cons n str
+
+cons-c : ∀{n} → Bool → CompressedString  n → CompressedString (suc n)
+cons-c b empty = one b 0
+cons-c b (one x n) with b ≟ x
+... | yes _ = one x (suc n)
+... | no  _ = cons 0 (one x n)
+cons-c b (cons n str) with b ≟ head-c (cons n str)
+... | yes _ = cons (suc n) str
+... | no  _ = cons 0 (cons n str)
+
+
+compress : ∀{n} → Vec Bool n → CompressedString n
+compress [] = empty
+compress (l ∷ ls) = cons-c l (compress ls)
+
+
+decompress : ∀{n} → CompressedString n → Vec Bool n
+decompress {zero} empty = []
+decompress {suc n} str = head-c str ∷ decompress (tail-c str)
+
+-- Consing the opposite element introduces a cons constructor.
+
+cons-c-¬head : ∀ {n} (xs : CompressedString (suc n)) → cons-c (not (head-c xs)) xs ≡ cons zero xs
+cons-c-¬head (one x _) with not x ≟ x
+... | yes ¬x≡x = ⊥-elim (not-¬ refl (sym ¬x≡x))
+... | no _ = refl
+cons-c-¬head (cons n xs) with not (not (head-c xs)) ≟ not (head-c xs)
+... | yes ¬¬x≡¬x = ⊥-elim (not-¬ refl (sym ¬¬x≡¬x))
+... | no _ = refl
+
+-- Eta equality
+
+cons-c∘<head-c,tail-c> : ∀ {n} (xs : CompressedString (suc n)) → cons-c (head-c xs) (tail-c xs) ≡ xs
+cons-c∘<head-c,tail-c> (one x zero) = refl
+cons-c∘<head-c,tail-c> (one x (suc n)) with x ≟ x
+... | yes _ = refl
+... | no x≢x = ⊥-elim (x≢x refl)
+cons-c∘<head-c,tail-c> (cons zero xs) = cons-c-¬head xs
+cons-c∘<head-c,tail-c> (cons (suc n) xs) with not (head-c xs) ≟ not (head-c xs)
+... | yes _ = refl
+... | no x≢x = ⊥-elim (x≢x refl)
+
+-- Beta equalities
+
+head-c∘cons-c : ∀ {n} x (xs : CompressedString n) → head-c (cons-c x xs) ≡ x
+head-c∘cons-c x empty = refl
+head-c∘cons-c x (one y n) with x ≟ y
+... | yes x≡y = sym x≡y
+... | no x≢y = sym (¬-not x≢y)
+head-c∘cons-c x (cons n xs) with x ≟ not (head-c xs)
+... | yes x≡¬y = sym x≡¬y
+... | no x≢¬y = sym (¬-not x≢¬y)
+
+tail-c∘cons-c : ∀ {n} x (xs : CompressedString n) → tail-c (cons-c x xs) ≡ xs
+tail-c∘cons-c x empty = refl
+tail-c∘cons-c x (one y n) with x ≟ y
+... | yes _ = refl
+... | no _ = refl
+tail-c∘cons-c x (cons n xs) with x ≟ not (head-c xs)
+... | yes _ = refl
+... | no _ = refl
+
+-- Goals
+
+prf₁ : ∀{n} (xs : CompressedString n) → compress (decompress xs) ≡ xs
+prf₁ {zero} empty = refl
+prf₁ {suc n} xs = begin
+  cons-c (head-c xs) (compress (decompress (tail-c xs))) ≡⟨ cong (cons-c (head-c xs)) (prf₁ (tail-c xs)) ⟩
+  cons-c (head-c xs) (tail-c xs)                         ≡⟨ cons-c∘<head-c,tail-c> xs ⟩
+  xs                                                     ∎
+
+prf₂ : ∀{n} (xs : Vec Bool n) → decompress (compress xs) ≡ xs
+prf₂ [] = refl
+prf₂ (x ∷ xs) =
+  cong₂ _∷_
+    (head-c∘cons-c x (compress xs))
+    (begin
+      decompress (tail-c (cons-c x (compress xs))) ≡⟨ cong decompress (tail-c∘cons-c x (compress xs)) ⟩
+      decompress (compress xs)                     ≡⟨ prf₂ xs ⟩
+      xs                                           ∎)
diff --git a/src/Problem9.agda b/src/Problem9.agda
new file mode 100644
index 0000000..9bc5a61
--- /dev/null
+++ b/src/Problem9.agda
@@ -0,0 +1,102 @@
+{-# OPTIONS --safe #-}
+
+module Problem9 where
+
+open import Data.Nat
+open import Relation.Binary.PropositionalEquality
+open import Data.Maybe as Maybe using (Maybe; just; nothing)
+open import Relation.Nullary
+open import Data.List
+open import Data.Nat.Properties using (suc-injective)
+open import Data.List.Properties using (++-identityʳ;length-++; ++-assoc;unfold-reverse; length-reverse)
+
+open ≡-Reasoning
+
+variable A : Set
+
+record Queue A : Set where
+  constructor Q
+  field
+    size-front  : ℕ
+    size-back   : ℕ
+    front : List A
+    back  : List A
+
+    invariant : size-back ≤ size-front
+    size-inv₁ : length front ≡ size-front
+    size-inv₂ : length back ≡ size-back
+open Queue
+
+record CorrectQueue (Q : Set → Set) : Set₁ where
+  field
+    abstraction : Q A → List A
+    enqueue     : A → Q A → Q A
+    dequeue     : Q A → Maybe (Q A)
+    first       : Q A → Maybe A
+    size        : Q A → ℕ
+    empty       : Q A
+
+    emptyᵣ      : abstraction (empty {A}) ≡ []
+    sizeᵣ       : ∀ (q : Q A) → size q ≡ length (abstraction q)
+    firstᵣ      : ∀ (q : Q A) → first q ≡ head (abstraction q)
+    dequeueᵣ    : ∀ (q : Q A) → Maybe.map abstraction (dequeue q) ≡ tail (abstraction q)
+    enqueueᵣ    : ∀ (q : Q A) x → abstraction (enqueue x q) ≡ abstraction q ∷ʳ x
+
+enqueueQ  : A → Queue A → Queue A
+enqueueQ x q with suc (size-back q) ≤? size-front  q
+... | yes p = Q (size-front q) (suc (size-back q)) (front q) (x ∷ back q) p (size-inv₁ q) (cong suc (size-inv₂ q))
+... | no  p = Q (size-front q + suc (size-back q)) 0 (front q ++ reverse (x ∷ back q)) [] z≤n (trans (length-++ (front q)) (cong₂ _+_ (size-inv₁ q) (trans (length-reverse (x ∷ back q) ) (cong suc (size-inv₂ q))))) refl
+
+dequeueQ : Queue A → Maybe (Queue A)
+dequeueQ (Q _ _ [] [] z≤n refl refl) = nothing
+dequeueQ (Q (suc size-front₁) size-back₁ (x ∷ front₁) back₁ invariant₁ size-inv₃ size-inv₄) with size-back₁ ≤? size-front₁
+... | yes p  = just (Q size-front₁ size-back₁ front₁ back₁ p (suc-injective size-inv₃) size-inv₄)
+... | no p   = just (Q (size-front₁ + size-back₁) 0 (front₁ ++ reverse back₁) [] z≤n (trans (length-++ front₁) (cong₂ _+_ (suc-injective size-inv₃) (trans (length-reverse back₁) size-inv₄))) refl)
+
+firstQ : Queue A → Maybe A
+firstQ (Q size-front₁ size-back₁ [] back₁ invariant₁ size-inv₃ size-inv₄) = nothing
+firstQ (Q size-front₁ size-back₁ (x ∷ front₁) back₁ invariant₁ size-inv₃ size-inv₄) = just x
+
+sizeQ : Queue A → ℕ
+sizeQ q = size-front q + size-back q
+
+emptyQ : Queue A
+emptyQ = Q 0 0 [] [] z≤n refl refl
+
+open CorrectQueue
+
+goal : CorrectQueue Queue
+
+-- Data portion of goal
+goal .abstraction q = front q ++ reverse (back q)
+goal .enqueue x q = enqueueQ x q
+goal .dequeue q = dequeueQ q
+goal .first q = firstQ q
+goal .size q = sizeQ q
+goal .empty = emptyQ
+
+-- Correctness portion of goal
+goal .emptyᵣ = refl
+goal .sizeᵣ q = begin
+  sizeQ q                                      ≡⟨⟩
+  size-front q + size-back q                   ≡˘⟨ cong₂ _+_ (size-inv₁ q) (size-inv₂ q) ⟩
+  length (front q) + length (back q)           ≡˘⟨ cong (length (front q) +_) (length-reverse (back q)) ⟩
+  length (front q) + length (reverse (back q)) ≡˘⟨ length-++ (front q) ⟩
+  length (front q ++ reverse (back q))         ∎
+goal .firstᵣ (Q .0 .0 [] [] z≤n refl refl) = refl
+goal .firstᵣ (Q _ _ (x ∷ front₁) back₁ _ _ _) = refl
+goal .dequeueᵣ (Q .0 .0 [] [] z≤n refl refl) = refl
+goal .dequeueᵣ (Q (suc size-front₁) size-back₁ (x ∷ front₁) back₁ invariant₁ size-inv₃ size-inv₄)
+  with size-back₁ ≤? size-front₁
+... | yes p = refl
+... | no p = cong just (++-identityʳ (front₁ ++ reverse back₁))
+goal .enqueueᵣ q x with suc (size-back q) ≤? size-front q
+... | yes p = begin
+  front q ++ reverse (x ∷ back q)         ≡⟨ cong (front q ++_) (unfold-reverse x (back q)) ⟩
+  front q ++ reverse (back q) ++ x ∷ []   ≡˘⟨ ++-assoc (front q) (reverse (back q)) (x ∷ []) ⟩
+  (front q ++ reverse (back q)) ++ x ∷ [] ∎
+... | no p = begin
+  (front q ++ reverse (x ∷ back q)) ++ [] ≡⟨ ++-identityʳ (front q ++ reverse (x ∷ back q)) ⟩
+  front q ++ reverse (x ∷ back q)         ≡⟨ cong (front q ++_) (unfold-reverse x (back q)) ⟩
+  front q ++ reverse (back q) ++ x ∷ []   ≡˘⟨ ++-assoc (front q) (reverse (back q)) (x ∷ []) ⟩
+  (front q ++ reverse (back q)) ++ x ∷ [] ∎