Update to Agda 2.6.4

.github/workflows/ci.yaml

@@ -37,7 +37,7 @@ jobs:
     strategy:
       matrix:
         os: [macOS-latest, ubuntu-latest]
-        agda: ['2.6.3']
+        agda: ['2.6.4']
     steps:
       - name: Checkout our repository
         uses: actions/checkout@v3

.github/workflows/pages.yaml

@@ -27,7 +27,7 @@ jobs:
     runs-on: macOS-latest
     strategy:
       matrix:
-        agda: ['2.6.3']
+        agda: ['2.6.4']
     environment:
       name: github-pages
       url: ${{ steps.deployment.outputs.page_url }}

DESIGN-PRINCIPLES.md

@@ -6,8 +6,8 @@ to it. This document aims to provide a clear and concise introduction.
 
 ## Postulates and assumptions
 
-The library assumes the `--without-K` and `--exact-split` flags of Agda and
-makes use of several postulates.
+The library assumes the `--without-K`, `--exact-split`, and `--level-universe`
+flags of Agda and makes use of several postulates.
 
 1. We make full use of Agda's `data` types for introducing inductive types.
 2. We make full use of Agda's universe levels, including `ω`. However, it should

HOWTO-INSTALL.md

@@ -5,7 +5,7 @@
 ### Quick setup
 
 To work or experiment with the `agda-unimath` library on your machine, you will
-need to have `agda` version 2.6.3 installed, and a suitable editor such as
+need to have `agda` version 2.6.4 installed, and a suitable editor such as
 [Emacs](https://www.gnu.org/software/emacs/) or
 [Visual Studio Code](https://code.visualstudio.com/). The following instructions
 will help you on your way right away:
@@ -122,15 +122,15 @@ working branches when necessary.
 
 ## Installing Agda {#installing-agda}
 
-The `agda-unimath` library is built and verified with Agda 2.6.3, and we provide
+The `agda-unimath` library is built and verified with Agda 2.6.4, and we provide
 two methods for installation: with or without the package manager
 [Nix](https://nixos.org/). Nix streamlines the installation of Agda and its
 dependencies, providing a consistent and reproducible environment for the
 library across different systems.
 
 ### Without Nix
 
-To install Agda 2.6.3 without Nix, follow the
+To install Agda 2.6.4 without Nix, follow the
 [installation guide](https://agda.readthedocs.io/en/latest/getting-started/installation.html)
 provided on the Agda documentation page.
 

Makefile

@@ -4,7 +4,8 @@
 # files, and if these options are pervasive (i.e. they need to be enabled in all
 # modules that include the modules that have them enabled), then they need to be
 # added to the everything file as well.
-everythingOpts := --guardedness
+everythingOpts := --level-universe --guardedness
+
 # use "$ export AGDAVERBOSE=-v20" if you want to see all
 AGDAVERBOSE ?= -v1
 AGDAFILES := $(shell find src -name temp -prune -o -type f \( -name "*.lagda.md" -not -name "everything.lagda.md" \) -print)

agda-unimath.agda-lib

@@ -1,3 +1,3 @@
 name: agda-unimath
 include: src
-flags: --without-K --exact-split --no-import-sorts --auto-inline
+flags: --without-K --exact-split --level-universe --no-import-sorts --auto-inline

scripts/demote_foundation_imports.py

@@ -129,7 +129,7 @@ def process_agda_file(agda_file, agda_options, root, temp_dir):
     root = 'src'
     temp_dir = 'temp'
     status = 0
-    agda_options = '--without-K --exact-split --no-import-sorts --auto-inline --no-caching'
+    agda_options = '--without-K --exact-split --level-universe --no-import-sorts --auto-inline --no-caching'
 
     temp_root = os.path.join(root, temp_dir)
     shutil.rmtree(temp_root, ignore_errors=True)

scripts/remove_unused_imports.py

@@ -95,7 +95,7 @@ def process_agda_file(agda_file, agda_options, root, temp_dir):
     root = 'src'
     temp_dir = 'temp'
     status = 0
-    agda_options = '--without-K --exact-split --no-import-sorts --auto-inline --no-caching'
+    agda_options = '--without-K --exact-split --level-universe --no-import-sorts --auto-inline --no-caching'
 
     temp_root = os.path.join(root, temp_dir)
     shutil.rmtree(temp_root, ignore_errors=True)