@inproceedings{angiuli-2018-cartesian,
  doi = {10.4230/LIPICS.CSL.2018.6},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.6},
  author = {Angiuli, Carlo and Hou (Favonia), Kuen-Bang and Harper, Robert},
  keywords = {Homotopy Type Theory, Two-Level Type Theory, Computational Type Theory, Cubical Sets},
  language = {en},
  title = {Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities},
  volume = {119},
  pages = {6:1-6:17},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2018},
  copyright = {Creative Commons Attribution 3.0 Unported license},
  booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)}
}