diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index 80c8498d43..0a421f0ae7 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -76,11 +76,11 @@ jobs:
           if [[ '${{ github.ref }}' == 'refs/heads/experimental' \
              || '${{ github.base_ref }}' == 'experimental' ]]; then
             # Pick Agda version for experimental
-            echo "AGDA_COMMIT=18cc53941e924b144c0f1f3953280ef726009f7e" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=ef912c68fd329ad3046d156e3c1a70a7fec19ba1" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/experimental" >> "${GITHUB_ENV}"
           else
             # Pick Agda version for master
-            echo "AGDA_COMMIT=tags/v2.7.0.1" >> "${GITHUB_ENV}";
+            echo "AGDA_COMMIT=tags/v2.8.0-rc3" >> "${GITHUB_ENV}";
             echo "AGDA_HTML_DIR=html/master" >> "${GITHUB_ENV}"
           fi
 
diff --git a/CHANGELOG/v1.3.md b/CHANGELOG/v1.3.md
index be0113a0d5..391c2070a1 100644
--- a/CHANGELOG/v1.3.md
+++ b/CHANGELOG/v1.3.md
@@ -226,7 +226,7 @@ Deprecated modules
 
 * A warning is now raised whenever you import a deprecated module. This should
   aid the transition to the new modules. These warnings can be disabled locally
-  by adding the pragma `{-# OPTIONS --warn=noUserWarning #-}` to the top of a module.
+  by adding the pragma `{-# OPTIONS --warning=noUserWarning #-}` to the top of a module.
 
 The following modules have been renamed as part of a drive to improve
 consistency across the library. The deprecated modules still exist and
