Skip to main content

Research Repository

Advanced Search

A rewriting coherence theorem with applications in homotopy type theory

Kraus, Nicolai; von Raumer, Jakob

A rewriting coherence theorem with applications in homotopy type theory Thumbnail


Authors

Jakob von Raumer



Contributors

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.

Citation

Kraus, N., & von Raumer, J. (2022). A rewriting coherence theorem with applications in homotopy type theory. Mathematical Structures in Computer Science, 32(7), 982-1014. https://doi.org/10.1017/s0960129523000026

Journal Article Type Article
Acceptance Date Jan 6, 2023
Online Publication Date Feb 6, 2023
Publication Date 2022-08
Deposit Date Mar 23, 2023
Publicly Available Date Mar 29, 2024
Journal Mathematical Structures in Computer Science
Print ISSN 0960-1295
Electronic ISSN 1469-8072
Publisher Cambridge University Press (CUP)
Peer Reviewed Peer Reviewed
Volume 32
Issue 7
Pages 982-1014
DOI https://doi.org/10.1017/s0960129523000026
Keywords Homotopy type theory; higher-dimensional rewriting; constructive mathematics; coherence of structure; well- founded relation; confluence; Squier theory; abstract rewriting system; polygraph
Public URL https://nottingham-repository.worktribe.com/output/18814063
Publisher URL https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/on-reduction-and-normalization-in-the-computational-core/14DE21ED5F5B6A62EDD17E210D3A41C5

Files




You might also like



Downloadable Citations