diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 79d4a7c0b..db55232eb 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -13,17 +13,23 @@ on:
   merge_group:
 
 env:
-  DEFAULT_AGDA_VERSION: "2.6.3"
-  DEFAULT_AGDA_STDLIB_VERSION: "1.7.2"
+  DEFAULT_AGDA_VERSION: "2.7.0"
+  DEFAULT_AGDA_STDLIB_VERSION: "2.1"
   DEFAULT_GHC_VERSION: "9.4.8"
   DEFAULT_CABAL_VERSION: "3.10.1.0"
   DEFAULT_EPUBCHECK_VERSION: "4.2.6"
   NOKOGIRI_USE_SYSTEM_LIBRARIES: true
 
+# Use PowerShell by default
 defaults:
   run:
     shell: pwsh
 
+# Limit concurrent runs to one per branch
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 jobs:
   build:
     strategy:
@@ -38,25 +44,35 @@ jobs:
             os: windows-latest
 
           # Older versions of Agda
-          - name: "Build with older Agda 2.6.2.2"
-            agda-version: "2.6.2.2"
-            agda-stdlib-version: "1.7.1"
-          - name: "Build with older Agda 2.6.2.1"
-            agda-version: "2.6.2.1"
-            agda-stdlib-version: "1.7.1"
-          - name: "Build with older Agda 2.6.2"
-            agda-version: "2.6.2"
-            agda-stdlib-version: "1.7.1"
-          - name: "Build with older Agda 2.6.1.3"
-            agda-version: "2.6.1.3"
-            agda-stdlib-version: "1.6"
+          - name: "Build with older Agda 2.6.4.3"
+            agda-version: "2.6.4.3"
+            agda-stdlib-version: "2.0"
+
+          # 2024-09-05:
+          #   Version 2.0 of the standard library breaks backwards compatibility.
+          #   Therefore, versions of Agda before 2.6.4.3 are no longer supported.
+          #
+          # - name: "Build with older Agda 2.6.4.3"
+          #   agda-version: "2.6.4.3"
+          #   agda-stdlib-version: "1.7.2"
+          # - name: "Build with older Agda 2.6.2.2"
+          #   agda-version: "2.6.2.2"
+          #   agda-stdlib-version: "1.7.1"
+          # - name: "Build with older Agda 2.6.2.1"
+          #   agda-version: "2.6.2.1"
+          #   agda-stdlib-version: "1.7.1"
+          # - name: "Build with older Agda 2.6.2"
+          #   agda-version: "2.6.2"
+          #   agda-stdlib-version: "1.7.1"
+          # - name: "Build with older Agda 2.6.1.3"
+          #   agda-version: "2.6.1.3"
+          #   agda-stdlib-version: "1.6"
 
           # Newer versions of GHC
-          # - name: "Build with newer GHC 9.8.1"
-          #   ghc-version: "9.8.1"
-          #   experimental: true
-          - name: "Build with newer GHC 9.6.3"
-            ghc-version: "9.6.3"
+          - name: "Build with newer GHC 9.8.2"
+            ghc-version: "9.8.2"
+          - name: "Build with newer GHC 9.6.6"
+            ghc-version: "9.6.6"
 
           # Older versions of GHC
           - name: "Build with older GHC 9.2.8"
@@ -82,7 +98,7 @@ jobs:
           cabal-version: "${{ env.DEFAULT_CABAL_VERSION }}"
 
       - name: "Setup Agda"
-        uses: wenkokke/setup-agda@latest
+        uses: wenkokke/setup-agda@v2
         with:
           agda-version: "${{ matrix.agda-version || env.DEFAULT_AGDA_VERSION }}"
           force-no-build: "true"
diff --git a/README.md b/README.md
index cede469b5..de9e45238 100644
--- a/README.md
+++ b/README.md
@@ -59,11 +59,11 @@ or using `ghcup tui` and choosing to `set` the appropriate tools.
 
 ### Install Agda
 
-The easiest way to install Agda is using Cabal. PLFA uses Agda version 2.6.3. Run the following command:
+The easiest way to install Agda is using Cabal. PLFA uses Agda version 2.7.0. Run the following command:
 
 ```bash
 cabal update
-cabal install Agda-2.6.3
+cabal install Agda-2.7.0
 ```
 
 This step will take a long time and a lot of memory to complete.
