diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index 70773cd832..c8f3e3f4d2 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -2,12 +2,10 @@ name: Ubuntu build
 on:
   push:
     branches:
-      - master
-      - experimental
+    - release-1.7.3-base
   pull_request:
     branches:
-      - master
-      - experimental
+    - release-1.7.3-base
 
 ########################################################################
 ## CONFIGURATION
@@ -46,11 +44,11 @@ on:
 ########################################################################
 
 env:
-  GHC_VERSION: 8.6.5
-  CABAL_VERSION: 3.2.0.0
+  GHC_VERSION: 9.6.3
+  CABAL_VERSION: 3.10.1.0
   CABAL_INSTALL: cabal v1-install --ghc-options='-O1 +RTS -M6G -RTS'
   # CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
-  AGDA: agda -Werror +RTS -M3.5G -H3.5G -A128M -RTS -i. -i src/
+  AGDA: agda -Werror +RTS -M6G -H3.5G -A128M -RTS -i. -i src/
 
 jobs:
   test-stdlib:
@@ -71,22 +69,10 @@ jobs:
 
       - name: Initialise variables
         run: |
-          if [[ '${{ github.ref }}' == 'refs/heads/master' \
-             || '${{ github.base_ref }}' == 'master' ]]; then
-            # Pick Agda version for master
-            echo "AGDA_COMMIT=tags/v2.6.1.3.20210524" >> $GITHUB_ENV;
-            echo "AGDA_HTML_DIR=html" >> $GITHUB_ENV
-          elif [[ '${{ github.ref }}' == 'refs/heads/experimental' \
-               || '${{ github.base_ref }}' == 'experimental' ]]; then
-            # Pick Agda version for experimental
-            echo "AGDA_COMMIT=9047e32a1b0cba98a299ed439a08d35bc4846f99" >> $GITHUB_ENV;
-            echo "AGDA_HTML_DIR=html/experimental" >> $GITHUB_ENV
-          fi
-
-          if [[ '${{ github.ref }}' == 'refs/heads/master' \
-             || '${{ github.ref }}' == 'refs/heads/experimental' ]]; then
-             echo "AGDA_DEPLOY=true" >> $GITHUB_ENV
-          fi
+          echo "AGDA_COMMIT=tags/v2.6.4"   >> "$GITHUB_ENV"
+          echo "AGDA_HTML_DIR=html/v1.7.3" >> "$GITHUB_ENV"
+          echo "AGDA_DEPLOY=true"          >> "$GITHUB_ENV"
+
 
 ########################################################################
 ## CACHING
@@ -98,14 +84,17 @@ jobs:
       # i.e. if we change either the version of Agda, ghc, or cabal that we want
       # to use for the build.
       - name: Cache cabal packages
-        uses: actions/cache@v2
+        uses: actions/cache@v3
         id: cache-cabal
         with:
           path: |
             ~/.cabal/packages
             ~/.cabal/store
             ~/.cabal/bin
-          key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_COMMIT }}
+          key: ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_COMMIT }}-${{ github.sha }}
+          restore-keys: |
+            ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-${{ env.AGDA_COMMIT }}-
+            ${{ runner.os }}-${{ env.GHC_VERSION }}-${{ env.CABAL_VERSION }}-
 
 ########################################################################
 ## INSTALLATION STEPS
@@ -113,16 +102,19 @@ jobs:
 
       - name: Install cabal
         if: steps.cache-cabal.outputs.cache-hit != 'true'
-        uses: actions/setup-haskell@v1.1.3
+        uses: haskell-actions/setup@v2
         with:
           ghc-version: ${{ env.GHC_VERSION }}
           cabal-version: ${{ env.CABAL_VERSION }}
+          cabal-update: true
 
       - name: Put cabal programs in PATH
-        run: echo "~/.cabal/bin" >> $GITHUB_PATH
+        run: echo "~/.cabal/bin" >> "$GITHUB_PATH"
 
