KIT | KIT-Bibliothek | Impressum | Datenschutz

A rewriting coherence theorem with applications in homotopy type theory

Kraus, Nicolai; von Raumer, Jakob 1
1 Institut für Programmstrukturen und Datenorganisation (IPD), Karlsruher Institut für Technologie (KIT)

Abstract:

Higher-dimensional rewriting systems are tools to analyse the structure of formally reducing terms to normal forms, as well as comparing the different reduction paths that lead to those normal forms. This higher structure can be captured by finding a homotopy basis for the rewriting system. We show that the basic notions of confluence and wellfoundedness are sufficient to recursively build such a homotopy basis, with a construction reminiscent of an argument by Craig C. Squier. We then go on to translate this construction to the setting of homotopy type theory, where managing equalities between paths is important in order to construct functions which are coherent with respect to higher dimensions. Eventually, we apply the result to approximate a series of open questions in homotopy type theory, such as the characterisation of the homotopy groups of the free group on a set and the pushout of 1-types. This paper expands on our previous conference contribution Coherence via Wellfoundedness by laying out the construction in the language of higher-dimensional rewriting.


Verlagsausgabe §
DOI: 10.5445/IR/1000156291
Veröffentlicht am 27.02.2023
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
KIT-Bibliothek (BIB)
Publikationstyp Zeitschriftenaufsatz
Publikationsjahr 2023
Sprache Englisch
Identifikator ISSN: 0960-1295, 1469-8072
KITopen-ID: 1000156291
Erschienen in Mathematical Structures in Computer Science
Verlag Cambridge University Press (CUP)
Band 32
Heft 7
Seiten 982–1014
Vorab online veröffentlicht am 06.02.2023
Schlagwörter Homotopy type theory, higher-dimensional rewriting, constructive mathematics, coherence of structure, wellfounded relation, confluence, Squier theory, abstract rewriting system, polygraph
Nachgewiesen in Web of Science
Scopus
Dimensions
Relationen in KITopen
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page