Cartesian Cubical Type Theory, by Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Kuen-Bang Hou (Favonia), Robert Harper, Daniel R. Licata
cart-cube.pdf -- draft paper
agda/ -- Agda formalization of the model, using the internal language
technique developed by Orton and Pitts. This was developed
using a development version of Agda, so if you experience
problems checking it with the current release, let us know.
Everything.agda has a suggested reading order.