From db4163611ec4b29a6dd20a4729223a3044e1d047 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Fri, 21 Jul 2023 13:04:52 -0300
Subject: [PATCH 1/6] Put indexed data types in the right universe

To fix agda/agda#6654, we've decided that large indices will no longer
be allowed by default. There is an infective flag `--large-indices` to
bring them back, but none of the uses of large indices in the standard
library were essential: to avoid complicated mutually-recursive PRs
across repos, I adjusted the levels to check with `--no-large-indices`
instead of adding the flag to the modules that used them.
---
 src/Data/Star/Decoration.agda | 2 +-
 src/Data/Star/Pointer.agda    | 2 +-
 src/Reflection/Annotated.agda | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Data/Star/Decoration.agda b/src/Data/Star/Decoration.agda
index 24428a5843..170b5abb07 100644
--- a/src/Data/Star/Decoration.agda
+++ b/src/Data/Star/Decoration.agda
@@ -28,7 +28,7 @@ data NonEmptyEdgePred {ℓ r p : Level} {I : Set ℓ} (T : Rel I r)
 -- Decorating an edge with more information.
 
 data DecoratedWith {ℓ r p : Level} {I : Set ℓ} {T : Rel I r} (P : EdgePred p T)
-       : Rel (NonEmpty (Star T)) p where
+       : Rel (NonEmpty (Star T)) (ℓ ⊔ r ⊔ p) where
   ↦ : ∀ {i j k} {x : T i j} {xs : Star T j k}
       (p : P x) → DecoratedWith P (nonEmpty (x ◅ xs)) (nonEmpty xs)
 
diff --git a/src/Data/Star/Pointer.agda b/src/Data/Star/Pointer.agda
index 6214e3e7dc..70dfdb94be 100644
--- a/src/Data/Star/Pointer.agda
+++ b/src/Data/Star/Pointer.agda
@@ -21,7 +21,7 @@ open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 
 data Pointer {r p q} {T : Rel I r}
              (P : EdgePred p T) (Q : EdgePred q T)
-             : Rel (Maybe (NonEmpty (Star T))) (p ⊔ q) where
+             : Rel (Maybe (NonEmpty (Star T))) (ℓ ⊔ r ⊔ p ⊔ q) where
   step : ∀ {i j k} {x : T i j} {xs : Star T j k}
          (p : P x) → Pointer P Q (just (nonEmpty (x ◅ xs)))
                                  (just (nonEmpty xs))
diff --git a/src/Reflection/Annotated.agda b/src/Reflection/Annotated.agda
index ba63faf0fb..171dfe75c4 100644
--- a/src/Reflection/Annotated.agda
+++ b/src/Reflection/Annotated.agda
@@ -35,8 +35,8 @@ Annotation : ∀ ℓ → Set (suc ℓ)
 Annotation ℓ = ∀ {u} → ⟦ u ⟧ → Set ℓ
 
 -- An annotated type is a family over an Annotation and a reflected term.
-Typeₐ : ∀ ℓ → Univ → Set (suc ℓ)
-Typeₐ ℓ u = Annotation ℓ → ⟦ u ⟧ → Set ℓ
+Typeₐ : ∀ ℓ → Univ → Set (suc (suc ℓ))
+Typeₐ ℓ u = Annotation ℓ → ⟦ u ⟧ → Set (suc ℓ)
 
 private
   variable
@@ -168,7 +168,7 @@ mutual
 
 -- An annotation function computes the top-level annotation given a
 -- term annotated at all sub-terms.
-AnnotationFun : Annotation ℓ → Set ℓ
+AnnotationFun : Annotation ℓ → Set (suc ℓ)
 AnnotationFun Ann = ∀ u {t : ⟦ u ⟧} → Annotated′ Ann t → Ann t
 
 

From c38f1409cd826e881a835945129a2032e770298e Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Tue, 10 Oct 2023 10:45:02 +0200
Subject: [PATCH 2/6] Prepare for v1.7.3: move CHANGELOG to CHANGELOG/v1.7.2

---
 CHANGELOG.md => CHANGELOG/v1.7.2.md | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename CHANGELOG.md => CHANGELOG/v1.7.2.md (100%)

