[DBLP:conf/lics/KrausR20]  Nicolai Kraus, Jakob von Raumer, Coherence via WellFoundedness: Taming SetQuotients in Homotopy Type
Theory, Holger Hermanns and
Lijun Zhang and
Naoki Kobayashi and
Dale Miller (Ed.), LICS '20: 35th Annual {ACM/IEEE} Symposium on Logic in Computer
Science, Saarbr{\"U}cken, Germany, July 811, 2020, pp. 662675, ACM, 2020.

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 subchains 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)wellfounded 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 higherdimensional 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 wellbehaved, cuts off higher structure (settruncates). 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 typetheoretic setting and use it to show coherence conditions necessary to eliminate from setquotients into 1types, deriving approximations to open problems on free groups and pushouts. We have formalised the main result in the proof assistant Lean.
Download
BibTeX
Authors at the institute