# Cartesian Cubical Type Theory 
by Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, 
Kuen-Bang Hou (Favonia), Robert Harper, Daniel R. Licata
```

  cart-cube.pdf    -- current version of paper
  cart-cube-v2.pdf -- second version paper
                      (lacking some presentational improvements)
  cart-cube-v1.pdf -- orignal version of paper
                      (with a different composition for Glue types)
```

The formalization that corresponds exactly to the paper is
[browsable](http://dlicata.wescreates.wesleyan.edu/pubs/abcfhl/agda/ABCFHL-MSCS.html) and
[downloadable](https://dlicata.wescreates.wesleyan.edu/pubs/abcfhl/abcfhl.tar.gz).
  
The code in this repository includes that, as well as some other, related material:
```
  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.

# A Model of Type Theory with Directed Univalence in Bicubical Sets
by Matthew Z. Weaver and Daniel R. Licata

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