cubical: the standard library for Cubical Agda, and its compatibility matrix

A library for a language still being designed

Cubical is a standard library for Cubical Agda, and the project description calls it experimental. That framing is the first thing to understand about it.

Cubical Agda is a dependently typed programming language with univalence and higher inductive types, implemented by a variation of cubical type theory. The type theory it implements comes from the paper Cubical Type Theory: a constructive interpretation of the univalence axiom by Cohen, Coquand, Huber and Mörtberg. The language itself is described in the paper Cubical Agda: a dependently typed programming language with univalence and higher inductive types by Vezzosi, Mörtberg and Abel.

What the library provides is the layer above the language: the modules, the abstractions and the results that a formalisation needs and that nobody should have to write from scratch. The repository is named after it and the homepage is the rendered documentation, a clickable version of the whole library at agda.github.io/cubical/Cubical.Everything.html.

The audience is therefore people working in the formalisation side of homotopy type theory, in research groups, in summer schools and in graduate courses. The README points at a Discord server shared with agda-unimath and the 1lab, which is the right social context for a library like this: a small group of people who read each other's pull requests.

The licence is listed as a custom one that GitHub cannot classify, with the details in the LICENSE file at the root of the repository.

The version table is the compatibility contract

The single most useful thing in the README is a table, and for a library like this it is more than a convenience.

The README states that the library checks with the Agda version indicated in the table, and that if you want to use a specific release of Agda, the table lists which releases of Agda are known to work with which release of the library, with the note that most likely a lot more combinations work as well.

|-------------------------|--------------------------------|
| current master          | `v2.8.0`                       |
| `v0.9`                  | `v2.8.0`                       |
| `v0.8`                  | `v2.6.4.1` `v2.7.0.1`          |
| `v0.7`                  | `v2.6.4` `v2.6.4.1`            |

The older rows continue in the same style, with v0.6 against v2.6.4, v0.5 against v2.6.3 and v2.6.4, v0.4 against v2.6.2.2, v0.3 against v2.6.2, v0.2 against v2.6.1.3, and v0.1 against v2.6.0.1. The README also notes that the Agda versions in the table correspond to tags, which is what makes the table usable as a checkout instruction rather than a compatibility claim.

The example makes that concrete. If you have Agda 2.6.2.2, you can switch to version 0.4 of the cubical library with:

git checkout v0.4

So the workflow for a newcomer with an older Agda is a checkout rather than a fight with the type checker, and the same table tells a team with a pinned toolchain which library release to vendor.

The decomposition behind higher inductive types

The theoretical background section of the README explains the one design decision that matters most, and it is worth understanding before reading any of the code.

The key difference from the original cubical type theory is that the Kan composition operations are decomposed into homogeneous composition and generalized transport, following the paper On Higher Inductive Types in Cubical Type Theory by Coquand, Huber and Mörtberg. The README states the consequence plainly: this makes it possible to directly represent higher inductive types.

Higher inductive types are the feature that distinguishes cubical type theory from the ordinary dependent type theory in most proof assistants. They let you define a type by naming its constructors and their computation rules, rather than encoding them with an encoding trick that costs you canonicity or the ability to eliminate into the type. A library that supports them directly is what makes the language worth using.

The decomposition is what makes the implementation tractable. Composition in the original formulation is one operation with a complicated computation rule, and higher inductive types want a primitive that behaves like a path between paths. Splitting it into homogeneous composition, which is what a path does, and generalized transport, which is what a higher path does, gives the system two simpler primitives to work with.

The practical consequence for a user of the library is that the modules are organised around this vocabulary, and the names in the code reflect the two operations rather than the one. That is why the rendered documentation is the reference to read, rather than a tutorial.

Learning resources, and the honest note about a dated blog post

The README collects learning resources in one place, and one of them comes with a warning that is worth repeating.

The first entry is introductory course notes from the HoTTest summer school, with literate Agda files and recordings on YouTube. Literate Agda files are the format where the code and the prose are in the same document, so a proof reads as a document rather than as a file with comments, and for a library aimed at teaching, that is the right medium.