@@ -264,22 +264,22 @@ If you plan to build PLFA locally, please refer to [Contributing][plfa-contribut
 [pre-commit-status-url]: https://results.pre-commit.ci/latest/github/plfa/plfa.github.io/dev
 [plfa-badge-version-svg]: https://img.shields.io/github/v/tag/plfa/plfa.github.io?label=release
 [plfa-badge-version-url]: https://github.com/plfa/plfa.github.io/releases/latest
-[agda-badge-version-svg]: https://img.shields.io/badge/agda-v2.6.3-blue.svg
-[agda-badge-version-url]: https://github.com/agda/agda/releases/tag/v2.6.3.
-[agda-stdlib-version-svg]: https://img.shields.io/badge/agda--stdlib-v1.7.2-blue.svg
-[agda-stdlib-version-url]: https://github.com/agda/agda-stdlib/releases/tag/v1.7.2
+[agda-badge-version-svg]: https://img.shields.io/badge/agda-v2.7.0-blue.svg
+[agda-badge-version-url]: https://github.com/agda/agda/releases/tag/v2.7.0.
+[agda-stdlib-version-svg]: https://img.shields.io/badge/agda--stdlib-v2.1-blue.svg
+[agda-stdlib-version-url]: https://github.com/agda/agda-stdlib/releases/tag/v2.1
 [plfa]: https://plfa.inf.ed.ac.uk
 [plfa-epub]: https://plfa.github.io/plfa.epub
 [plfa-contributing]: https://plfa.github.io/Contributing/
 [ghcup]: https://www.haskell.org/ghcup/
 [git]: https://git-scm.com/downloads
 [xcode]: https://developer.apple.com/xcode/
-[agda-readthedocs-installation]: https://agda.readthedocs.io/en/v2.6.3/getting-started/installation.html
-[agda-readthedocs-hello-world]: https://agda.readthedocs.io/en/v2.6.3/getting-started/hello-world.html
-[agda-readthedocs-holes]: https://agda.readthedocs.io/en/v2.6.3/getting-started/a-taste-of-agda.html#preliminaries
-[agda-readthedocs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.3/tools/emacs-mode.html
-[agda-readthedocs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.3/tools/emacs-mode.html#notation-for-key-combinations
-[agda-readthedocs-package-system]: https://agda.readthedocs.io/en/v2.6.3/tools/package-system.html#example-using-the-standard-library
+[agda-readthedocs-installation]: https://agda.readthedocs.io/en/v2.7.0/getting-started/installation.html
+[agda-readthedocs-hello-world]: https://agda.readthedocs.io/en/v2.7.0/getting-started/hello-world.html
+[agda-readthedocs-holes]: https://agda.readthedocs.io/en/v2.7.0/getting-started/a-taste-of-agda.html#preliminaries
+[agda-readthedocs-emacs-mode]: https://agda.readthedocs.io/en/v2.7.0/tools/emacs-mode.html
+[agda-readthedocs-emacs-notation]: https://agda.readthedocs.io/en/v2.7.0/tools/emacs-mode.html#notation-for-key-combinations
+[agda-readthedocs-package-system]: https://agda.readthedocs.io/en/v2.7.0/tools/package-system.html#example-using-the-standard-library
 [emacs]: https://www.gnu.org/software/emacs/download.html
 [emacs-tour]: https://www.gnu.org/software/emacs/tour/
 [emacs-home]: https://www.gnu.org/software/emacs/manual/html_node/efaq-w32/Location-of-init-file.html
diff --git a/courses/TSPL/2019/Assignment2.lagda.md b/courses/TSPL/2019/Assignment2.lagda.md
index c6fdd653f..1c6748c7a 100644
--- a/courses/TSPL/2019/Assignment2.lagda.md
+++ b/courses/TSPL/2019/Assignment2.lagda.md
@@ -53,12 +53,7 @@ open import Data.Unit using (⊤; tt)
 open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness)
-open import Relation.Nullary.Negation using (¬?)
-open import Relation.Nullary.Product using (_×-dec_)
-open import Relation.Nullary.Sum using (_⊎-dec_)
-open import Relation.Nullary.Negation using (contraposition)
+open import Relation.Nullary using (¬_; Dec; yes; no; ⌊_⌋; toWitness; fromWitness; ¬?; _×-dec_; _⊎-dec_; contraposition)
 open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
 open import plfa.part1.Relations using (_<_; z<s; s<s)
 open import plfa.part1.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_; extensionality)
diff --git a/src/plfa/part1/Connectives.lagda.md b/src/plfa/part1/Connectives.lagda.md
index f0632aa9d..a36c6d2b0 100644
--- a/src/plfa/part1/Connectives.lagda.md
+++ b/src/plfa/part1/Connectives.lagda.md
@@ -30,8 +30,8 @@ principle known as _Propositions as Types_:
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
 open Eq.≡-Reasoning
-open import Data.Nat using (ℕ)
-open import Function using (_∘_)
+open import Data.Nat.Base using (ℕ)
+open import Function.Base using (_∘_)
 open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality; _⇔_)
 open plfa.part1.Isomorphism.≃-Reasoning
 ```
@@ -787,7 +787,7 @@ import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
 import Data.Unit using (⊤; tt)
 import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to case-⊎)
 import Data.Empty using (⊥; ⊥-elim)
-import Function.Equivalence using (_⇔_)
+import Function.Bundles using (_⇔_)
 ```
 The standard library constructs pairs with `_,_` whereas we use `⟨_,_⟩`.
 The former makes it convenient to build triples or larger tuples from pairs,
diff --git a/src/plfa/part1/Decidable.lagda.md b/src/plfa/part1/Decidable.lagda.md
index 7d5496765..601d0f456 100644
--- a/src/plfa/part1/Decidable.lagda.md
+++ b/src/plfa/part1/Decidable.lagda.md
@@ -22,14 +22,13 @@ of a new notion of _decidable_.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
 open Eq.≡-Reasoning
-open import Data.Nat using (ℕ; zero; suc)
-open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Relation.Nullary using (¬_)
-open import Relation.Nullary.Negation using ()
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Product.Base using (_×_) renaming (_,_ to ⟨_,_⟩)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Relation.Nullary.Negation as Neg using (¬_)
   renaming (contradiction to ¬¬-intro)
 open import Data.Unit using (⊤; tt)