-      - name: Cabal update
-        run: cabal update
+      - name: Install alex and happy
+        if: steps.cache-cabal.outputs.cache-hit != 'true'
+        run: |
+          ${{ env.CABAL_INSTALL }} alex happy
 
       - name: Download and install Agda from github
         if: steps.cache-cabal.outputs.cache-hit != 'true'
@@ -141,7 +133,7 @@ jobs:
 
       # By default github actions do not pull the repo
       - name: Checkout stdlib
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
 
       - name: Test stdlib
         run: |
@@ -182,10 +174,10 @@ jobs:
 
 
       - name: Deploy HTML
-        uses: JamesIves/github-pages-deploy-action@4.1.3
+        uses: JamesIves/github-pages-deploy-action@v4
         if: ${{ success() && env.AGDA_DEPLOY }}
 
         with:
           branch: gh-pages
           folder: html
-          git-config-name: Github Actions
\ No newline at end of file
+          git-config-name: Github Actions
diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml
index 3eef98ae73..064b6865a1 100644
--- a/.github/workflows/haskell-ci.yml
+++ b/.github/workflows/haskell-ci.yml
@@ -6,79 +6,148 @@
 #
 #   haskell-ci regenerate
 #
-# For more information, see https://github.com/haskell-CI/haskell-ci
+# For more information, see https://github.com/andreasabel/haskell-ci
 #
-# version: 0.12.1
+# version: 0.17.20231010
 #
-# REGENDATA ("0.12.1",["github","--no-cabal-check","agda-stdlib-utils.cabal"])
+# REGENDATA ("0.17.20231010",["github","--no-cabal-check","agda-stdlib-utils.cabal"])
 #
 name: Haskell-CI
 on:
   push:
     branches:
-      - master
-      - experimental
+      - release-1.7.3-base
   pull_request:
     branches:
-      - master
-      - experimental
+      - release-1.7.3-base
 jobs:
   linux:
     name: Haskell-CI - Linux - ${{ matrix.compiler }}
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
+    timeout-minutes:
+      60
     container:
-      image: buildpack-deps:xenial
+      image: buildpack-deps:focal
     continue-on-error: ${{ matrix.allow-failure }}
     strategy:
       matrix:
         include:
-          - compiler: ghc-9.0.1
+          - compiler: ghc-9.8.1
+            compilerKind: ghc
+            compilerVersion: 9.8.1
+            setup-method: ghcup
             allow-failure: false
-          - compiler: ghc-8.10.4
+          - compiler: ghc-9.6.3
+            compilerKind: ghc
+            compilerVersion: 9.6.3
+            setup-method: ghcup
+            allow-failure: false
+          - compiler: ghc-9.4.7
+            compilerKind: ghc
+            compilerVersion: 9.4.7
+            setup-method: ghcup
+            allow-failure: false
+          - compiler: ghc-9.2.8
+            compilerKind: ghc
+            compilerVersion: 9.2.8
+            setup-method: ghcup
+            allow-failure: false
+          - compiler: ghc-9.0.2
+            compilerKind: ghc
+            compilerVersion: 9.0.2
+            setup-method: ghcup
+            allow-failure: false
+          - compiler: ghc-8.10.7
+            compilerKind: ghc
+            compilerVersion: 8.10.7
+            setup-method: ghcup
             allow-failure: false
           - compiler: ghc-8.8.4
+            compilerKind: ghc
+            compilerVersion: 8.8.4
+            setup-method: hvr-ppa
             allow-failure: false
           - compiler: ghc-8.6.5
+            compilerKind: ghc
+            compilerVersion: 8.6.5
+            setup-method: hvr-ppa
             allow-failure: false
           - compiler: ghc-8.4.4
+            compilerKind: ghc
+            compilerVersion: 8.4.4
+            setup-method: hvr-ppa
             allow-failure: false
           - compiler: ghc-8.2.2
+            compilerKind: ghc
+            compilerVersion: 8.2.2
+            setup-method: hvr-ppa
             allow-failure: false
           - compiler: ghc-8.0.2
