Abstract
In Homotopy Type Theory (HoTT), the 'encode-decode' method makes heavy use of explicit recursion over higher inductive types to construct, and prove properties of, homotopy equivalences. We argue for the classical separation between specification and implementation, and hence for using relations to track the graphs of encode/decode functions. Our aim is to isolate the technicalities of their definitions, arising from higher path constructors, from their properties. We describe our technique in the calculation of 1(S1), and comment on its applicability in the current Agda implementation of HoTT.
| Original language | English |
|---|---|
| Title of host publication | Abstracts of the 21st International Conference on Types for Proofs and Programs, TYPES 2015 |
| Publisher | Institute of Cybernetics at Tallinn University of Technology |
| Pages | 63-64 |
| Number of pages | 2 |
| ISBN (Electronic) | 9789949430871 |
| ISBN (Print) | 9789949430864 |
| Publication status | Published - 2015 |