Towards a cubical type theory without an interval
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 of equality is encoded as a term in a context ext...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Published: |
Dagstuhl Publishing
2017
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/44008/ |