+            compilerKind: ghc
+            compilerVersion: 8.0.2
+            setup-method: hvr-ppa
             allow-failure: false
       fail-fast: false
     steps:
       - name: apt
         run: |
           apt-get update
-          apt-get install -y --no-install-recommends gnupg ca-certificates dirmngr curl git software-properties-common
-          apt-add-repository -y 'ppa:hvr/ghc'
-          apt-get update
-          apt-get install -y $CC cabal-install-3.4
+          apt-get install -y --no-install-recommends gnupg ca-certificates dirmngr curl git software-properties-common libtinfo5
+          if [ "${{ matrix.setup-method }}" = ghcup ]; then
+            mkdir -p "$HOME/.ghcup/bin"
+            curl -sL https://downloads.haskell.org/ghcup/0.1.19.5/x86_64-linux-ghcup-0.1.19.5 > "$HOME/.ghcup/bin/ghcup"
+            chmod a+x "$HOME/.ghcup/bin/ghcup"
+            "$HOME/.ghcup/bin/ghcup" config add-release-channel https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-prereleases-0.0.7.yaml;
+            "$HOME/.ghcup/bin/ghcup" install ghc "$HCVER" || (cat "$HOME"/.ghcup/logs/*.* && false)
+            "$HOME/.ghcup/bin/ghcup" install cabal 3.10.1.0 || (cat "$HOME"/.ghcup/logs/*.* && false)
+          else
+            apt-add-repository -y 'ppa:hvr/ghc'
+            apt-get update
+            apt-get install -y "$HCNAME"
+            mkdir -p "$HOME/.ghcup/bin"
+            curl -sL https://downloads.haskell.org/ghcup/0.1.19.5/x86_64-linux-ghcup-0.1.19.5 > "$HOME/.ghcup/bin/ghcup"
+            chmod a+x "$HOME/.ghcup/bin/ghcup"
+            "$HOME/.ghcup/bin/ghcup" config add-release-channel https://raw.githubusercontent.com/haskell/ghcup-metadata/master/ghcup-prereleases-0.0.7.yaml;
+            "$HOME/.ghcup/bin/ghcup" install cabal 3.10.1.0 || (cat "$HOME"/.ghcup/logs/*.* && false)
+          fi
         env:
-          CC: ${{ matrix.compiler }}
+          HCKIND: ${{ matrix.compilerKind }}
+          HCNAME: ${{ matrix.compiler }}
+          HCVER: ${{ matrix.compilerVersion }}
       - name: Set PATH and environment variables
         run: |
           echo "$HOME/.cabal/bin" >> $GITHUB_PATH
-          echo "LANG=C.UTF-8" >> $GITHUB_ENV
-          echo "CABAL_DIR=$HOME/.cabal" >> $GITHUB_ENV
-          echo "CABAL_CONFIG=$HOME/.cabal/config" >> $GITHUB_ENV
-          HCDIR=$(echo "/opt/$CC" | sed 's/-/\//')
-          HCNAME=ghc
-          HC=$HCDIR/bin/$HCNAME
-          echo "HC=$HC" >> $GITHUB_ENV
-          echo "HCPKG=$HCDIR/bin/$HCNAME-pkg" >> $GITHUB_ENV
-          echo "HADDOCK=$HCDIR/bin/haddock" >> $GITHUB_ENV
-          echo "CABAL=/opt/cabal/3.4/bin/cabal -vnormal+nowrap" >> $GITHUB_ENV
+          echo "LANG=C.UTF-8" >> "$GITHUB_ENV"
+          echo "CABAL_DIR=$HOME/.cabal" >> "$GITHUB_ENV"
+          echo "CABAL_CONFIG=$HOME/.cabal/config" >> "$GITHUB_ENV"
+          HCDIR=/opt/$HCKIND/$HCVER
+          if [ "${{ matrix.setup-method }}" = ghcup ]; then
+            HC=$("$HOME/.ghcup/bin/ghcup" whereis ghc "$HCVER")
+            HCPKG=$(echo "$HC" | sed 's#ghc$#ghc-pkg#')
+            HADDOCK=$(echo "$HC" | sed 's#ghc$#haddock#')
+            echo "HC=$HC" >> "$GITHUB_ENV"
+            echo "HCPKG=$HCPKG" >> "$GITHUB_ENV"
+            echo "HADDOCK=$HADDOCK" >> "$GITHUB_ENV"
+            echo "CABAL=$HOME/.ghcup/bin/cabal-3.10.1.0 -vnormal+nowrap" >> "$GITHUB_ENV"
+          else
+            HC=$HCDIR/bin/$HCKIND
+            echo "HC=$HC" >> "$GITHUB_ENV"
+            echo "HCPKG=$HCDIR/bin/$HCKIND-pkg" >> "$GITHUB_ENV"
+            echo "HADDOCK=$HCDIR/bin/haddock" >> "$GITHUB_ENV"
+            echo "CABAL=$HOME/.ghcup/bin/cabal-3.10.1.0 -vnormal+nowrap" >> "$GITHUB_ENV"
+          fi
+
           HCNUMVER=$(${HC} --numeric-version|perl -ne '/^(\d+)\.(\d+)\.(\d+)(\.(\d+))?$/; print(10000 * $1 + 100 * $2 + ($3 == 0 ? $5 != 1 : $3))')
-          echo "HCNUMVER=$HCNUMVER" >> $GITHUB_ENV
-          echo "ARG_TESTS=--enable-tests" >> $GITHUB_ENV
-          echo "ARG_BENCH=--enable-benchmarks" >> $GITHUB_ENV
-          echo "HEADHACKAGE=false" >> $GITHUB_ENV
-          echo "ARG_COMPILER=--$HCNAME --with-compiler=$HC" >> $GITHUB_ENV
-          echo "GHCJSARITH=0" >> $GITHUB_ENV
+          echo "HCNUMVER=$HCNUMVER" >> "$GITHUB_ENV"
+          echo "ARG_TESTS=--enable-tests" >> "$GITHUB_ENV"
+          echo "ARG_BENCH=--enable-benchmarks" >> "$GITHUB_ENV"
+          echo "HEADHACKAGE=false" >> "$GITHUB_ENV"
+          echo "ARG_COMPILER=--$HCKIND --with-compiler=$HC" >> "$GITHUB_ENV"
+          echo "GHCJSARITH=0" >> "$GITHUB_ENV"
         env:
-          CC: ${{ matrix.compiler }}
+          HCKIND: ${{ matrix.compilerKind }}
+          HCNAME: ${{ matrix.compiler }}
+          HCVER: ${{ matrix.compilerVersion }}
       - name: env
         run: |
           env
@@ -101,6 +170,10 @@ jobs:
           repository hackage.haskell.org
             url: http://hackage.haskell.org/
           EOF
+          cat >> $CABAL_CONFIG <<EOF
+          program-default-options
+            ghc-options: $GHCJOBS +RTS -M3G -RTS
+          EOF
           cat $CABAL_CONFIG
       - name: versions
         run: |
@@ -113,14 +186,14 @@ jobs:
       - name: install cabal-plan
         run: |
           mkdir -p $HOME/.cabal/bin
-          curl -sL https://github.com/haskell-hvr/cabal-plan/releases/download/v0.6.2.0/cabal-plan-0.6.2.0-x86_64-linux.xz > cabal-plan.xz
-          echo 'de73600b1836d3f55e32d80385acc055fd97f60eaa0ab68a755302685f5d81bc  cabal-plan.xz' | sha256sum -c -
+          curl -sL https://github.com/haskell-hvr/cabal-plan/releases/download/v0.7.3.0/cabal-plan-0.7.3.0-x86_64-linux.xz > cabal-plan.xz
+          echo 'f62ccb2971567a5f638f2005ad3173dba14693a45154c1508645c52289714cb2  cabal-plan.xz' | sha256sum -c -
           xz -d < cabal-plan.xz > $HOME/.cabal/bin/cabal-plan
           rm -f cabal-plan.xz
           chmod a+x $HOME/.cabal/bin/cabal-plan
           cabal-plan --version
       - name: checkout
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
         with:
           path: source
       - name: initial cabal.project for sdist
@@ -139,7 +212,8 @@ jobs:
       - name: generate cabal.project
         run: |
           PKGDIR_agda_stdlib_utils="$(find "$GITHUB_WORKSPACE/unpacked" -maxdepth 1 -type d -regex '.*/agda-stdlib-utils-[0-9.]*')"
-          echo "PKGDIR_agda_stdlib_utils=${PKGDIR_agda_stdlib_utils}" >> $GITHUB_ENV
+          echo "PKGDIR_agda_stdlib_utils=${PKGDIR_agda_stdlib_utils}" >> "$GITHUB_ENV"
+          rm -f cabal.project cabal.project.local
           touch cabal.project
           touch cabal.project.local
           echo "packages: ${PKGDIR_agda_stdlib_utils}" >> cabal.project
@@ -154,8 +228,8 @@ jobs:
         run: |
           $CABAL v2-build $ARG_COMPILER $ARG_TESTS $ARG_BENCH --dry-run all
           cabal-plan
-      - name: cache
-        uses: actions/cache@v2
+      - name: restore cache
+        uses: actions/cache/restore@v3
         with:
           key: ${{ runner.os }}-${{ matrix.compiler }}-${{ github.sha }}
           path: ~/.cabal/store
@@ -170,7 +244,16 @@ jobs:
       - name: build
         run: |
           $CABAL v2-build $ARG_COMPILER $ARG_TESTS $ARG_BENCH all --write-ghc-environment-files=always
+      - name: haddock
+        run: |
+          $CABAL v2-haddock --disable-documentation --haddock-all $ARG_COMPILER --with-haddock $HADDOCK $ARG_TESTS $ARG_BENCH all
       - name: unconstrained build
         run: |
           rm -f cabal.project.local
           $CABAL v2-build $ARG_COMPILER --disable-tests --disable-benchmarks all
+      - name: save cache
+        uses: actions/cache/save@v3
+        if: always()
+        with:
+          key: ${{ runner.os }}-${{ matrix.compiler }}-${{ github.sha }}
+          path: ~/.cabal/store
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0183ec654f..8de9bf14ee 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,9 +1,18 @@
-Version 1.7.2
+Version 1.7.3
 =============
 
-The library has been tested using Agda 2.6.3.
+The library has been tested using Agda 2.6.4.
 
-* In accordance with changes to the flags in Agda 2.6.3, all modules that previously used
-  the `--without-K` flag now use the `--cubical-compatible` flag instead.
-  
-* Updated the code using `primFloatToWord64` - the library API has remained unchanged.
+* 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`
+
+* 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/CHANGELOG/v1.7.2.md b/CHANGELOG/v1.7.2.md
new file mode 100644
index 0000000000..0183ec654f
--- /dev/null
+++ b/CHANGELOG/v1.7.2.md
@@ -0,0 +1,9 @@
+Version 1.7.2
+=============
+
+The library has been tested using Agda 2.6.3.
+
+* In accordance with changes to the flags in Agda 2.6.3, all modules that previously used
+  the `--without-K` flag now use the `--cubical-compatible` flag instead.
+  
+* Updated the code using `primFloatToWord64` - the library API has remained unchanged.
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/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
diff --git a/cabal.haskell-ci b/cabal.haskell-ci
new file mode 100644
index 0000000000..ec3b597c83
--- /dev/null
+++ b/cabal.haskell-ci
@@ -0,0 +1 @@
+branches: release-1.7.3-base
\ No newline at end of file
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/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/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
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
 
 
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