From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-io1-xd3d.google.com (mail-io1-xd3d.google.com [IPv6:2607:f8b0:4864:20::d3d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 78fa33f6 for ; Mon, 27 Jan 2020 18:18:16 +0000 (UTC) Received: by mail-io1-xd3d.google.com with SMTP id 13sf6669851iof.14 for ; Mon, 27 Jan 2020 10:18:15 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1580149095; cv=pass; d=google.com; s=arc-20160816; b=Z6+stizrXNrwlUv3eh9F98RrmsNBALcbfu22Z5Ce7yj3PPiw3rxQ/Rp3fjJvQJXIKW CrjEhBboRwa89hj5QKqfd516MtQXLCNBFHhLn8rD5SHt6yZ8N/hFwjIm/ObnwgF0ZFBE yE4blLGwHrSG5c642f+xNjUY5v8zMsqILV8csVaF6RPk33FIa+7F8pdfjl6134hWp1nt U/sXobgWHPDYFR8Vdd+oBlUq6JXsSjuoIvG9FB55hYQS5Kx9t7HjAKH79rJzmyFpZyPE TPeYZ/Xw3v4gurBctSfEZkLHf9FxBq2PmPAvzHdU8lSqL3N5hLlHW5Q/LkzX0qSWW+8t KUIw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=3abpcQdLgArnEiMm1EKSqml4hnnJFRnwc6cGNhxi8qc=; b=ooKUD6/jjhgWf1W36jxXztzP8OP1kuh9tAdZsLWeJlXkMaPQmox9U8QF4hPe1Gkjz1 2eLWjmEyhnjDNRQlRvoJ/lRbTPEXFisVFu1yGRudsbgjrxuUr+svjXOyuLOVLx63AUZ8 n9+ea0bwQYuSWJB+tXorHXPrnGsWAib/Jo8oS2i3gT3XHCwBSJx6HR9UwRsZhV5BzqlB EGxKZoGHqd+BKGGVFEbwORAaTLPGCmchG0wdCmwVPNB+L10vXB5BVnzT+wl7MN8re1dS 22ure6E0DqwiPGUtjOKh6Ys0i30HpSVKmEhzB8vGzW5AUd3qBoF2eJxHeBtiybJCdBWO 2wRQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=GDO8ZuKX; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2607:f8b0:4864:20::333 as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=3abpcQdLgArnEiMm1EKSqml4hnnJFRnwc6cGNhxi8qc=; b=hOLByfVrF2wkpBwhiKLVxXQXbGElicGABHOegaz2wbGU9MsK93yleNyPXmLHJfuvUk 0wpNcZ1PGa3gatA0q1XDac69yexn+SQ8huAnS3/NVsWSoemkvqGrj3h/cT+FCxeVbE4W CCN9bWb+37w6Ztjlxt8Zf0O0v8Mbf4u9vvoGCtESGTik078YIQ/keFdELLFEpjuvqju6 xKHqW5xz77GfS82SDz+lQ4yP0sw0B6J/6uKfmBIX3BZiUEXkVuZPg01fdO/1M9m80UV1 e7aQQwsxKf77FxAqaOX5mxwCVBLiKj2hn5GyFA7O93xhTuwbCgSQskOzqwqnXUWiC4Vj uWDQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=3abpcQdLgArnEiMm1EKSqml4hnnJFRnwc6cGNhxi8qc=; b=EqLqdZp7ay+5QVtXY6tIRwZAWSUeO+OTz+74ccTmCd25pf3SN8b7CME0RIc3oHKBgU DFAHZ2SdQf7HdFZEbvjleMXQQrzWdpl8i7H0aqYidoSihmj4y7euS1JlXdFhyo8Nz+kJ vD7IBNasQIeiKgBwkhu2xNjTn79Eg2jXOKy5P+OTbd/cOScOXZg1XgSQv48R7RpBxu8L w0uvicSpBZg0jIaRrtezDJGPJKWk8T2V0WKtbcj3UlQ06iS/AeCGS/lOvdN/4dV9vEZa Y9R5/5JJtiWrbgJqHpwCICcH1KzAgwS/S/90k1kk3RBXNytj36VAX9uO1myx0TIte1D/ N8QQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=3abpcQdLgArnEiMm1EKSqml4hnnJFRnwc6cGNhxi8qc=; b=nGdzFVXkGx0eFjqwm7Fc0WfzXKsOJPHnBeOlJE6wad4FrokcAHerrQA7w5GwWXz4Oa JvMEOAtT6ejbMk0YmHPZ90EFDikVFFoewbhVArYcM/luY4G6mqG5tHDGjEEEzqolg2xG xtp+0bJx9nk3qP5RScrx1QRImI5tGo/L1gF/BanLAOtUeKGBN2puniTxtm8OaqmIdatU rTVIT0mlkLI9EEA5yzK/1DRM76STxS6nxZWZy8jnFAZ3cs0kq5asHi+2nQ52TjtPBqug iM6dz7fbMbgS+RdMSF1O950oZVAH7CRzgbd0hCSLihW+NGhlGD93ntfNpIz+3Ma+qFNo nhcw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVVO7v3y2U+ERgkyYZvdqF2zeujBTf5iJtm95DmFjVuoMG5ka2T 6vLqA/jh4jT6R6BqoAN5yY8= X-Google-Smtp-Source: APXvYqyMIUTYlTx+ywbw/GBcgYsw7fC8bbMSdKnc+KrsJNfAV2jIEcNOSV55DJoksotk2Bp3ZSeGLg== X-Received: by 2002:a92:485a:: with SMTP id v87mr15870002ila.128.1580149094196; Mon, 27 Jan 2020 10:18:14 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a92:db04:: with SMTP id b4ls2195933iln.5.gmail; Mon, 27 Jan 2020 10:18:13 -0800 (PST) X-Received: by 2002:a92:5ad7:: with SMTP id b84mr4635432ilg.105.1580149093236; Mon, 27 Jan 2020 10:18:13 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1580149093; cv=none; d=google.com; s=arc-20160816; b=0TCCbI/iwiBIAJ8W9aC+fnaK73nKJ0hklDUZagwbu6XybukPKSIasEdPPsph8fvfIl JtcvlU3fqBq2OcENuSx+/qKWpGtff952EXwuwGDySx5KLYmDniBNX0eNpv2fo9wUOwzc mmxswRTNLmRrBeiPzkL0VElC/lKzt+IHzPvAMBnUcKF03Jh/uutd84Xo2lfGmjUkeis+ ZDq3lJ6mfZKX7R1CjmvIZ7fZEO+DM6uUHKKT5bNjD8HY2e/sPkqS1LeyDdOi7TllG8gr CvCS3tceG4IubUOWtg/l7e35VebqxjtYpHZSX8Y4K8s331331XGSBI/ZafOTwSyD28O/ uO9w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=mFpTUuG5PIitPhg1qIob/Vgzb75tRRZPoU3kYt8+45o=; b=1AMsVCvyUmop/qOeopG0VTDPDTXByEj6bDvJbHJgAsvz1nAnNTPdjh8e+tBOp+3FzS 4BgtISH5nR0Mq3UVAf+TlZKxNmk51E8Yz596YP/AJO/UJGOMIQ0JAaZSibU98nIYllNO RrhstAoCt9dAjPMc6UKMAtF+cwpoRVIv5yKLrtMc+82gc5QqU14pcBd2jBc/ShU63oop CeNFQzu35LbVCzkqJ1+Z2RSJyb9XOQruNtqf7FUrFPVbKjCp6gzmLXXKrm2MFtXuTe2P hkBeKeFa9GgqxKaTUMSD6iB8agapB711kfPINiFgtSNN8chK+Ym2bHTSNSxnNMF1Vc76 wOTQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=GDO8ZuKX; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2607:f8b0:4864:20::333 as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ot1-x333.google.com (mail-ot1-x333.google.com. [2607:f8b0:4864:20::333]) by gmr-mx.google.com with ESMTPS id h4si833744ilf.3.2020.01.27.10.18.13 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 27 Jan 2020 10:18:13 -0800 (PST) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2607:f8b0:4864:20::333 as permitted sender) client-ip=2607:f8b0:4864:20::333; Received: by mail-ot1-x333.google.com with SMTP id h9so9311116otj.11 for ; Mon, 27 Jan 2020 10:18:13 -0800 (PST) X-Received: by 2002:a05:6830:11:: with SMTP id c17mr2960210otp.360.1580149092683; Mon, 27 Jan 2020 10:18:12 -0800 (PST) MIME-Version: 1.0 From: Nicolai Kraus Date: Mon, 27 Jan 2020 18:18:01 +0000 Message-ID: Subject: [HoTT] Coherence via Wellfoundedness To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000005c93b9059d232185" X-Original-Sender: nicolai.kraus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=GDO8ZuKX; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2607:f8b0:4864:20::333 as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --0000000000005c93b9059d232185 Content-Type: text/plain; charset="UTF-8" Hello all, 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 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 -- 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. --0000000000005c93b9059d232185 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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=

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