Altenkirch, T., & Kaposi, A. (2018). Towards a cubical type theory without an interval. LIPIcs, 3:1-3:27. https://doi.org/10.4230/LIPIcs.TYPES.2015.3