From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,MAILING_LIST_MULTI,NICE_REPLY_A, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 25911 invoked from network); 8 Mar 2021 16:27:29 -0000 Received: from mail-lj1-x23e.google.com (2a00:1450:4864:20::23e) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 16:27:29 -0000 Received: by mail-lj1-x23e.google.com with SMTP id d16sf4603753lja.12 for ; Mon, 08 Mar 2021 08:27:29 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615220848; cv=pass; d=google.com; s=arc-20160816; b=MPhqHANhyQ5YT7m2KHAqawY62bN/Mgz5YeEk0nIUPwEf+ChoTTuXMQFB2Z0IH2GAWu Lktyq1W/6fi8nofIDtBTw2+DFsOQx8TbVKfLaXfZH3PLtDDccUSfytOBxuZf4D9c8adF ueIRYb2oyu2JRBvTsDL17SE0VW0EPsSO7R8YbMyuTrQ74S6Y1is2Icg2Mg1evmah+JEW fExh7Tvcq8EtKsm1edgQd9T0P11TbvkhkegskCNGKNrfRCHmwKfuSA5k3M6go0mt71EN YuyuTOg7PZG8A8Y++zBQrcTxsmxNmNrO4mfJ1kH60GyJvx3JFrJG0WIgIWCzKWmJZCa4 IQTw== 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:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject:sender :dkim-signature:dkim-signature; bh=dLnjWtTzDp3rj6lZMrZIpTL40hfqyZDcUM9zZf7/3L0=; b=NOaFwl1DFXVBtlMGImdHaI4SvT5mMMaoUXx18/ynQpgKQru+c7XklrpZrePU+oIlRC knp8inxDugzqMy5ImXvQpqBxoWHWv4eqZKo39u74z+0QvztchuM8YiYGTsxkzgVlbETW YBIVKpvRu1kuV+wdxzv6nM5ryFakzR3DslkXWrbpVEEEwQt1s32BnGwujJSI7Rlp56wk h6m+aCphWKu/fH6Fi3IgYwKw+bBl+jerCGpiOej7TaftAPZhm9tmKJoc7VLxrHTk4CPA O90jw691mR5F1Kb6w2iOfcUPWRn0uzHkkz7H7xkW9yZIRj2gylwR1AbQ06JsFTkZNEf7 XIZg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=t6XjS0XZ; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::32b as permitted sender) smtp.mailfrom=sojakova.kristina@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:subject:to:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=dLnjWtTzDp3rj6lZMrZIpTL40hfqyZDcUM9zZf7/3L0=; b=ZT0HC0LEt/L/KJZQfxQqeAWAF0aD2mhfiB2pkFEm4VwCcFpN4kob2VFx6r8VLa/cwC il1d5NAXgkKb8uanh9YQ8ILzRiNPYafS9NsPmWd6ZWH7bztH/9CwgU3cmhYtAIXhesHe 94iJ+NsQakChZvHUqbezU4i3U+ovY9v8AaK1vwWPsc77rFxiUGSGkibgwvfdFGanSI5Z pzdltXpRQM7JyURihMWpdI+BYGMJg1g1zrClPXJQFwujZrHiRMQVXxOo5T/7jQAs+KhA qcNklfMSwtAwD2aMQg118gYLXfDiJUS6wH1nYtZpqcEWOKSAd816NY8uoUlzTfV8BRKE hIZQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=dLnjWtTzDp3rj6lZMrZIpTL40hfqyZDcUM9zZf7/3L0=; b=Q1Oi8vViG6X0/T7DuwZMDajyzM1lvwmpSMiKnqJ49kDPFf8mL/NNSj7sHIGKnd6yzR q3LHvaP/cfZfuT0TgjuOkrhzIGsl8DaX0qku5kw3ifWKrknhrwXght3Dn6Z0HDRsTw7u JAZfv15xeK25l3tkgjh7cdkCJ+bpeeDiPy/jpHUVT4I5thlVohxDmT/TRVhkB1L0I/EF fFGBA4uUA+BMwRzr9eyObdHuNJT7bQjKSV9d0i08o4o0xaeXqPRENH0Heqwm3TjNehTH SY7owPaqCGpbq6odndzYIugc6R/ue1GmdaLnoqW5xvlX6i+G+0324XhcKWBh+bDAFpaf 0JeQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-language :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=dLnjWtTzDp3rj6lZMrZIpTL40hfqyZDcUM9zZf7/3L0=; b=XqW3Er5AMDFZItbmYXZFDdRdNd7KJoUbosU4iDcG1t+jOc386a9W3jN76VZ/GleSGL RCrbRCuS9e1hEjfh59ZWa0k5cCYM37Z7nzHrQOyvoguVmz6lgXoZu0XJZnpSaiV/PpKz NaBpF1fBqjF8suzDOhnLIrw4jxGDZakRTTljGzFigJhcTkFWxh4l2/EG8mo9d5LTkHGY dx0PcZtXDLCG6JJfJVkbDsdWgUmEd+GK15Rs0hzirzC/o9SxoxivKdvcIunkXjgoBSkZ /pOm3POoGPQUVZuguRHGI8ri+LAhu2XDkwK8/7E721+77PGCm369sRprLJl9gzyghGi5 7WSw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM532boRshnK1xaOFq3T5mwOCo6BzpMlyifMm9RW/576BMmUhYs9OF uoAiRy38xxOxGgi4YQ/vJ/Q= X-Google-Smtp-Source: ABdhPJzwJv3a5Z3XZe/0dmAU96cD7D6rgl7XBXLSTbamrCRZHUwd2XcMkr7LkAWI0sZlulRBvNa6QA== X-Received: by 2002:a2e:95d6:: with SMTP id y22mr11776679ljh.361.1615220847789; Mon, 08 Mar 2021 08:27:27 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:391a:: with SMTP id g26ls3578357lja.4.gmail; Mon, 08 Mar 2021 08:27:26 -0800 (PST) X-Received: by 2002:a2e:720c:: with SMTP id n12mr14424305ljc.67.1615220846594; Mon, 08 Mar 2021 08:27:26 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615220846; cv=none; d=google.com; s=arc-20160816; b=0D02XqmFqAxSTvV25dC8cgNu1dNs8HxepW2kkC6lwv1FbzZvm3/HnEG+V0maMMvEcq 3PfzjIQNq0ixPk3yVfxxVkdbakToaXdQSMA9ytvzq8sQD9dGs5S52L8pe4v0He9hONGC nNCsD8f4hLNu+QNVBe+BE923oMFzEJGZMBLhNUXyHJpVURpbWaRigiPskS4/kgicLlRK +xXxHfpWV23h2/OwUCjrLKRyvq8mOrNiNxN6U/Z0zk9V0rXu9SR0W1rzkT8hIcI1U2wU VOA3b107P4JytMAjiFBiuka1EZ/a2ZFAgcxjDoGSeqEh86N17DrpPHoLSxJUTTQ+PWCk KRAA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject :dkim-signature; bh=jWdC2gxe4/WDV21/endbJF4fzwzsiXqKm0WvAA47Cwg=; b=OHoBjdIWEOhwsxmLir7EiolXDaPKvzvq7Xt3REakEgbmjQbKYPgxaV4FabiFN7ET9r sTYWPhN23pvoxqOfl1Z3Ds1cKfjxJcdWcHFyL0i2ecy7/pk/xZlCuTmA+eb0no6TuQBk XkTprhtyyuREnFG0Jub/j6QA3zAG72/lWINZRLP+jE3F1vzajmGs3ECMP+DZ9Ym1UcCj ofwjzYX1k50bkJbBNR8OOVwimweeJ+Jm7NrPP4Nolg/XlMU4Gtx2prt7eE/WvBvJP8dk bTWsgh/c/Ns1XRZGSfxCEVFKP/Y135v0gHEPoLTZVi2DWagoeht85eV7cA7uTEegq4vU f5tw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=t6XjS0XZ; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::32b as permitted sender) smtp.mailfrom=sojakova.kristina@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x32b.google.com (mail-wm1-x32b.google.com. [2a00:1450:4864:20::32b]) by gmr-mx.google.com with ESMTPS id j2si302016lfe.5.2021.03.08.08.27.26 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 08:27:26 -0800 (PST) Received-SPF: pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::32b as permitted sender) client-ip=2a00:1450:4864:20::32b; Received: by mail-wm1-x32b.google.com with SMTP id 124-20020a1c00820000b029010b871409cfso4160388wma.4 for ; Mon, 08 Mar 2021 08:27:26 -0800 (PST) X-Received: by 2002:a1c:4b11:: with SMTP id y17mr22416139wma.171.1615220845724; Mon, 08 Mar 2021 08:27:25 -0800 (PST) Received: from ?IPv6:2001:861:3cc3:38e0:4822:caf5:1111:6bed? ([2001:861:3cc3:38e0:4822:caf5:1111:6bed]) by smtp.gmail.com with ESMTPSA id 3sm22131878wry.72.2021.03.08.08.27.25 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 08:27:25 -0800 (PST) Subject: Re: [HoTT] Syllepsis in HoTT To: HomotopyTypeTheory@googlegroups.com References: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> <7d4b6fd7-3035-e0b9-c966-97dd89d8b457@gmail.com> <87blbtk7ey.fsf@uwo.ca> <1f7bbcb8-ee50-0c24-174e-d3852e52bbee@gmail.com> <87pn09ipd5.fsf@uwo.ca> From: Kristina Sojakova Message-ID: Date: Mon, 8 Mar 2021 17:27:24 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.10.0 MIME-Version: 1.0 In-Reply-To: <87pn09ipd5.fsf@uwo.ca> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US X-Original-Sender: sojakova.kristina@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=t6XjS0XZ; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::32b as permitted sender) smtp.mailfrom=sojakova.kristina@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: , Is there a geometric interpretation for the proof I gave? On 3/8/21 5:25 PM, Dan Christensen wrote: > On Mar 8, 2021, Egbert Rijke wrote: > >> I had a different route in mind, much less efficient. There are three >> kinds of concatenations in the third identity type, all three pairs of >> them satisfy interchange laws, and there is a coherence law between >> the three interchange laws. > In case anyone wants to play with this in Coq, in this branch > > https://github.com/jdchristensen/HoTT/tree/Hurewicz > > the file Smashing.v contains similar facts, e.g. pmagma_loops_shuffle. > (But no coherence law is proved.) > > Dan > -- 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/c4d0d50f-8a11-3d63-7c32-3fa3aae1fd96%40gmail.com.