Skip to main content

Research Repository

Advanced Search

Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory

Kraus, Nicolai; Von Raumer, Jakob

Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory Thumbnail


Authors

Jakob Von Raumer



Abstract

Suppose we are given a graph and want to show a property for all its cycles (closed chains). Induction on the length of cycles does not work since sub-chains of a cycle are not necessarily closed. This paper derives a principle reminiscent of induction for cycles for the case that the graph is given as the symmetric closure of a locally confluent and (co-)well-founded relation. We show that, assuming the property in question is sufficiently nice, it is enough to prove it for the empty cycle and for cycles given by local confluence. Our motivation and application is in the field of homotopy type theory, which allows us to work with the higher-dimensional structures that appear in homotopy theory and in higher category theory, making coherence a central issue. This is in particular true for quotienting- A natural operation which gives a new type for any binary relation on a type and, in order to be well-behaved, cuts off higher structure (set-truncates). The latter makes it hard to characterise the type of maps from a quotient into a higher type, and several open problems stem from this difficulty. We prove our theorem on cycles in a type-theoretic setting and use it to show coherence conditions necessary to eliminate from set-quotients into 1-types, deriving approximations to open problems on free groups and pushouts. We have formalised the main result in the proof assistant Lean.

Citation

Kraus, N., & Von Raumer, J. (2020). Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory. In LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (662-675). https://doi.org/10.1145/3373718.3394800

Conference Name ACM International Conference Proceeding Series
Conference Location Saarbrücken Germany (held online)
Start Date Jun 8, 2020
End Date Jun 11, 2020
Acceptance Date Mar 18, 2020
Online Publication Date May 25, 2020
Publication Date Jul 8, 2020
Deposit Date Jul 15, 2020
Publicly Available Date Mar 28, 2024
Publisher Association for Computing Machinery (ACM)
Pages 662-675
Book Title LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science
ISBN 9781450371049
DOI https://doi.org/10.1145/3373718.3394800
Public URL https://nottingham-repository.worktribe.com/output/4576923
Publisher URL https://dl.acm.org/doi/10.1145/3373718.3394800

Files




You might also like



Downloadable Citations