The encode-decode method, relationally

James McKinna, Fredrik Nordvall Forsberg

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationAbstracts of the 21st International Conference on Types for Proofs and Programs, TYPES 2015
PublisherInstitute of Cybernetics at Tallinn University of Technology
Pages63-64
Number of pages2
ISBN (Electronic)9789949430871
ISBN (Print)9789949430864
Publication statusPublished - 2015

Fingerprint Dive into the research topics of 'The encode-decode method, relationally'. Together they form a unique fingerprint.

  • Cite this

    McKinna, J., & Forsberg, F. N. (2015). The encode-decode method, relationally. In Abstracts of the 21st International Conference on Types for Proofs and Programs, TYPES 2015 (pp. 63-64). Institute of Cybernetics at Tallinn University of Technology.