Hello all,

-- The results which I've t=
alked 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:**

Co= nsider paths in a given graph. If we want to prove a certain property for a= ll paths, the obvious approach is to try induction on [the length of] a pat= h. If we want to prove a certain property for all *closed* paths (first ver= tex =3D last vertex), this does not work since closed paths are not inducti= vely generated (if we remove an edge from a closed path, it is not closed a= ny more).

We have studied this situation because certain coherence p= roperties 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-t= ype B, a function from the set-truncated quotient A/< to B is given by:<= br>=C2=A0 (1) =C2=A0f : A -> B

=C2=A0 (2) =C2=A0h : Pi(x,y:A). x<y= -> f(x) =3D f(y)

=C2=A0 (3) =C2=A0c : 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 th= ose 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 t= he problem explained in the first paragraph, although we know that (3) can&= #39;t be false. Not yet quite an instance, but close to being one, is the s= ituation Mike described with "the [...] universe certainly is fully co= herent" 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 con= structive sense: every span can be completed to the obvious shape);

Sec= ond, it is (co-) well-founded.

(These assumptions are natural if the re= lation 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-z= ag generated by a span with local confluence. And that is possible (and fai= rly easy), simply because we know how the "confluence zig-zags" w= ill look like.

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

As always, any comments are welcome!

Nicolai=

https://arxiv.org/abs/2001.07655

Co= nsider paths in a given graph. If we want to prove a certain property for a= ll paths, the obvious approach is to try induction on [the length of] a pat= h. If we want to prove a certain property for all *closed* paths (first ver= tex =3D last vertex), this does not work since closed paths are not inducti= vely generated (if we remove an edge from a closed path, it is not closed a= ny more).

We have studied this situation because certain coherence p= roperties 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-t= ype B, a function from the set-truncated quotient A/< to B is given by:<= br>=C2=A0 (1) =C2=A0f : A -> B

=C2=A0 (2) =C2=A0h : Pi(x,y:A). x<y= -> f(x) =3D f(y)

=C2=A0 (3) =C2=A0c : 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 th= ose 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 t= he problem explained in the first paragraph, although we know that (3) can&= #39;t be false. Not yet quite an instance, but close to being one, is the s= ituation Mike described with "the [...] universe certainly is fully co= herent" 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 con= structive sense: every span can be completed to the obvious shape);

Sec= ond, it is (co-) well-founded.

(These assumptions are natural if the re= lation 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-z= ag generated by a span with local confluence. And that is possible (and fai= rly easy), simply because we know how the "confluence zig-zags" w= ill look like.

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

As always, any comments are welcome!

Nicolai=

You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.

To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.

To view this discussion on the web visit https:/= /groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBokxk5mHf%2BuQ0OeEbLE= m0Xuk1WKiFK77mxnBbcp_FBX4A%40mail.gmail.com.

--0000000000005c93b9059d232185--