diff --git a/README.md b/README.md
index 4eba8bf8cd..81221ebbac 100644
--- a/README.md
+++ b/README.md
@@ -2,6 +2,8 @@
 
 [![Ubuntu build](https://github.com/agda/agda-stdlib/actions/workflows/ci-ubuntu.yml/badge.svg?branch=experimental)](https://github.com/agda/agda-stdlib/actions/workflows/ci-ubuntu.yml)
 
+**Note**: The library is currently tracking Agda 2.8.0 release candidate 3 in preparation for the release of Agda 2.8.0 and version 2.3 of the library. You will need to have the release candidate installed in order to type-check it.
+
 The Agda standard library
 =========================
 
diff --git a/src/Algebra/Construct/Initial.agda b/src/Algebra/Construct/Initial.agda
index ce60096210..4c9003c90b 100644
--- a/src/Algebra/Construct/Initial.agda
+++ b/src/Algebra/Construct/Initial.agda
@@ -75,10 +75,10 @@ rawMagma = record { ℤero }
 -- Structures
 
 isEquivalence : IsEquivalence _≈_
-isEquivalence = record { ℤero }
+isEquivalence = record { refl = refl; sym = sym; trans = λ {k = k} → trans {k = k} }
 
 isMagma : IsMagma _≈_ _∙_
-isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }
+isMagma = record { isEquivalence = isEquivalence ; ∙-cong = λ {y = y} {u = u} {v = v} → ∙-cong {y = y} {v = v} }
 
 isSemigroup : IsSemigroup _≈_ _∙_
 isSemigroup = record { isMagma = isMagma ; assoc = λ () }
diff --git a/src/Algebra/Operations/Semiring.agda b/src/Algebra/Operations/Semiring.agda
index 08d55c884d..b4f880afa9 100644
--- a/src/Algebra/Operations/Semiring.agda
+++ b/src/Algebra/Operations/Semiring.agda
@@ -8,7 +8,7 @@
 
 -- Disabled to prevent warnings from deprecated
 -- Algebra.Operations.CommutativeMonoid
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 open import Algebra
 import Algebra.Operations.CommutativeMonoid as MonoidOperations
diff --git a/src/Algebra/Properties/BooleanAlgebra.agda b/src/Algebra/Properties/BooleanAlgebra.agda
index 0445f20505..b45517e600 100644
--- a/src/Algebra/Properties/BooleanAlgebra.agda
+++ b/src/Algebra/Properties/BooleanAlgebra.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 -- Disabled to prevent warnings from deprecated names
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 open import Algebra.Lattice.Bundles
 
diff --git a/src/Algebra/Properties/DistributiveLattice.agda b/src/Algebra/Properties/DistributiveLattice.agda
index df03dfa38a..9e32a7e9fa 100644
--- a/src/Algebra/Properties/DistributiveLattice.agda
+++ b/src/Algebra/Properties/DistributiveLattice.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 -- Disabled to prevent warnings from deprecated names
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 open import Algebra.Lattice.Bundles
 open import Algebra.Lattice.Structures.Biased
diff --git a/src/Data/Fin/Induction.agda b/src/Data/Fin/Induction.agda
index 29203d6b38..6d0a9f9d72 100644
--- a/src/Data/Fin/Induction.agda
+++ b/src/Data/Fin/Induction.agda
@@ -5,7 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ (issue #1726)
+{-# OPTIONS --warning=noUserWarning #-} -- for deprecated _≺_ (issue #1726)
 
 module Data.Fin.Induction where
 
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 4962ed962b..6150bb93a6 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -6,7 +6,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for deprecated _≺_ and _≻toℕ_ (issue #1726)
+{-# OPTIONS --warning=noUserWarning #-} -- for deprecated _≺_ and _≻toℕ_ (issue #1726)
 
 module Data.Fin.Properties where
 
diff --git a/src/Data/List.agda b/src/Data/List.agda
index 70e8519440..45b466b99f 100644
--- a/src/Data/List.agda
+++ b/src/Data/List.agda
@@ -8,7 +8,7 @@
 -- lists.
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans
+{-# OPTIONS --warning=noUserWarning #-} -- for deprecated scans
 
 module Data.List where
 
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 21094066b6..91be7a427f 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -8,7 +8,7 @@
 -- equalities than _≡_.
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for deprecated scans
+{-# OPTIONS --warning=noUserWarning #-} -- for deprecated scans
 
 module Data.List.Properties where
 
diff --git a/src/Data/List/Solver.agda b/src/Data/List/Solver.agda
index 8b17b3ef9e..f97011c8bb 100644
--- a/src/Data/List/Solver.agda
+++ b/src/Data/List/Solver.agda
@@ -7,7 +7,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 -- Disabled to prevent warnings from deprecated monoid solver
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 module Data.List.Solver where
 
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 943e2eedf0..f7a5359a82 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -5,7 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for +-rawMonoid, *-rawMonoid (issue #1865, #1844, #1755)
+{-# OPTIONS --warning=noUserWarning #-} -- for +-rawMonoid, *-rawMonoid (issue #1865, #1844, #1755)
 
 module Data.Rational.Properties where
 
diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda
index df70346f53..d94c410341 100644
--- a/src/Data/Rational/Unnormalised/Properties.agda
+++ b/src/Data/Rational/Unnormalised/Properties.agda
@@ -5,7 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-} -- for +-rawMonoid, *-rawMonoid (issue #1865, #1844, #1755)
+{-# OPTIONS --warning=noUserWarning #-} -- for +-rawMonoid, *-rawMonoid (issue #1865, #1844, #1755)
 
 module Data.Rational.Unnormalised.Properties where
 
diff --git a/src/Function/Bijection.agda b/src/Function/Bijection.agda
index 91974b6294..c94b83b9b7 100644
--- a/src/Function/Bijection.agda
+++ b/src/Function/Bijection.agda
@@ -5,7 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 module Function.Bijection where
 
diff --git a/src/Function/Equivalence.agda b/src/Function/Equivalence.agda
index 9556023b56..ea07fd0c9a 100644
--- a/src/Function/Equivalence.agda
+++ b/src/Function/Equivalence.agda
@@ -5,7 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 module Function.Equivalence where
 
diff --git a/src/Function/HalfAdjointEquivalence.agda b/src/Function/HalfAdjointEquivalence.agda
index b78c1bc139..619eed7ae6 100644
--- a/src/Function/HalfAdjointEquivalence.agda
+++ b/src/Function/HalfAdjointEquivalence.agda
@@ -5,7 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 module Function.HalfAdjointEquivalence where
 
diff --git a/src/Function/Injection.agda b/src/Function/Injection.agda
index 72785584f1..2647b1b5d3 100644
--- a/src/Function/Injection.agda
+++ b/src/Function/Injection.agda
@@ -5,7 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 module Function.Injection where
 
diff --git a/src/Function/Inverse.agda b/src/Function/Inverse.agda
index 792382ca17..621647dbdc 100644
--- a/src/Function/Inverse.agda
+++ b/src/Function/Inverse.agda
@@ -5,7 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 module Function.Inverse where
 
diff --git a/src/Function/LeftInverse.agda b/src/Function/LeftInverse.agda
index d9ccc9a806..e8010ded50 100644
--- a/src/Function/LeftInverse.agda
+++ b/src/Function/LeftInverse.agda
@@ -5,7 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 module Function.LeftInverse where
 
diff --git a/src/Function/Related.agda b/src/Function/Related.agda
index 3bcb839237..94cca300d0 100644
--- a/src/Function/Related.agda
+++ b/src/Function/Related.agda
@@ -5,7 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 module Function.Related where
 
diff --git a/src/Function/Surjection.agda b/src/Function/Surjection.agda
index 684da0b3d7..2e741833b0 100644
--- a/src/Function/Surjection.agda
+++ b/src/Function/Surjection.agda
@@ -5,7 +5,7 @@
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
-{-# OPTIONS --warn=noUserWarning #-}
+{-# OPTIONS --warning=noUserWarning #-}
 
 module Function.Surjection where