The encode-decode method, relationally

James McKinna, Fredrik Nordvall Forsberg

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


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
Number of pages2
ISBN (Electronic)9789949430871
ISBN (Print)9789949430864
Publication statusPublished - 2015


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

Cite this