Skip to content

mzeuner/cubical

This branch is 20 commits ahead of, 916 commits behind agda/cubical:master.

Folders and files

NameName
Last commit message
Last commit date

Latest commit

d85523f · Dec 17, 2021
Jun 23, 2021
Dec 17, 2021
Apr 16, 2020
Dec 16, 2021
Aug 14, 2021
Nov 22, 2021
Oct 13, 2020
Aug 1, 2019
Dec 16, 2021
Jul 29, 2021
Apr 22, 2021
Jul 29, 2021
May 29, 2020

Repository files navigation

A standard library for Cubical Agda

This library compiles with the master branch of the development version of Agda. For detailed install instructions see the INSTALL file.

If you want to use Agda 2.6.2 instead of the latest development version, you can check out the tag v0.3 of this library.

If you want to use Agda 2.6.1.3 instead of the latest development version, you can check out the tag v0.2 of this library.

If you want to use Agda 2.6.0.1 instead of the latest development version, you can check out the tag v0.1 of this library.

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

For a paper on with detials 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.

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

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.

Maintainers

Build Status

Gitter

About

No description, website, or topics provided.

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Agda 99.9%
  • Other 0.1%