Skip to content

martinescardo/cubical

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

An experimental 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.

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.

The library is divided into:

  • Cubical/Core: minimal core library to get Cubical Agda up and running.

  • Cubical/Basics: basic theory (natural numbers, integers, basic results about equivalences...). This folder does not contain any HITs.

  • Cubical/HITs: various higher inductive types and results about them.

For an introduction to Cubical Agda and this library see this blog post.

Maintainers

Build Status

About

No description, website, or topics provided.

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Agda 99.9%
  • Makefile 0.1%