-open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Empty using (⊥)
 open import plfa.part1.Relations using (_<_; z<s; s<s)
 open import plfa.part1.Isomorphism using (_⇔_)
 ```
@@ -510,7 +509,7 @@ we can decide if the first implies the second:
 ```agda
 _→-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A → B)
 _     →-dec yes y  =  yes (λ _ → y)
-no ¬x →-dec _      =  yes (λ x → ⊥-elim (¬x x))
+no ¬x →-dec _      =  yes (λ x → Neg.contradiction x ¬x)
 yes x →-dec no ¬y  =  no (λ f → ¬y (f x))
 ```
 The implication holds if either the second holds or
@@ -658,11 +657,9 @@ Show that both of the above are decidable.
 import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
 import Data.Nat using (_≤?_)
 import Relation.Nullary using (Dec; yes; no)
-import Relation.Nullary.Decidable using (⌊_⌋; True; toWitness; fromWitness)
-import Relation.Nullary.Negation using (¬?)
-import Relation.Nullary.Product using (_×-dec_)
-import Relation.Nullary.Sum using (_⊎-dec_)
-import Relation.Binary using (Decidable)
+import Relation.Nullary.Decidable using
+  (⌊_⌋; True; toWitness; fromWitness; _×-dec_; _⊎-dec_; ¬?)
+import Relation.Binary.Definitions using (Decidable)
 ```
 
 
diff --git a/src/plfa/part1/Induction.lagda.md b/src/plfa/part1/Induction.lagda.md
index 39fdfa42d..41ae017ae 100644
--- a/src/plfa/part1/Induction.lagda.md
+++ b/src/plfa/part1/Induction.lagda.md
@@ -21,14 +21,14 @@ _induction_.
 
 We require equality as in the previous chapter, plus the naturals
 and some operations upon them.  We also require a couple of new operations,
-`cong`, `sym`, and `_≡⟨_⟩_`, which are explained below:
+`cong`, `sym`, `_≡⟨⟩_` and `_≡⟨_⟩_`, which are explained below:
 ```agda
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; cong; sym)
-open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
+open Eq.≡-Reasoning using (begin_; step-≡-∣; step-≡-⟩; _∎)
 open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_;_^_)
 ```
-(Importing `step-≡` defines `_≡⟨_⟩_`.)
+(Importing `step--∣` defines `_≡⟨⟩_` and importing `step-≡-⟩` defines `_≡⟨_⟩_`.)
 
 
 ## Properties of operators
diff --git a/src/plfa/part1/Isomorphism.lagda.md b/src/plfa/part1/Isomorphism.lagda.md
index 4db122e07..49f95f7b5 100644
--- a/src/plfa/part1/Isomorphism.lagda.md
+++ b/src/plfa/part1/Isomorphism.lagda.md
@@ -20,7 +20,7 @@ distributivity.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; cong; cong-app)
 open Eq.≡-Reasoning
-open import Data.Nat using (ℕ; zero; suc; _+_)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Nat.Properties using (+-comm)
 ```
 
@@ -489,11 +489,10 @@ Why do `to` and `from` not form an isomorphism?
 
 Definitions similar to those in this chapter can be found in the standard library:
 ```agda
-import Function using (_∘_)
-import Function.Inverse using (_↔_)
-import Function.LeftInverse using (_↞_)
+import Function.Base using (_∘_)
+import Function.Bundles using (_↔_; _↩_)
 ```
-The standard library `_↔_` and `_↞_` correspond to our `_≃_` and
+The standard library `_↔_` and `_↩_` correspond to our `_≃_` and
 `_≲_`, respectively, but those in the standard library are less
 convenient, since they depend on a nested record structure and are
 parameterised with regard to an arbitrary notion of equivalence.
diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md
index 05c7feefe..dc7dacca3 100644
--- a/src/plfa/part1/Lists.lagda.md
+++ b/src/plfa/part1/Lists.lagda.md
@@ -17,13 +17,13 @@ examples of polymorphic types and higher-order functions.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)
 open Eq.≡-Reasoning
-open import Data.Bool using (Bool; true; false; T; _∧_; _∨_; not)
-open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
+open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
 open import Data.Nat.Properties using
   (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ; *-distribʳ-+)
 open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
-open import Function using (_∘_)
+open import Data.Product.Base using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
+open import Function.Base using (_∘_)
 open import Level using (Level)
 open import plfa.part1.Isomorphism using (_≃_; _⇔_)
 ```
@@ -58,14 +58,18 @@ and `1 ∷ (2 ∷ [])` is a list of the remaining elements, called the
 _tail_. A list is a strange beast: it has a head and a tail,
 nothing in between, and the tail is itself another list!
 
-As we've seen, parameterised types can be translated to
-indexed types. The definition above is equivalent to the following:
+As we've seen, some parameterised types can be translated to
+indexed types. The definition above translates to the following:
 ```agda
-data List′ : Set → Set where
+data List′ : Set → Set₁ where
   []′  : ∀ {A : Set} → List′ A
   _∷′_ : ∀ {A : Set} → A → List′ A → List′ A
 ```