diff --git a/CHANGELOG.md b/CHANGELOG/v1.7.2.md
similarity index 100%
rename from CHANGELOG.md
rename to CHANGELOG/v1.7.2.md

From 2f2c413d4adcb854f25a865d578e929020d82d5b Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Tue, 10 Oct 2023 10:48:05 +0200
Subject: [PATCH 3/6] v1.7.3 CHANGELOG entry for `--large-indices` (#2030)

---
 CHANGELOG.md | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 CHANGELOG.md

diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000000..0b05a15bbd
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,11 @@
+Version 1.7.3
+=============
+
+The library has been tested using Agda 2.6.4.
+
+* To avoid _large indices_ that are by default no longer allowed in Agda 2.6.4,
+  universe levels have been increased in the following definitions:
+  - `Data.Star.Decoration.DecoratedWith`
+  - `Data.Star.Pointer.Pointer`
+  - `Reflection.AnnotatedAST.Typeₐ`
+  - `Reflection.AnnotatedAST.AnnotationFun`

From c7c145c5c963da352a4db29a65ec71cd2c5caa90 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Thu, 12 Oct 2023 18:39:54 +0200
Subject: [PATCH 4/6] Bump agda-stdlib-utils to 1.7.3 and update its
 dependencies

---
 agda-stdlib-utils.cabal | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/agda-stdlib-utils.cabal b/agda-stdlib-utils.cabal
index 6e8bc7b33b..b3860888ab 100644
--- a/agda-stdlib-utils.cabal
+++ b/agda-stdlib-utils.cabal
@@ -1,5 +1,5 @@
 name:            agda-stdlib-utils
-version:         1.7.2
+version:         1.7.3
 cabal-version:   >= 1.10
 build-type:      Simple
 description:     Helper programs.
@@ -11,24 +11,26 @@ tested-with:     GHC == 8.0.2
                  GHC == 8.8.4
                  GHC == 8.10.7
                  GHC == 9.0.2
-                 GHC == 9.2.1
-                 GHC == 9.4.4
+                 GHC == 9.2.8
+                 GHC == 9.4.7
+                 GHC == 9.6.3
+                 GHC == 9.8.1
 
 executable GenerateEverything
   hs-source-dirs:   .
   main-is:          GenerateEverything.hs
   default-language: Haskell2010
   default-extensions: PatternGuards, PatternSynonyms
-  build-depends:      base      >= 4.9.0.0 && < 4.18
+  build-depends:      base      >= 4.9.0.0 && < 4.20
                     , directory >= 1.0.0.0 && < 1.4
                     , filemanip >= 0.3.6.2 && < 0.4
                     , filepath  >= 1.4.1.0 && < 1.5
-                    , mtl       >= 2.2.2   && < 2.3
+                    , mtl       >= 2.2.2   && < 2.4
 
 executable AllNonAsciiChars
   hs-source-dirs:   .
   main-is:          AllNonAsciiChars.hs
   default-language: Haskell2010
-  build-depends:      base      >= 4.9.0.0 && < 4.18
+  build-depends:      base      >= 4.9.0.0 && < 4.20
                     , filemanip >= 0.3.6.2 && < 0.4
-                    , text      >= 1.2.3.0 && < 2.1
+                    , text      >= 1.2.3.0 && < 2.2

From 60816a7448051437b2e5a80f4f800b0eb328d9c1 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Wed, 11 Oct 2023 12:06:55 +0200
Subject: [PATCH 5/6] Add CITATION.cff; bump version to 1.7.3

bump to 1.7.3 in
- standard-library.agda-lib
- README.agda
- installation-guide.txt
---
 CITATION.cff                |  8 ++++++++
 README.agda                 |  4 ++--
 notes/installation-guide.md | 12 ++++++------
 standard-library.agda-lib   |  2 +-
 4 files changed, 17 insertions(+), 9 deletions(-)
 create mode 100644 CITATION.cff

diff --git a/CITATION.cff b/CITATION.cff
new file mode 100644
index 0000000000..78e63bd810
--- /dev/null
+++ b/CITATION.cff
@@ -0,0 +1,8 @@
+cff-version: 1.2.0
+message: "If you use this software, please cite it as below."
+authors:
+- name: "The Agda Community"
+title: "Agda Standard Library"
+version: 1.7.3
+date-released: 2023-10-15
+url: "https://github.com/agda/agda-stdlib"
\ No newline at end of file
diff --git a/README.agda b/README.agda
index 1406d70967..1b5bc7f351 100644
--- a/README.agda
+++ b/README.agda
@@ -3,7 +3,7 @@
 module README where
 
 ------------------------------------------------------------------------
--- The Agda standard library, version 1.7.2
+-- The Agda standard library, version 1.7.3
 --
 -- Authors: Nils Anders Danielsson, Matthew Daggitt, Guillaume Allais
 -- with contributions from Andreas Abel, Stevan Andjelkovic,
@@ -18,7 +18,7 @@ module README where
 -- Noam Zeilberger and other anonymous contributors.
 ------------------------------------------------------------------------
 
--- This version of the library has been tested using Agda 2.6.2.
+-- This version of the library has been tested using Agda 2.6.4.
 
 -- The library comes with a .agda-lib file, for use with the library
 -- management system.
diff --git a/notes/installation-guide.md b/notes/installation-guide.md
index e51088aa6a..0086700170 100644
--- a/notes/installation-guide.md
+++ b/notes/installation-guide.md
@@ -1,19 +1,19 @@
 Installation instructions
 =========================
 
-Use version v1.7.2 of the standard library with Agda 2.6.2.
+Use version v1.7.3 of the standard library with Agda 2.6.4.
 
 1. Navigate to a suitable directory `$HERE` (replace appropriately) where
    you would like to install the library.
 
-2. Download the tarball of v1.7.2 of the standard library. This can either be
+2. Download the tarball of v1.7.3 of the standard library. This can either be
    done manually by visiting the Github repository for the library, or via the
    command line as follows:
    ```
-   wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.7.2.tar.gz
+   wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.7.3.tar.gz
    ```
    Note that you can replace `wget` with other popular tools such as `curl` and that
-   you can replace `1.7.2` with any other version of the library you desire.
+   you can replace `1.7.3` with any other version of the library you desire.
 
 3. Extract the standard library from the tarball. Again this can either be
    done manually or via the command line as follows:
@@ -24,14 +24,14 @@ Use version v1.7.2 of the standard library with Agda 2.6.2.
 4. [ OPTIONAL ] If using [cabal](https://www.haskell.org/cabal/) then run
    the commands to install via cabal:
    ```
-   cd agda-stdlib-1.7.2
+   cd agda-stdlib-1.7.3
    cabal install
    ```
 
 5. Register the standard library with Agda's package system by adding
    the following line to `$HOME/.agda/libraries`:
    ```
-   $HERE/agda-stdlib-1.7.2/standard-library.agda-lib
+   $HERE/agda-stdlib-1.7.3/standard-library.agda-lib
    ```
 
 Now, the standard library is ready to be used either:
diff --git a/standard-library.agda-lib b/standard-library.agda-lib
index 29885b7c5c..4f40cf4b61 100644
--- a/standard-library.agda-lib
+++ b/standard-library.agda-lib
@@ -1,4 +1,4 @@
-name: standard-library-1.7.2
+name: standard-library-1.7.3
 include: src
 flags:
   --warning=noUnsupportedIndexedMatch

From 657fe75754b480173c0e33df04070406796fc5f0 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Thu, 12 Oct 2023 14:50:46 +0200
Subject: [PATCH 6/6] Add some aliases for forward compatibility with v2.0

Some objects will get a new name in v2.0.
We add some of these names already here to ease the transition to v2.0:

- add modules `Effect.*` reexporting `Category.*`
- add `IO.Primitive.pure` as alias for `IO.Primitive.return`
---
 CHANGELOG.md                               |  7 +++++++
 src/Effect/Applicative.agda                | 12 ++++++++++++
 src/Effect/Applicative/Indexed.agda        | 12 ++++++++++++
 src/Effect/Applicative/Predicate.agda      | 12 ++++++++++++
 src/Effect/Comonad.agda                    | 12 ++++++++++++
 src/Effect/Functor.agda                    | 12 ++++++++++++
 src/Effect/Functor/Indexed.agda            | 12 ++++++++++++
 src/Effect/Functor/Predicate.agda          | 12 ++++++++++++
 src/Effect/Monad.agda                      | 12 ++++++++++++
 src/Effect/Monad/Continuation.agda         | 12 ++++++++++++
 src/Effect/Monad/Indexed.agda              | 12 ++++++++++++
 src/Effect/Monad/Partiality.agda           | 12 ++++++++++++
 src/Effect/Monad/Partiality/All.agda       | 12 ++++++++++++
 src/Effect/Monad/Partiality/Instances.agda | 12 ++++++++++++
 src/Effect/Monad/Predicate.agda            | 12 ++++++++++++
 src/Effect/Monad/Reader.agda               | 12 ++++++++++++
 src/Effect/Monad/State.agda                | 12 ++++++++++++
 src/IO/Primitive.agda                      |  3 +++
 18 files changed, 202 insertions(+)
 create mode 100644 src/Effect/Applicative.agda
 create mode 100644 src/Effect/Applicative/Indexed.agda
 create mode 100644 src/Effect/Applicative/Predicate.agda
 create mode 100644 src/Effect/Comonad.agda
 create mode 100644 src/Effect/Functor.agda
 create mode 100644 src/Effect/Functor/Indexed.agda
 create mode 100644 src/Effect/Functor/Predicate.agda
 create mode 100644 src/Effect/Monad.agda
 create mode 100644 src/Effect/Monad/Continuation.agda
 create mode 100644 src/Effect/Monad/Indexed.agda
 create mode 100644 src/Effect/Monad/Partiality.agda
 create mode 100644 src/Effect/Monad/Partiality/All.agda
 create mode 100644 src/Effect/Monad/Partiality/Instances.agda
 create mode 100644 src/Effect/Monad/Predicate.agda
 create mode 100644 src/Effect/Monad/Reader.agda
 create mode 100644 src/Effect/Monad/State.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0b05a15bbd..8de9bf14ee 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,3 +9,10 @@ The library has been tested using Agda 2.6.4.
   - `Data.Star.Pointer.Pointer`
   - `Reflection.AnnotatedAST.Typeₐ`
   - `Reflection.AnnotatedAST.AnnotationFun`
+
+* The following aliases have been added:
+  - `IO.Primitive.pure` as alias for `IO.Primitive.return`
+  - modules `Effect.*` as aliases for modules `Category.*`
+
+  These allow to address said objects with the new name they will have in v2.0 of the library,
+  to ease the transition from v1.7.3 to v2.0.
diff --git a/src/Effect/Applicative.agda b/src/Effect/Applicative.agda
new file mode 100644
index 0000000000..859131b8a6
--- /dev/null
+++ b/src/Effect/Applicative.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Applicative`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Applicative where
+
+open import Category.Applicative public
diff --git a/src/Effect/Applicative/Indexed.agda b/src/Effect/Applicative/Indexed.agda
new file mode 100644
index 0000000000..58a7c6418a
--- /dev/null
+++ b/src/Effect/Applicative/Indexed.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Applicative.Indexed`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Applicative.Indexed where
+
+open import Category.Applicative.Indexed public
diff --git a/src/Effect/Applicative/Predicate.agda b/src/Effect/Applicative/Predicate.agda
new file mode 100644
index 0000000000..b28c57598f
--- /dev/null
+++ b/src/Effect/Applicative/Predicate.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Applicative.Predicate`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Applicative.Predicate where
+
+open import Category.Applicative.Predicate public
diff --git a/src/Effect/Comonad.agda b/src/Effect/Comonad.agda
new file mode 100644
index 0000000000..45ea111c5a
--- /dev/null
+++ b/src/Effect/Comonad.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Comonad`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Comonad where
+
+open import Category.Comonad public
diff --git a/src/Effect/Functor.agda b/src/Effect/Functor.agda
new file mode 100644
index 0000000000..5c276929b6
--- /dev/null
+++ b/src/Effect/Functor.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Functor`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Functor where
+
+open import Category.Functor public
diff --git a/src/Effect/Functor/Indexed.agda b/src/Effect/Functor/Indexed.agda
new file mode 100644
index 0000000000..9d4efdef1f
--- /dev/null
+++ b/src/Effect/Functor/Indexed.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Functor.Indexed`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Functor.Indexed where
+
+open import Category.Functor.Indexed public
diff --git a/src/Effect/Functor/Predicate.agda b/src/Effect/Functor/Predicate.agda
new file mode 100644
index 0000000000..a11b2cef64
--- /dev/null
+++ b/src/Effect/Functor/Predicate.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Functor.Predicate`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Functor.Predicate where
+
+open import Category.Functor.Predicate public
diff --git a/src/Effect/Monad.agda b/src/Effect/Monad.agda
new file mode 100644
index 0000000000..c4df178be8
--- /dev/null
+++ b/src/Effect/Monad.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Monad`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Monad where
+
+open import Category.Monad public
diff --git a/src/Effect/Monad/Continuation.agda b/src/Effect/Monad/Continuation.agda
new file mode 100644
index 0000000000..357102eef6
--- /dev/null
+++ b/src/Effect/Monad/Continuation.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Monad.Continuation`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Monad.Continuation where
+
+open import Category.Monad.Continuation public
diff --git a/src/Effect/Monad/Indexed.agda b/src/Effect/Monad/Indexed.agda
new file mode 100644
index 0000000000..8bed8e27eb
--- /dev/null
+++ b/src/Effect/Monad/Indexed.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Monad.Indexed`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Monad.Indexed where
+
+open import Category.Monad.Indexed public
diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda
new file mode 100644
index 0000000000..80783e6148
--- /dev/null
+++ b/src/Effect/Monad/Partiality.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Monad.Partiality`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Monad.Partiality where
+
+open import Category.Monad.Partiality public
diff --git a/src/Effect/Monad/Partiality/All.agda b/src/Effect/Monad/Partiality/All.agda
new file mode 100644
index 0000000000..f91e83b6d5
--- /dev/null
+++ b/src/Effect/Monad/Partiality/All.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Monad.Partiality.All`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Monad.Partiality.All where
+
+open import Category.Monad.Partiality.All public
diff --git a/src/Effect/Monad/Partiality/Instances.agda b/src/Effect/Monad/Partiality/Instances.agda
new file mode 100644
index 0000000000..aa322c83ab
--- /dev/null
+++ b/src/Effect/Monad/Partiality/Instances.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Monad.Partiality.Instances`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Monad.Partiality.Instances where
+
+open import Category.Monad.Partiality.Instances public
diff --git a/src/Effect/Monad/Predicate.agda b/src/Effect/Monad/Predicate.agda
new file mode 100644
index 0000000000..56d6dbe0a4
--- /dev/null
+++ b/src/Effect/Monad/Predicate.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Monad.Predicate`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Monad.Predicate where
+
+open import Category.Monad.Predicate public
diff --git a/src/Effect/Monad/Reader.agda b/src/Effect/Monad/Reader.agda
new file mode 100644
index 0000000000..78d05ae0de
--- /dev/null
+++ b/src/Effect/Monad/Reader.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Monad.Reader`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Monad.Reader where
+
+open import Category.Monad.Reader public
diff --git a/src/Effect/Monad/State.agda b/src/Effect/Monad/State.agda
new file mode 100644
index 0000000000..14ffbf6b5c
--- /dev/null
+++ b/src/Effect/Monad/State.agda
@@ -0,0 +1,12 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- This module duplicates `Category.Monad.State`
+-- for forward compatibility with v2.0.
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Effect.Monad.State where
+
+open import Category.Monad.State public
diff --git a/src/IO/Primitive.agda b/src/IO/Primitive.agda
index 45ae1b5fc5..a0e15a3c5d 100644
--- a/src/IO/Primitive.agda
+++ b/src/IO/Primitive.agda
@@ -27,3 +27,6 @@ postulate
 {-# COMPILE GHC _>>=_  = \_ _ _ _ -> (>>=) #-}
 {-# COMPILE UHC return = \_ _ x -> UHC.Agda.Builtins.primReturn x #-}
 {-# COMPILE UHC _>>=_  = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-}
+
+-- Forward compatibility with v2.0.
+pure = return