Bicubical Directed Type Theory

by Matthew Weaver (PhD Thesis)

  thesis.pdf    -- copy of thesis

...along with...

A Model of Type Theory with Directed Univalence in Bicubical Sets

by Matthew Z. Weaver and Daniel R. Licata

The code in this repository includes formalizations corresponding to the above, as well as some other, related material:

  agda/directed/ -- Agda formalization
                    (compile All.agda to check everything)

The formalization also includes that from the following paper.

Cartesian Cubical Type Theory

by Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, Daniel R. Licata

  agda/ -- full Agda formalization
           (compile ABCFHL.agda to check everything)

The formalizations were checked by Agda 2.6.1.2, which includes the 'flat' modality that was previously in a special agda-flat branch.

NOTE: This is a static copy of the following repository: https://github.com/dlicata335/cart-cube.