Update PLFA to use Agda v2.7

.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"

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

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)

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,

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)
 ```
 
 

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

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.

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)

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/).

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

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 (_∘_)
 ```
 
 

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; β; ξ₁; ξ₂; ζ; _—→_; _—↠_; _—→⟨_⟩_; _∎;