diff --git a/gnu/packages/agda.scm b/gnu/packages/agda.scm
index 16573e6d57..240a51de1a 100644
--- a/gnu/packages/agda.scm
+++ b/gnu/packages/agda.scm
@@ -262,3 +262,36 @@ (define-public agda-categories
     (description "A new Categories library for Agda")
     (home-page "https://github.com/agda/agda-categories")
     (license license:expat)))
+
+(define-public agda-cubical
+  ;; Upstream's HEAD follows the latest Agda release, but they don't release
+  ;; until a newer Agda release comes up, so their releases are always one
+  ;; version late.
+  (let* ((revision "1")
+         (commit "814d54b08b360b8e80828065f54b80e3a98a0092"))
+    (package
+      (name "agda-cubical")
+      (version (git-version "0.4" revision commit))
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://github.com/agda/cubical.git")
+                      (commit commit)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "0d25gb1qzpx539k62qjsjq4xmzp34qk7n3hmd9y6v8slhrrxw312"))))
+      (build-system agda-build-system)
+      (arguments
+       (list
+        #:gnu-and-haskell? #t
+        #:phases
+        #~(modify-phases %standard-phases
+            (replace 'build
+              (lambda _
+                (invoke "make"))))))
+      (synopsis "Standard library for Cubical Agda")
+      (description "A standard library for Cubical Agda, comparable to
+agda-stdlib but using cubical methods.")
+      (home-page "https://github.com/agda/cubical")
+      (license license:expat))))