-Each constructor takes the parameter as an implicit argument.
+This is almost equivalent, save that with parametrised types the result
+can be in `Set`, whereas for technical reasons indexed types require the
+result to be `Set₁`.
+
+Each constructor of `List` takes the parameter as an implicit argument.
 Thus, our example list could also be written:
 ```agda
 _ : List ℕ
@@ -1119,8 +1123,7 @@ import Data.List.Relation.Unary.All using (All; []; _∷_)
 import Data.List.Relation.Unary.Any using (Any; here; there)
 import Data.List.Membership.Propositional using (_∈_)
 import Data.List.Properties
-  using (reverse-++-commute; map-compose; map-++-commute; foldr-++)
-  renaming (mapIsFold to map-is-foldr)
+  using (reverse-++-commute; map-compose; map-++-commute; foldr-++; map-is-foldr)
 import Algebra.Structures using (IsMonoid)
 import Relation.Unary using (Decidable)
 import Relation.Binary using (Decidable)
diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md
index 102477a0c..292a89b7d 100644
--- a/src/plfa/part1/Naturals.lagda.md
+++ b/src/plfa/part1/Naturals.lagda.md
@@ -262,7 +262,7 @@ about it from the Agda standard library:
 ```agda
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
-open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)
+open Eq.≡-Reasoning using (begin_; step-≡-∣; _∎)
 ```
 
 The first line brings the standard library module that defines
@@ -273,7 +273,9 @@ are `_≡_`, the equality operator, and `refl`, the name for evidence
 that two terms are equal.  The third line takes a module that
 specifies operators to support reasoning about equivalence, and adds
 all the names specified in the `using` clause into the current scope.
-In this case, the names added are `begin_`, `_≡⟨⟩_`, and `_∎`.  We
+In this case, the names added are `begin_`, `step-≡-|`, and `_∎`.
+Furthermore this also brings in to scope `_≡⟨⟩_` which is a mixfix
+synonym for `step-≡-∣`. We
 will see how these are used below.  We take these as givens for now,
 but will see how they are defined in
 Chapter [Equality](/Equality/).
diff --git a/src/plfa/part1/Negation.lagda.md b/src/plfa/part1/Negation.lagda.md
index a7a25919b..211207c12 100644
--- a/src/plfa/part1/Negation.lagda.md
+++ b/src/plfa/part1/Negation.lagda.md
@@ -14,10 +14,11 @@ and classical logic.
 
 ```agda
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-open import Data.Nat using (ℕ; zero; suc)
-open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Data.Product using (_×_)
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Empty using (⊥)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Data.Product.Base using (_×_)
+open import Relation.Nullary.Negation using (contradiction)
 open import plfa.part1.Isomorphism using (_≃_; extensionality)
 ```
 
@@ -174,7 +175,7 @@ is no `x` in their domain, so the equality holds trivially.
 Indeed, we can show any two proofs of a negation are equal:
 ```agda
 assimilation : ∀ {A : Set} (¬x ¬x′ : ¬ A) → ¬x ≡ ¬x′
-assimilation ¬x ¬x′ = extensionality (λ x → ⊥-elim (¬x x))
+assimilation ¬x ¬x′ = extensionality (λ x → contradiction x ¬x)
 ```
 Evidence for `¬ A` implies that any evidence of `A`
 immediately leads to a contradiction.  But extensionality
@@ -401,7 +402,7 @@ of two stable formulas is stable.
 Definitions similar to those in this chapter can be found in the standard library:
 ```agda
 import Relation.Nullary using (¬_)
-import Relation.Nullary.Negation using (contraposition)
+import Relation.Nullary.Negation using (contradiction; contraposition)
 ```
 
 ## Unicode
diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md
index e1d908f5a..0ab3372c2 100644
--- a/src/plfa/part1/Quantifiers.lagda.md
+++ b/src/plfa/part1/Quantifiers.lagda.md
@@ -14,12 +14,12 @@ This chapter introduces universal and existential quantification.
 ```agda
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
-open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
-open import Relation.Nullary using (¬_)
-open import Data.Product using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_)
+open import Relation.Nullary.Negation using (¬_)
+open import Data.Product.Base using (_×_; proj₁; proj₂) renaming (_,_ to ⟨_,_⟩)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import plfa.part1.Isomorphism using (_≃_; extensionality; ∀-extensionality)
-open import Function using (_∘_)
+open import Function.Base using (_∘_)
 ```
 
 
diff --git a/src/plfa/part2/BigStep.lagda.md b/src/plfa/part2/BigStep.lagda.md
index 06d8cf913..99e3b4c9f 100644
--- a/src/plfa/part2/BigStep.lagda.md
+++ b/src/plfa/part2/BigStep.lagda.md
@@ -33,9 +33,9 @@ single sub-computation has been completed.
 ```agda
 open import Relation.Binary.PropositionalEquality
   using (_≡_; refl; trans; sym; cong-app)
-open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
+open import Data.Product.Base using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
   renaming (_,_ to ⟨_,_⟩)
