diff --git a/.github/workflows/ci-ubuntu.yml b/.github/workflows/ci-ubuntu.yml
index 5129d5ff2..d8b3b347c 100644
--- a/.github/workflows/ci-ubuntu.yml
+++ b/.github/workflows/ci-ubuntu.yml
@@ -42,7 +42,7 @@ on:
 ########################################################################
 
 env:
-  AGDA_BRANCH: v2.6.4
+  AGDA_BRANCH: v2.6.4.1
   GHC_VERSION: 9.4.7
   CABAL_VERSION: 3.6.2.0
   CABAL_INSTALL: cabal install --overwrite-policy=always --ghc-options='-O1 +RTS -M6G -RTS'
diff --git a/CITATION.cff b/CITATION.cff
index 407d6f4ee..048a89cda 100644
--- a/CITATION.cff
+++ b/CITATION.cff
@@ -3,6 +3,6 @@ message: "If you use this software, please cite it as below."
 authors:
 - name: "The Agda Community"
 title: "Cubical Agda Library"
-version: 0.6
-date-released: 2023-10-24
+version: 0.7
+date-released: 2024-02-12
 url: "https://github.com/agda/cubical"
diff --git a/GNUmakefile b/GNUmakefile
index 9ff39ba0d..92830cce3 100644
--- a/GNUmakefile
+++ b/GNUmakefile
@@ -2,7 +2,7 @@ AGDA_BIN?=agda
 AGDA_FLAGS?=-W error
 AGDA_EXEC?=$(AGDA_BIN) $(AGDA_FLAGS)
 FIX_WHITESPACE?=fix-whitespace
-RTS_OPTIONS=+RTS -H6G -RTS
+RTS_OPTIONS=+RTS -M32G -RTS
 AGDA=$(AGDA_EXEC) $(RTS_OPTIONS)
 RUNHASKELL?=runhaskell
 EVERYTHINGS=$(RUNHASKELL) ./Everythings.hs
@@ -31,7 +31,7 @@ check-whitespace:
 
 .PHONY : check-everythings
 check-everythings:
-	$(EVERYTHINGS) check-except Experiments
+	$(EVERYTHINGS) check-except
 
 .PHONY : gen-everythings
 gen-everythings:
diff --git a/README.md b/README.md
index 9ce7431e4..e27dacc8e 100644
--- a/README.md
+++ b/README.md
@@ -15,15 +15,16 @@ If you want to use some specific release of Agda,
 the following table lists which releases of Agda you can use with which release of this library.
 Agda versions as written below, correspond to tags.
 
-| cubical library version | Agda versions     |
-|-------------------------|-------------------|
-| `current master`        | `v2.6.4`          |
-| `v0.6`                  | `v2.6.4`          |
-| `v0.5`                  | `v2.6.3` `v2.6.4` |
-| `v0.4`                  | `v2.6.2.2`        |
-| `v0.3`                  | `v2.6.2`          |
-| `v0.2`                  | `v2.6.1.3`        |
-| `v0.1`                  | `v2.6.0.1`        |
+| cubical library version | Agda versions       |
+|-------------------------|---------------------|
+| current master          | `v2.6.4` `v2.6.4.1` |
+| `v0.7`                  | `v2.6.4` `v2.6.4.1` |
+| `v0.6`                  | `v2.6.4`            |
+| `v0.5`                  | `v2.6.3` `v2.6.4`   |
+| `v0.4`                  | `v2.6.2.2`          |
+| `v0.3`                  | `v2.6.2`            |
+| `v0.2`                  | `v2.6.1.3`          |
+| `v0.1`                  | `v2.6.0.1`          |
 
 For example, if you have Agda 2.6.2.2, you can switch to version 0.4 of the cubical library with
 ```
diff --git a/cubical.agda-lib b/cubical.agda-lib
index 6565f1c36..064f900d4 100644
--- a/cubical.agda-lib
+++ b/cubical.agda-lib
@@ -1,4 +1,4 @@
-name: cubical-0.6
+name: cubical-0.7
 include: .
 depend:
 flags: --cubical --no-import-sorts -WnoUnsupportedIndexedMatch
diff --git a/flake.lock b/flake.lock
index b8510c40c..6fa40f03e 100644
--- a/flake.lock
+++ b/flake.lock
@@ -10,16 +10,16 @@
         ]
       },
       "locked": {
-        "lastModified": 1696540558,
-        "narHash": "sha256-fqYyjgOFQrU4ryGcLyz5gMYMdPk1P24ra7kQiUrbilg=",
+        "lastModified": 1701366566,
+        "narHash": "sha256-B8Jmjld0gGbkVO08GsovVqrUXCs8VfJ8UdM3sjHnzgM=",
         "owner": "agda",
         "repo": "agda",
-        "rev": "f42acb696e43d382639f04f869e9a99ab36a91c6",
+        "rev": "4293e0a94d15acac915ab9088b2ec028f78d14a9",
         "type": "github"
       },
       "original": {
         "owner": "agda",
-        "ref": "v2.6.4",
+        "ref": "v2.6.4.1",
         "repo": "agda",
         "type": "github"
       }
@@ -45,11 +45,11 @@
         "systems": "systems"
       },
       "locked": {
-        "lastModified": 1694529238,
-        "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=",
+        "lastModified": 1705309234,
+        "narHash": "sha256-uNRRNRKmJyCRC/8y1RqBkqWBLM034y4qN7EprSdmgyA=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "ff7b65b44d01cf9ba6a71320833626af21126384",
+        "rev": "1ef2e671c3b0c19053962c07dbda38332dcebf26",
         "type": "github"
       },
       "original": {
@@ -60,11 +60,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1696757521,
-        "narHash": "sha256-cfgtLNCBLFx2qOzRLI6DHfqTdfWI+UbvsKYa3b3fvaA=",
+        "lastModified": 1705883077,
+        "narHash": "sha256-ByzHHX3KxpU1+V0erFy8jpujTufimh6KaS/Iv3AciHk=",
         "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "2646b294a146df2781b1ca49092450e8a32814e1",
+        "rev": "5f5210aa20e343b7e35f40c033000db0ef80d7b9",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index 2d5fcb7c3..42f1b1bea 100644
--- a/flake.nix
+++ b/flake.nix
@@ -8,7 +8,7 @@
     flake = false;
   };
   inputs.agda = {
-    url = "github:agda/agda/v2.6.4";
+    url = "github:agda/agda/v2.6.4.1";
     inputs = {
       nixpkgs.follows = "nixpkgs";
       flake-utils.follows = "flake-utils";
@@ -21,7 +21,7 @@
       overlay = final: prev: {
         cubical = final.agdaPackages.mkDerivation rec {
           pname = "cubical";
-          version = "0.6";
+          version = "0.7";
 
           src = cleanSourceWith {
             filter = name: type: