The results which I've talked about in Herrsching in December are now on the arXiv:
https://arxiv.org/abs/2001.07655

In this work, Jakob von Raumer and I address the following problem:
Consider paths in a given graph. If we want to prove a certain property for all paths, the obvious approach is to try induction on [the length of] a path. If we want to prove a certain property for all *closed* paths (first vertex = last vertex), this does not work since closed paths are not inductively generated (if we remove an edge from a closed path, it is not closed any more).

We have studied this situation because certain coherence properties in HoTT can be formulated in terms of cycles. Our primary example is the following. Let's say we have a type A and a family (<) : A -> A -> Type (a "binary proof-relevant relation"). For a 1-type B, a function from the set-truncated quotient A/< to B is given by:
  (1)  f : A -> B
  (2)  h : Pi(x,y:A). x<y -> f(x) = f(y)
  (3)  c : the property that h maps every closed zig-zag in A to reflexivity in B.
(A closed zig-zag is a closed path in the graph generated by the symmetric closure of <).

In those examples that we were interested in, we found that property (3) is very difficult to check (or we simply didn't manage to at all) because of the problem explained in the first paragraph, although we know that (3) can't be false. Not yet quite an instance, but close to being one, is the situation Mike described with "the [...] universe certainly is fully coherent" in
https://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/

Our paper builds on the observation that, at least in all those cases we were interested in, the relation < has additional and so far unused properties:
First, it is locally confluent (in the constructive sense: every span can be completed to the obvious shape);
Second, it is (co-) well-founded.
(These assumptions are natural if the relation is encoding some reduction.)
We construct a new relation on the type of closed zig-zags with the property that this new relation is again (co-) well-founded. The consequence is, in a nutshell, that every closed zig-zag can be expressed as a combination of shapes given by local confluence.

The application is this: If we want to prove a property such as (3), for all closed zig-zags, it is enough to check the property for the zig-zag generated by a span with local confluence. And that is possible (and fairly easy), simply because we know how the "confluence zig-zags" will look like.

An application-of-the-application is the statement that the fundamental groups of the free higher group over a set are trivial, and related results.

As always, any comments are welcome!
Nicolai