Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Nicolai Kraus <nicolai.kraus@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: [HoTT] Coherence via Wellfoundedness
Date: Mon, 27 Jan 2020 18:18:01 +0000	[thread overview]
Message-ID: <CA+AZBBokxk5mHf+uQ0OeEbLEm0Xuk1WKiFK77mxnBbcp_FBX4A@mail.gmail.com> (raw)

[-- Attachment #1: Type: text/plain, Size: 3131 bytes --]

Hello all,

The results which I've talked about in Herrsching in December are now on
the arXiv:

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

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
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!

You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBokxk5mHf%2BuQ0OeEbLEm0Xuk1WKiFK77mxnBbcp_FBX4A%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 3762 bytes --]

                 reply	other threads:[~2020-01-27 18:18 UTC|newest]

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=CA+AZBBokxk5mHf+uQ0OeEbLEm0Xuk1WKiFK77mxnBbcp_FBX4A@mail.gmail.com \
    --to=nicolai.kraus@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \


* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).