Towards a cubical type theory without an interval
(2018)
Journal Article
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
Following the cubical set model of type theory which validates the univalence axiom, cubical type theories have been developed that interpret the identity type using an interval pretype. These theories start from a geometric view of equality. A proof... Read More about Towards a cubical type theory without an interval.