Repository files navigation

The source code has a glorious clickablerendered version.

There is also adiscord server, shared withagda-unimath and the1lab.

This library checks withAgda version indicated in the table below.For detailed install instructions see theINSTALLfile.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.

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

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

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

• For some introductory lecture notes see the material for the Cubical Agda courseof theEPIT 2021 spring school.

For a paper with details about Cubical Agda, seeCubical Agda: a dependently typedprogramming language with univalence and higher inductivetypes by Andrea Vezzosi, AndersMörtberg, and Andreas Abel.

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

Cubical Type Theory: a constructive interpretation of the univalenceaxiom - Cyril Cohen, ThierryCoquand, Simon Huber, Anders Mörtberg.

The key difference is that the Kan composition operations aredecomposed into homogeneous composition and generalized transport asin:

On Higher Inductive Types in Cubical TypeTheory - Thierry Coquand, SimonHuber, Anders Mörtberg.

This makes it possible to directly represent higher inductive types.

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.

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