@inproceedings{sterling-2019-cubical,
  doi = {10.4230/LIPICS.FSCD.2019.31},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.31},
  author = {Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel},
  keywords = {Dependent type theory, extensional equality, cubical type theory, categorical gluing, canonicity, Theory of computation → Type theory, Theory of computation → Algebraic semantics, Theory of computation → Denotational semantics},
  language = {en},
  title = {Cubical Syntax for Reflection-Free Extensional Equality},
  volume = {131},
  pages = {31:1-31:25},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2019},
  copyright = {Creative Commons Attribution 3.0 Unported license},
  booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}
}