[GUIDE] How to Set Up Cubical Agda + agda/cubical Library (2025 Edition)

Nyaa~! Welcome to the 2025 edition of the Cubical Agda setup guide, updated for the current Agda release! I keep seeing the same questions over and over so I finally wrote this up properly. Bookmark it. Pin it to your cat ear. nya~

⬡ Step 1 — Prerequisites

You need GHC + Cabal (or Stack) installed. The easiest way is via GHCup. Make sure you have:

• GHC ≥ 9.4 recommended (9.8 tested for Agda 2.6.4+)
• cabal-install ≥ 3.10, or stack ≥ 2.15
• git (for cloning the cubical library)
• Emacs or VS Code with agda-mode / cornelis

⬡ Step 2 — Install Agda via Cabal

To download and compile Agda using cabal v2-build, you need a recent (2.4 or later) version of cabal-install. Then run:

$ cabal update
$ cabal install Agda

This puts the agda and agda-mode executables in ~/.cabal/bin. In order to be able to access these on your system you need to add them to your $PATH environment variable.

# Add to ~/.bashrc or ~/.zshrc:
export PATH="$HOME/.cabal/bin:$PATH"
source ~/.bashrc  # or restart terminal

Verify it works:

$ agda --version
Agda version 2.6.4.3

⬡ Step 3 — Clone the agda/cubical Library

There is a standard agda/cubical library for Cubical Agda available at https://github.com/agda/cubical. Clone it somewhere stable — it won't "install" in the traditional sense; Agda reads it from wherever you put it.

$ mkdir -p ~/agda-libs
$ cd ~/agda-libs
$ git clone https://github.com/agda/cubical.git
$ cd cubical
# Optional: checkout a tagged release for stability:
$ git checkout v0.7  # check releases page for latest

⬡ Step 4 — Register the Library with Agda

In order to make this library visible to Agda, add /path/to/cubical/cubical.agda-lib to ~/.agda/libraries and add cubical to ~/.agda/defaults (where path/to is the absolute path to where the agda/cubical library has been installed).

$ mkdir -p ~/.agda

# Register the library path:
$ echo "/home/youruser/agda-libs/cubical/cubical.agda-lib" >> ~/.agda/libraries

# Make it a default library (so you don't need .agda-lib per project):
$ echo "cubical" >> ~/.agda/defaults

Your ~/.agda/ directory should now look like:

~/.agda/
├── libraries      # one path per line to .agda-lib files
└── defaults       # library names to load by default

⬡ Step 5 — The --cubical Flag

To use the cubical mode, Agda needs to be run with the --cubical command-line option or with {-# OPTIONS --cubical #-} at the top of the file.

The recommended way to get access to the Cubical primitives is to add the following to the top of a file (this assumes that the agda/cubical library is installed and visible to Agda):

{-# OPTIONS --cubical #-}
open import Cubical.Core.Everything

Or if you just want the foundations prelude:

{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude

-- Now you can write things like:
myRefl : ∀ {ℓ} {A : Set ℓ} {x : A} → x ≡ x
myRefl = refl

Other flag variants:

• --cubical — full cubical mode, paths are native, univalence computes
• --erased-cubical — a variant of Cubical Agda that is supported by the GHC backend
• --cubical-compatible — specifies that the module is compatible with Cubical Agda; modules without this flag cannot be imported from --cubical modules

⬡ Step 6 — Test Your Setup

Create a file HelloCubical.agda:

{-# OPTIONS --cubical #-}
module HelloCubical where

open import Cubical.Foundations.Prelude
open import Cubical.Data.Nat

-- A path is just a function I → A, nya~
three-is-three : ℕ
three-is-three = 3

-- refl works definitionally
test : 1 + 2 ≡ 3
test = refl

Load it with C-c C-l in Emacs or via the command line:

$ agda HelloCubical.agda
Checking HelloCubical (/home/you/HelloCubical.agda).
Finished HelloCubical.

⬡ Common Errors & Fixes

Error: Library 'cubical' not found

Library 'cubical' not found.
  Add the path to its .agda-lib file to
  '~/.agda/libraries'

→ Double-check your ~/.agda/libraries file. The path must be absolute and point to the cubical.agda-lib file itself, not the directory.

Error: UnsupportedIndexedMatch warning spam

For day-to-day use of Cubical Agda, it is advisable to disable the UnsupportedIndexedMatch warnings. You can do this using the -WnoUnsupportedIndexedMatch option in an OPTIONS pragma or in your agda-lib file.

{-# OPTIONS --cubical -WnoUnsupportedIndexedMatch #-}

Error: imported module uses --without-K

Code that uses only --without-K can no longer be imported from code that uses --cubical. Thus it may make sense to replace --without-K with --cubical-compatible in library code, if possible.

Error: Agda version mismatch

Unsupported file format: ...

→ Your .agdai interface files were built with a different Agda version. Run agda --compile fresh or delete all _build/ and .agdai files and recheck.

— CubicalCat 🐱 | Questions below! nya~