The second is a blog post introducing the library on the homotopy type theory blog, and the README says that many files and results have moved since it was written. That is a warning about the whole category. A blog post about a library from 2018 describes a snapshot of a library that has since been reorganised, and following it today means hitting moved modules.

The third resource is the lecture notes for the Cubical Agda course at the EPIT 2021 spring school, which is course notes rather than a tutorial, and is therefore closer to a syllabus of what a student can expect to be able to do.

Taken together the three are a sensible path: the summer school for a guided introduction with recordings, the course notes for the structure of the subject, and the blog post for the idea, with the caveat that the code it points at has moved.

The library's own rendered documentation remains the authority for what exists now, which is the opposite of how a prose tutorial behaves.

Pull request review in a volunteer project with named reviewers

The reviewing section is short and says something useful about how the project is run.

If you switch a draft pull request to ready to merge, or create an open pull request directly, the project should request a review from one of the listed reviewers. If that does not happen, you can request a reviewer yourself so they are aware of the open pull request, and the README suggests using Discord to get in touch with a reviewer if reviewing is taking a very long time.

The reviewer table gives an area of expertise for each person, which is a good way to route a change. Anders Mörtberg and Evan Cavallo cover most topics. Felix Cherubini and Max Zeuner cover algebra related topics. Axel Ljungström covers synthetic homotopy theory and cohomology. Max New covers category theory. Andrea Vezzosi is listed as inactive, and the README links an overview of the current open pull requests sorted by time since the last action, filtered to non-draft ones.

The sorting by last action is a small design choice with a real effect. A review queue ordered by age surfaces the pull requests that have been waiting longest, and a project where the reviewer pool is a handful of busy academics is one where a pull request can otherwise sit unnoticed for months. Asking for a review automatically, rather than hoping, and publishing the queue in a link, is the mechanism that keeps the queue moving.

For a contributor, the practical advice is simple and comes straight from the README: make the pull request non-draft, and if nothing happens, ask someone directly.

The repository is the library, the docs and the release tooling

The top level of the repository shows how much of this project is process rather than mathematics.

There is the Cubical/ directory holding the library itself, and cubical.agda-lib, which is the Agda library file that tells the type checker where the modules and their dependencies live. Alongside them are the files that make the project reproducible: INSTALL.md for the install instructions the README points at, MAKEWINDOWS.md, RELEASE.md for the release process, NAMING.md for the conventions, CONTRIBUTING.md, and CITATION.cff for the citation metadata.

The build tooling is a mix of the two ecosystems that Agda sits in. There is a GNUmakefile and a cabal.project, because Agda itself is written in Haskell and ships with Cabal and a Makefile, and there is also a default.nix, a flake.nix and a flake.lock for the Nix route, which is how most people reproduce an Agda environment today.

Two smaller files are worth noticing. fix-whitespace.yaml is a configuration for a whitespace fixing tool, which tells you that the project cares about a detail that looks trivial until a diff of a large file turns into noise. And generate-everything.sh is the script that produces the rendered documentation, which is how Cubical.Everything.html comes to exist from the literate sources.

The last push to the repository was on 2026-10-08. The release history is v0.7 from 2024-02-12, v0.8 from 2025-05-19 and v0.9 from 2025-07-30, and there is no GitHub release for the master branch, which the compatibility table lists separately as tracking Agda v2.8.0.

Editorial conclusion

cubical suits a researcher or student who wants to work in cubical type theory rather than only read about it, and it suits a team that has to pin a language version, because the compatibility table makes the choice of library release explicit instead of a matter of guesswork. It does not suit a production project, since the library is described as experimental, the language it supports is itself a research vehicle. Check three things before you commit: which Agda version you are on and which library release matches it, whether the abstractions you need are in the current release or still moving between modules, and how you will track upstream when the master branch is ahead of any tag. The last push to the repository was on 2026-10-08, the newest release is v0.9 from 2025-07-30, and the documentation lives in the rendered Cubical.Everything page rather than in the README.

Frequently asked questions

Official sources

1. agda/cubical on GitHub
2. Issues
3. Project website
4. README
5. Releases