-open import Function using (_∘_)
+open import Function.Base using (_∘_)
 open import plfa.part2.Untyped
   using (Context; _⊢_; _∋_; ★; ∅; _,_; Z; S_; `_; #_; ƛ_; _·_;
   subst; subst-zero; exts; rename; β; ξ₁; ξ₂; ζ; _—→_; _—↠_; _—→⟨_⟩_; _∎;
diff --git a/src/plfa/part2/Confluence.lagda.md b/src/plfa/part2/Confluence.lagda.md
index c9f482b40..3ba35f111 100644
--- a/src/plfa/part2/Confluence.lagda.md
+++ b/src/plfa/part2/Confluence.lagda.md
@@ -59,8 +59,8 @@ confluence for parallel reduction.
 
 ```agda
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-open import Function using (_∘_)
-open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
+open import Function.Base using (_∘_)
+open import Data.Product.Base using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
   renaming (_,_ to ⟨_,_⟩)
 open import plfa.part2.Substitution using (Rename; Subst)
 open import plfa.part2.Untyped
diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md
index 0c0d0705f..1fdf1b4a9 100644
--- a/src/plfa/part2/DeBruijn.lagda.md
+++ b/src/plfa/part2/DeBruijn.lagda.md
@@ -42,9 +42,8 @@ James Chapman, James McKinna, and many others.
 ```agda
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
-open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Decidable using (True; toWitness)
 ```
 
diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md
index 0133dcb7f..0dbcbb037 100644
--- a/src/plfa/part2/Inference.lagda.md
+++ b/src/plfa/part2/Inference.lagda.md
@@ -247,12 +247,12 @@ We are now ready to begin the formal development.
 ```agda
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
-open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
+open import Data.Empty using (⊥)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_; _*_)
 open import Data.String using (String; _≟_)
-open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Relation.Nullary.Decidable using (False; toWitnessFalse)
+open import Data.Product.Base using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
+open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Relation.Nullary.Decidable using ( Dec; yes; no; False; toWitnessFalse)
 ```
 
 Once we have a type derivation, it will be easy to construct
@@ -540,8 +540,8 @@ one showing `Γ ∋ x ⦂ A` and one showing `Γ ∋ x ⦂ B`, it follows that
 ```agda
 uniq-∋ : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
 uniq-∋ Z Z                 =  refl
-uniq-∋ Z (S x≢y _)         =  ⊥-elim (x≢y refl)
-uniq-∋ (S x≢y _) Z         =  ⊥-elim (x≢y refl)
+uniq-∋ Z (S x≢y _)         =  contradiction refl x≢y
+uniq-∋ (S x≢y _) Z         =  contradiction refl x≢y
 uniq-∋ (S _ ∋x) (S _ ∋x′)  =  uniq-∋ ∋x ∋x′
 ```
 If both derivations are by rule `Z` then uniqueness
diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md
index 275ef3ca1..193a7fe36 100644
--- a/src/plfa/part2/Lambda.lagda.md
+++ b/src/plfa/part2/Lambda.lagda.md
@@ -50,16 +50,14 @@ four.
 ## Imports
 
 ```agda
-open import Data.Bool using (Bool; true; false; T; not)
-open import Data.Empty using (⊥; ⊥-elim)
-open import Data.List using (List; _∷_; [])
-open import Data.Nat using (ℕ; zero; suc)
-open import Data.Product using (∃-syntax; _×_)
+open import Data.Bool.Base using (Bool; true; false; T; not)
+open import Data.List.Base using (List; _∷_; [])
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Product.Base using (∃-syntax; _×_)
 open import Data.String using (String; _≟_)
-open import Data.Unit using (tt)
-open import Relation.Nullary using (Dec; yes; no; ¬_)
-open import Relation.Nullary.Decidable using (False; toWitnessFalse)
-open import Relation.Nullary.Negation using (¬?)
+open import Data.Unit.Base using (tt)
+open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Relation.Nullary.Decidable using (Dec; yes; no; False; toWitnessFalse; ¬?)
 open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
 ```
 
@@ -1345,8 +1343,8 @@ there is at most one `A` such that the judgment holds:
 ```agda
 ∋-functional : ∀ {Γ x A B} → Γ ∋ x ⦂ A → Γ ∋ x ⦂ B → A ≡ B
 ∋-functional Z        Z          =  refl
-∋-functional Z        (S x≢ _)   =  ⊥-elim (x≢ refl)
-∋-functional (S x≢ _) Z          =  ⊥-elim (x≢ refl)
+∋-functional Z        (S x≢ _)   =  contradiction refl x≢
+∋-functional (S x≢ _) Z          =  contradiction refl x≢
 ∋-functional (S _ ∋x) (S _ ∋x′)  =  ∋-functional ∋x ∋x′
 ```
 
@@ -1372,10 +1370,10 @@ doing so requires types `A` and `B` such that `A ⇒ B ≡ A`:
 
 ```agda
 nope₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ ` "x" · ` "x" ⦂ A)
-nope₂ (⊢ƛ (⊢` ∋x · ⊢` ∋x′))  =  contradiction (∋-functional ∋x ∋x′)
+nope₂ (⊢ƛ (⊢` ∋x · ⊢` ∋x′))  = impossible (∋-functional ∋x ∋x′)
   where
-  contradiction : ∀ {A B} → ¬ (A ⇒ B ≡ A)
-  contradiction ()
+  impossible : ∀ {A B} → ¬ (A ⇒ B ≡ A)
+  impossible ()
 ```
 
 
diff --git a/src/plfa/part2/More.lagda.md b/src/plfa/part2/More.lagda.md
index 913fe895b..a1cc84c3e 100644
--- a/src/plfa/part2/More.lagda.md
+++ b/src/plfa/part2/More.lagda.md
@@ -299,7 +299,7 @@ We can also translate back the other way:
       `inj₂ W                             inject second component
 
 ### Typing
-
+⊥
     Γ ⊢ M ⦂ A
     -------------------- `inj₁ or ⊎-I₁
     Γ ⊢ `inj₁ M ⦂ A `⊎ B
@@ -554,9 +554,8 @@ and leave formalisation of the remaining constructs as an exercise.
 ```agda
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
-open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat using (ℕ; zero; suc; _*_; _<_; _≤?_; z≤n; s≤s)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Decidable using (True; toWitness)
 ```
 
diff --git a/src/plfa/part2/Properties.lagda.md b/src/plfa/part2/Properties.lagda.md
index f1564faf4..8619cc05f 100644
--- a/src/plfa/part2/Properties.lagda.md
+++ b/src/plfa/part2/Properties.lagda.md
@@ -20,14 +20,14 @@ sequences for us.
 open import Relation.Binary.PropositionalEquality
   using (_≡_; _≢_; refl; sym; cong; cong₂)
 open import Data.String using (String; _≟_)
-open import Data.Nat using (ℕ; zero; suc)
-open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Product
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Product.Base
   using (_×_; proj₁; proj₂; ∃; ∃-syntax)
   renaming (_,_ to ⟨_,_⟩)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Function using (_∘_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Relation.Nullary.Decidable using (Dec; yes; no)
+open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Function.Base using (_∘_)
 open import plfa.part1.Isomorphism
 open import plfa.part2.Lambda
 ```
@@ -489,7 +489,7 @@ drop {Γ} {x} {M} {A} {B} {C} ⊢M = rename ρ ⊢M
       -------------------------
     → Γ , x ⦂ B ∋ z ⦂ C
   ρ Z                 =  Z
-  ρ (S x≢x Z)         =  ⊥-elim (x≢x refl)
+  ρ (S x≢x Z)         =  contradiction refl x≢x
   ρ (S z≢x (S _ ∋z))  =  S z≢x ∋z
 ```
 Here map `ρ` can never be invoked on the inner occurrence of `x` since
@@ -550,9 +550,9 @@ subst : ∀ {Γ x N V A B}
   → Γ ⊢ N [ x := V ] ⦂ B
 subst {x = y} ⊢V (⊢` {x = x} Z) with x ≟ y
 ... | yes _         =  weaken ⊢V
-... | no  x≢y       =  ⊥-elim (x≢y refl)
+... | no  x≢y       =  contradiction refl x≢y
 subst {x = y} ⊢V (⊢` {x = x} (S x≢y ∋x)) with x ≟ y
-... | yes refl      =  ⊥-elim (x≢y refl)
+... | yes refl      =  contradiction refl x≢y
 ... | no  _         =  ⊢` ∋x
 subst {x = y} ⊢V (⊢ƛ {x = x} ⊢N) with x ≟ y
 ... | yes refl      =  ⊢ƛ (drop ⊢N)
@@ -1349,22 +1349,22 @@ det : ∀ {M M′ M″}
     --------
   → M′ ≡ M″
 det (ξ-·₁ L—→L′)   (ξ-·₁ L—→L″)     =  cong₂ _·_ (det L—→L′ L—→L″) refl
-det (ξ-·₁ L—→L′)   (ξ-·₂ VL M—→M″)  =  ⊥-elim (V¬—→ VL L—→L′)
-det (ξ-·₁ L—→L′)   (β-ƛ _)          =  ⊥-elim (V¬—→ V-ƛ L—→L′)
-det (ξ-·₂ VL _)    (ξ-·₁ L—→L″)     =  ⊥-elim (V¬—→ VL L—→L″)
+det (ξ-·₁ L—→L′)   (ξ-·₂ VL M—→M″)  =  contradiction L—→L′ (V¬—→ VL)
+det (ξ-·₁ L—→L′)   (β-ƛ _)          =  contradiction L—→L′ (V¬—→ V-ƛ)
+det (ξ-·₂ VL _)    (ξ-·₁ L—→L″)     =  contradiction L—→L″ (V¬—→ VL)
 det (ξ-·₂ _ M—→M′) (ξ-·₂ _ M—→M″)   =  cong₂ _·_ refl (det M—→M′ M—→M″)
-det (ξ-·₂ _ M—→M′) (β-ƛ VM)         =  ⊥-elim (V¬—→ VM M—→M′)
-det (β-ƛ _)        (ξ-·₁ L—→L″)     =  ⊥-elim (V¬—→ V-ƛ L—→L″)
-det (β-ƛ VM)       (ξ-·₂ _ M—→M″)   =  ⊥-elim (V¬—→ VM M—→M″)
+det (ξ-·₂ _ M—→M′) (β-ƛ VM)         =  contradiction M—→M′ (V¬—→ VM)
+det (β-ƛ _)        (ξ-·₁ L—→L″)     =  contradiction L—→L″ (V¬—→ V-ƛ)
+det (β-ƛ VM)       (ξ-·₂ _ M—→M″)   =  contradiction M—→M″ (V¬—→ VM)
 det (β-ƛ _)        (β-ƛ _)          =  refl
 det (ξ-suc M—→M′)  (ξ-suc M—→M″)    =  cong `suc_ (det M—→M′ M—→M″)
 det (ξ-case L—→L′) (ξ-case L—→L″)   =  cong₄ case_[zero⇒_|suc_⇒_]
                                          (det L—→L′ L—→L″) refl refl refl
-det (ξ-case L—→L′) β-zero           =  ⊥-elim (V¬—→ V-zero L—→L′)
-det (ξ-case L—→L′) (β-suc VL)       =  ⊥-elim (V¬—→ (V-suc VL) L—→L′)
-det β-zero         (ξ-case M—→M″)   =  ⊥-elim (V¬—→ V-zero M—→M″)
+det (ξ-case L—→L′) β-zero           =  contradiction L—→L′ (V¬—→ V-zero)
+det (ξ-case L—→L′) (β-suc VL)       =  contradiction L—→L′ (V¬—→ (V-suc VL))
+det β-zero         (ξ-case M—→M″)   =  contradiction M—→M″ (V¬—→ V-zero)
 det β-zero         β-zero           =  refl
-det (β-suc VL)     (ξ-case L—→L″)   =  ⊥-elim (V¬—→ (V-suc VL) L—→L″)
+det (β-suc VL)     (ξ-case L—→L″)   =  contradiction L—→L″ (V¬—→ (V-suc VL))
 det (β-suc _)      (β-suc _)        =  refl
 det β-μ            β-μ              =  refl
 ```
diff --git a/src/plfa/part2/Substitution.lagda.md b/src/plfa/part2/Substitution.lagda.md
index cb1c2a805..eb899742e 100644
--- a/src/plfa/part2/Substitution.lagda.md
+++ b/src/plfa/part2/Substitution.lagda.md
@@ -45,8 +45,8 @@ system that _decides_ whether any two substitutions are equal.
 ```agda
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; cong; cong₂; cong-app)
-open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
-open import Function using (_∘_)
+open Eq.≡-Reasoning using (begin_; step-≡-∣; step-≡-⟩; _∎)
+open import Function.Base using (_∘_)
 open import plfa.part2.Untyped
      using (Type; Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_;
             rename; subst; ext; exts; _[_]; subst-zero)
diff --git a/src/plfa/part2/Untyped.lagda.md b/src/plfa/part2/Untyped.lagda.md
index 6b9142285..d4cdb86c4 100644
--- a/src/plfa/part2/Untyped.lagda.md
+++ b/src/plfa/part2/Untyped.lagda.md
@@ -48,9 +48,8 @@ the range of different lambda calculi one may encounter.
 ```agda
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl)
-open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
-open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (¬_)
 open import Relation.Nullary.Decidable using (True; toWitness)
 ```
 
diff --git a/src/plfa/part3/Adequacy.lagda.md b/src/plfa/part3/Adequacy.lagda.md
index 26602e06c..ec319fdf1 100644
--- a/src/plfa/part3/Adequacy.lagda.md
+++ b/src/plfa/part3/Adequacy.lagda.md
@@ -65,17 +65,15 @@ The rest of this chapter is organized as follows.
 ## Imports
 
 ```agda
-import Relation.Binary.PropositionalEquality as Eq
-open Eq using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app)
-open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Data.Product.Base using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
   renaming (_,_ to ⟨_,_⟩)
-open import Data.Sum
-open import Relation.Nullary using (¬_)
-open import Relation.Nullary.Negation using (contradiction)
-open import Data.Empty using (⊥-elim) renaming (⊥ to Bot)
-open import Data.Unit
-open import Relation.Nullary using (Dec; yes; no)
-open import Function using (_∘_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Data.Empty using () renaming (⊥ to Bot)
+open import Data.Unit.Base using (tt; ⊤)
+open import Relation.Nullary.Decidable using (Dec; yes; no)
+open import Function.Base using (_∘_)
 open import plfa.part2.Untyped
      using (Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_;
             rename; subst; ext; exts; _[_]; subst-zero;
@@ -488,7 +486,7 @@ kth-x{γ' = γ'}{x = x} with γ' x
     where E : {c : Clos} → 𝔼 v c → above-fun w
             → Σ[ c' ∈ Clos ] (γ' ,' c) ⊢ N ⇓ c'  ×  𝕍 w c'
           E {c} 𝔼vc fw = ↓→𝔼 (λ {x} → 𝔾-ext{Γ}{γ}{γ'} 𝔾γγ' 𝔼vc {x}) d fw
-↓→𝔼 𝔾γγ' ⊥-intro f⊥ = ⊥-elim (above-fun⊥ f⊥)
+↓→𝔼 𝔾γγ' ⊥-intro f⊥ = contradiction f⊥ above-fun⊥
 ↓→𝔼 𝔾γγ' (⊔-intro{v = v₁}{w = v₂} d₁ d₂) fv12
     with above-fun? v₁ | above-fun? v₂
 ... | yes fv1 | yes fv2
diff --git a/src/plfa/part3/Compositional.lagda.md b/src/plfa/part3/Compositional.lagda.md
index f9eefc304..3a6231a6c 100644
--- a/src/plfa/part3/Compositional.lagda.md
+++ b/src/plfa/part3/Compositional.lagda.md
@@ -24,10 +24,10 @@ with such a definition and prove that it is equivalent to ℰ.
 ## Imports
 
 ```agda
-open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
+open import Data.Product.Base using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
   renaming (_,_ to ⟨_,_⟩)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Data.Unit using (⊤; tt)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Data.Unit.Base using (⊤; tt)
 open import plfa.part2.Untyped
   using (Context; _,_; ★; _∋_; _⊢_; `_; ƛ_; _·_)
 open import plfa.part3.Denotational
diff --git a/src/plfa/part3/Denotational.lagda.md b/src/plfa/part3/Denotational.lagda.md
index f483b634f..a73c5288a 100644
--- a/src/plfa/part3/Denotational.lagda.md
+++ b/src/plfa/part3/Denotational.lagda.md
@@ -52,17 +52,15 @@ down a denotational semantics of the lambda calculus.
 ## Imports
 
 ```agda
-open import Agda.Primitive using (lzero; lsuc)
-open import Data.Nat using (ℕ; zero; suc)
-open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
+open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Product.Base using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
   renaming (_,_ to ⟨_,_⟩)
-open import Data.Sum
-open import Data.Vec using (Vec; []; _∷_)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Data.Vec.Base using (Vec; []; _∷_)
 open import Relation.Binary.PropositionalEquality
-  using (_≡_; _≢_; refl; sym; cong; cong₂; cong-app)
-open import Relation.Nullary using (¬_)
-open import Relation.Nullary.Negation using (contradiction)
-open import Function using (_∘_)
+  using (_≡_; refl)
+open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Function.Base using (_∘_)
 open import plfa.part2.Untyped
   using (Context; ★; _∋_; ∅; _,_; Z; S_; _⊢_; `_; _·_; ƛ_;
          #_; twoᶜ; ext; rename; exts; subst; subst-zero; _[_])
diff --git a/src/plfa/part3/Soundness.lagda.md b/src/plfa/part3/Soundness.lagda.md
index 786d9f5e3..1c883f493 100644
--- a/src/plfa/part3/Soundness.lagda.md
+++ b/src/plfa/part3/Soundness.lagda.md
@@ -31,15 +31,12 @@ expansion is false for most typed lambda calculi!
 
 ```agda
 open import Relation.Binary.PropositionalEquality
-  using (_≡_; _≢_; refl; sym; cong; cong₂; cong-app)
-open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
+  using (_≡_; _≢_; refl; sym)
+open import Data.Product.Base using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
   renaming (_,_ to ⟨_,_⟩)
-open import Agda.Primitive using (lzero)
-open import Relation.Nullary using (¬_)
-open import Relation.Nullary.Negation using (contradiction)
-open import Data.Empty using (⊥-elim)
-open import Relation.Nullary using (Dec; yes; no)
-open import Function using (_∘_)
+open import Relation.Nullary.Negation using (¬_; contradiction)
+open import Relation.Nullary.Decidable using (Dec; yes; no)
+open import Function.Base using (_∘_)
 open import plfa.part2.Untyped
      using (Context; _,_; _∋_; _⊢_; ★; Z; S_; `_; ƛ_; _·_;
             subst; _[_]; subst-zero; ext; rename; exts;
@@ -363,7 +360,7 @@ diff-const-env : ∀{Γ} {x y : Γ ∋ ★} {v}
     -------------------
   → const-env x v y ≡ ⊥
 diff-const-env {Γ} {x} {y} neq with x var≟ y
-...  | yes eq  =  ⊥-elim (neq eq)
+...  | yes eq  =  contradiction eq neq
 ...  | no _    =  refl
 ```
 
diff --git a/standard-library b/standard-library
index b2e6385c1..97bc55e47 160000
--- a/standard-library
+++ b/standard-library
@@ -1 +1 @@
-Subproject commit b2e6385c1636897dbee0b10f7194376ff2c1753b
+Subproject commit 97bc55e47367c562b3032bf104f2a00b19716f88
diff --git a/web/posts/2024-09-05-migration-to-agda-2-7-0.md b/web/posts/2024-09-05-migration-to-agda-2-7-0.md
new file mode 100644
index 000000000..1abb1c548
--- /dev/null
+++ b/web/posts/2024-09-05-migration-to-agda-2-7-0.md
@@ -0,0 +1,24 @@
+---
+title: "Migration to Agda 2.7.0"
+---
+
+We upgraded to [Agda 2.7.0][agda-2.7.0] and [version 2.1 of the standard library][agda-stdlib-v2.1].
+If you want to continue working with the book, you'll have to update your versions locally.
+Please follow the instructions in [Getting Started](/GettingStarted/) to reinstall Agda and the standard library.
+
+In the past, we maintained compatibility with versions of Agda all the way back to [Agda 2.6.1.3][agda-2.6.1.3] and [version 1.6 of the standard library][agda-stdlib-v1.6].
+However, [version 2.0 of the standard library][agda-stdlib-v2.0] broke backwards compatibility with earlier versions of the standard library.
+Consequently, starting with today's version of PLFA, the oldest supported versions of Agda and its standard library are [Agda 2.6.4.3][agda-2.6.4.3] and [version 2.0 of the standard library][agda-stdlib-v2.0].
+
+[agda-stdlib-v1.6]: https://github.com/agda/agda-stdlib/releases/tag/v1.6
+  "Agda standard library version 1.6 on GitHub"
+[agda-stdlib-v2.0]: https://github.com/agda/agda-stdlib/releases/tag/v2.0
+  "Agda standard library version 2.0 on GitHub"
+[agda-stdlib-v2.1]: https://github.com/agda/agda-stdlib/releases/tag/v2.1
+  "Agda standard library version 2.1 on GitHub"
+[agda-2.6.1.3]: https://github.com/agda/agda/releases/tag/v2.6.1.3
+  "Agda version 2.6.1.3 on GitHub"
+[agda-2.6.4.3]: https://github.com/agda/agda/releases/tag/v2.6.4.3
+  "Agda version 2.6.4.3 on GitHub"
+[agda-2.7.0]: https://github.com/agda/agda/releases/tag/v2.7.0
+  "Agda version 2.7.0 on GitHub"