awswan/cubical

An experimental library for Cubical Agda

A standard library for Cubical Agda

The source code has a glorious clickable rendered version.

There is also a discord server, shared with agda-unimath and the 1lab.

Compiling, using and installing

This library checks with Agda version indicated in the table below. For detailed install instructions see the INSTALL file. 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 v2.6.4.1 v2.6.4.3
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

git checkout v0.4

Learning materials

• Introductory material from the HoTTest summer school: literate agda files recordings on youtube

• For an introduction to this library, see this blog post. Note that many files and results have moved since this blog post was written.

• For some introductory lecture notes see the material for the Cubical Agda course of the EPIT 2021 spring school.

Theoretical background

For a paper with details about Cubical Agda, see Cubical Agda: a dependently typed programming language with univalence and higher inductive types by Andrea Vezzosi, Anders Mörtberg, and Andreas Abel.

The type theory that Cubical Agda implements is a variation of the cubical type theory of:

Cubical Type Theory: a constructive interpretation of the univalence axiom - Cyril Cohen, Thierry Coquand, Simon Huber, Anders Mörtberg.

The key difference is that the Kan composition operations are decomposed into homogeneous composition and generalized transport as in:

On Higher Inductive Types in Cubical Type Theory - Thierry Coquand, Simon Huber, Anders Mörtberg.

This makes it possible to directly represent higher inductive types.

Reviewing of pull requests

If you switch your draft pull request (PR) to 'ready to merge', or directly create an open PR, we should request a review, by one of the reviewers below. If that doesn't happen, you can also request a reviewer yourself (for reviewer expertise see below), to make us aware of the open PR. Feel free to use Discord to get in touch with a reviewer in case reviewing is taking a very long time.

Reviewer	github handle	Area of expertise	Queue
Anders Mörtberg	mortberg	Most topics	link
Evan Cavallo	ecavallo	Most topics	link
Felix Cherubini	felixwellen	Mainly algebra related topics	link
Max Zeuner	mzeuner	Algebra related topics	link
Axel Ljungström	aljungstrom	Synthetic homotopy theory and cohomology	link
Andrea Vezzosi	Saizan	Inactive	link

Overview of the current open PRs, descending time since last action.