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.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,HTML_MESSAGE,MAILING_LIST_MULTI, NICE_REPLY_A,RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 20515 invoked from network); 8 Jul 2023 20:14:33 -0000 Received: from mail-lj1-x239.google.com (2a00:1450:4864:20::239) by inbox.vuxu.org with ESMTPUTF8; 8 Jul 2023 20:14:33 -0000 Received: by mail-lj1-x239.google.com with SMTP id 38308e7fff4ca-2b6ce2f2960sf21922021fa.0 for ; Sat, 08 Jul 2023 13:14:33 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1688847272; cv=pass; d=google.com; s=arc-20160816; b=geJUFClcT+yDdaQYFiTTSiUq0E2FCnIDLLf5gw5LMPmnmvaAVmFClNG0d2S+2dWut3 g5J22iB6390Ugx2xjMFQ7c5WxxzRJkCJHMHiCLk/dnDserX6AwBDL7esCQ0p/IkHm81+ EywInZzuiq8Ye0ms5mLRZ59Rx4i/P7QQUO8UQZveqvj60lEGhKt6fhDo/bKq7zK2DWTE ggKeQ/AUTKO++vFtOqSrsoAejP8wQC89TvlXgNS1MbV8Ppm8KuCfvaqCSUduz3GJDIpC Og3sAsJPQ3KquDNWNbB9kFwpJ9BcEKHUJdMmCW/ZHGtcEaY6UrZFrAYwgAa2ApDtjdQn XLdQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:in-reply-to:from:references:cc:to :content-language:subject:user-agent:mime-version:date:message-id :sender:dkim-signature:dkim-signature; bh=C4vsgQHCT4eiISZl+O7gyP1Hh2eca8Xg2PiEVtV90cI=; fh=ICenHIQ0lzzJFPs5q/7+XrBkLIciwl+416RNWfHyqqw=; b=ONdsq/rWaCtah1CDY/X9j7pRDyfM8t+G5PDMps9m686kvjh9dsG0FvC9KcuQBRO+Gb u1Xk5zkkAZa+W+XR4E3FiUdBhcKdgglcWWYCw7P//Ay8hsZBqId9TrRA7+0BEXse7EVA IZhayZyTSg/7NBQnkxP+X7qS4bMNVxFIQV5RTDSOJIFXEuDSkQxS/4y78unz6Pi1BE+4 WzhL8rVk7WScGYKlr7yscfsmFI9eNv6kcdNRYey8wGskY5rgLp2C7s8eiQ0Wh8OgzlPK Lu73dtaoOi5itI64O2yjY32FSeOMgeOFT7M6smd5aWwEjM51d+WGNdpJu4QgtuISts4Y ktzQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=nHVs6Jsn; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::42a 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=20221208; t=1688847272; x=1691439272; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:in-reply-to:from:references:cc:to :content-language:subject:user-agent:mime-version:date:message-id :sender:from:to:cc:subject:date:message-id:reply-to; bh=C4vsgQHCT4eiISZl+O7gyP1Hh2eca8Xg2PiEVtV90cI=; b=d7xLz2SKz1Kwixf4rfhiZMiPwXKhGdgdqbLfvJf+7oIuDUbSKF6bXhC2a31/MXNe88 hDixoGb2strRWbMrCNnfXDxFcswCIiYNCBNGmkC+y8KVnwSL+2xTiGcAq1kBVYlDufxw OZcM/hY3soPC3zL+pfvssGeicyxG0P2si/5AXQ8QASrmCbJssROPGcQcTs4CcKUmVL/1 KYQmspSJr4E4LnzEKiJln8xK4aMVcFxWLlKK9z4ECEvzIaxigF43xpOvaPooPVWjHbkb 7w9EqvxJGCCmQGUXoUg4aispDPUqFDoNKHnxMFNlyIkOtGbEiPOR9j4KtSSd6zI9w2YT QzXA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1688847272; x=1691439272; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:in-reply-to:from:references:cc:to :content-language:subject:user-agent:mime-version:date:message-id :from:to:cc:subject:date:message-id:reply-to; bh=C4vsgQHCT4eiISZl+O7gyP1Hh2eca8Xg2PiEVtV90cI=; b=WOKLfD1PWrme38yBTIF7AGKmLN3hBumfcFMp2UZOQAytMNx+3EOzYX0TIDWZY/tus1 sQ1jo1nOXYvdjZmuRGoFbi4VWHdxGjuKxFwLi4INMk+VnygHQCw0R/WcPs4ZMpWvqI0+ OM+nM4x+gn1DAGORMUCfg4CCl3u22y0VXSmMdCgAwiZ1/tIPUHxqLAxSa9oTf0fYNFNe ZlHziPMosC4v5kur54xquUBHtv2XFi7hKvLjbZ1fABJV+ZKWFy8m0nfUdMZ9cpF7vPHX cZhyAC7ST4tt6V1BBQtDCow8+G5omY/jZHJOAlo7+CvB+w2K1yAe+7SJx/Eg6l0xZk1+ BCSw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1688847272; x=1691439272; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:in-reply-to :from:references:cc:to:content-language:subject:user-agent :mime-version:date:message-id:x-beenthere:x-gm-message-state:sender :from:to:cc:subject:date:message-id:reply-to; bh=C4vsgQHCT4eiISZl+O7gyP1Hh2eca8Xg2PiEVtV90cI=; b=i+tBoEO0UUIcZ9hia3c1yFQ223Pgw/SBWEI/jIkXqon3/mHxYLG4hjjyH2K4cR7iUg TNTbgKjyfNM4/3btv798WgqdhavE+R7cOh0L5NQB2n52TUdiGUhihfOvlnWK152HJso7 /peOFFUScnKrMEr2nhq+KfGliC6KzNVDBU9vFJvNHDleiM7jY0+ncQyeqCyKTi43Mf3O Fb8I8gC7J+Zflz8mjQCvGjrxPshgqYzvJDfyPBrSL6FXy6hDDEu45Ug8YYJH6SlRXHFE WKR7+PdnZSD2UbCJrgr+f7Ri2sKoOzOvrMkYYKgF+GM9BaO0dPFCf07QrlwkBAsetz1i W1Aw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABy/qLYPZnDN4lCeAucSYGtEmBtR4wi4OvCA4HRrQloKW6XUZ2rHc778 U1ob8ESVkCuIUGXgx//mDR8= X-Google-Smtp-Source: APBJJlHWfDF2xrDshav1iXoe/bDL35ajsVkd7zV5PrlvBUeASoA/SJ2mj4y1nMcTXRZ7wLmMFlLJew== X-Received: by 2002:a2e:2e17:0:b0:2b6:cd70:2781 with SMTP id u23-20020a2e2e17000000b002b6cd702781mr2937564lju.12.1688847271542; Sat, 08 Jul 2023 13:14:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:bc89:0:b0:2b6:bdad:fb4b with SMTP id h9-20020a2ebc89000000b002b6bdadfb4bls779092ljf.1.-pod-prod-00-eu; Sat, 08 Jul 2023 13:14:28 -0700 (PDT) X-Received: by 2002:a05:6512:3e25:b0:4f8:5510:c897 with SMTP id i37-20020a0565123e2500b004f85510c897mr3505179lfv.18.1688847268410; Sat, 08 Jul 2023 13:14:28 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1688847268; cv=none; d=google.com; s=arc-20160816; b=ReiO1c+qV/GFajDUNbgOyADOFc8mMSVwpm41NtuKh9MydjLlGD+lMrWvm23/xadnF3 tCUWcyd026FOelRD6Zz+3nFJjmxVP6HHudW0/3kjQokpCF4l6zwiRverts6Jg78SpAYa o6D2KScEua+Cn6DpF2vZX93OCBtHTddlxxOFobrZR8ls6Q5LJqJYCz+3MT0TP3xhivEs XUcItbgFr9TxSyRrsE/3Zl7Gbqw7N9XaXFTDP6Gx5Ger5/x5gnftk2oE9w2VGedXMQBH Kh4ZhWZKZcySq2V1NZjM188l1UcdfzIHT5bMwZxmjNYYuY5JJAZVP+wTQ1imQuIYSAxy Mt7Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=in-reply-to:from:references:cc:to:content-language:subject :user-agent:mime-version:date:message-id:dkim-signature; bh=+495fSJuj+zq/RyeR0Inju33ot/P3NSZ6ekX/g8ZV4k=; fh=ICenHIQ0lzzJFPs5q/7+XrBkLIciwl+416RNWfHyqqw=; b=0ntWvqUryc7xaLsdkB4q5UUR1II9+lsOKrW0vrllZcWhS/EmzdxzNtija2e4qRH/kg DzY82esoeEfNt880/RcaS7JgVHMTbr23ai0EQd/eXbHxv5FCdx3zlz++UyRyDTywsiBf QDQv7BDYe20mLMkR4dpd614DrbHSR75v8gnCUZE3u4cRRGMp2Aw0flPcMgJcTvH58qQX glAzheZ9s4hQDlEw+1o8U+xcBXqPaYaILJ/tDseuEhgwgXwzC8XetonRbixbSqusQIpT MK3+Fw3vK7AYxKfdKJP3O5DUg/qthpzgJ8qTwOIGa9nIKL9l6QtQBYL3M79YC4uIwk2U QaKw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=nHVs6Jsn; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::42a as permitted sender) smtp.mailfrom=sojakova.kristina@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wr1-x42a.google.com (mail-wr1-x42a.google.com. [2a00:1450:4864:20::42a]) by gmr-mx.google.com with ESMTPS id m20-20020a056512115400b004f8621b17fasi460403lfg.3.2023.07.08.13.14.28 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 08 Jul 2023 13:14:28 -0700 (PDT) Received-SPF: pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::42a as permitted sender) client-ip=2a00:1450:4864:20::42a; Received: by mail-wr1-x42a.google.com with SMTP id ffacd0b85a97d-313e09a5b19so3538961f8f.0 for ; Sat, 08 Jul 2023 13:14:28 -0700 (PDT) X-Received: by 2002:a5d:420d:0:b0:314:3f1:cebf with SMTP id n13-20020a5d420d000000b0031403f1cebfmr11564481wrq.28.1688847267398; Sat, 08 Jul 2023 13:14:27 -0700 (PDT) Received: from ?IPV6:2001:861:3cc0:bc20:91bf:d689:8c3b:38bb? ([2001:861:3cc0:bc20:91bf:d689:8c3b:38bb]) by smtp.gmail.com with ESMTPSA id l6-20020adfe586000000b003112f836d4esm7637698wrm.85.2023.07.08.13.14.26 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 08 Jul 2023 13:14:27 -0700 (PDT) Content-Type: multipart/alternative; boundary="------------sYWMP8435ZnvbSge3TO7tdjP" Message-ID: <7a08f997-1433-177d-ab99-b45ea4a14a8f@gmail.com> Date: Sat, 8 Jul 2023 22:14:25 +0200 MIME-Version: 1.0 User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:102.0) Gecko/20100101 Thunderbird/102.12.0 Subject: Re: [HoTT] Syllepsis for syllepsis Content-Language: en-US To: David Roberts Cc: homotopytypetheory References: <5255bd6d-8b20-a4e5-bc6b-4f8418bc6700@gmail.com> <1F1A83E2-2EE9-42D6-BF30-D11DE1B12F56@andrej.com> <8e549102-49ca-407f-e95f-22d971f4b9fe@gmail.com> From: Kristina Sojakova In-Reply-To: X-Original-Sender: sojakova.kristina@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=nHVs6Jsn; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::42a 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: , List-Unsubscribe: , This is a multi-part message in MIME format. --------------sYWMP8435ZnvbSge3TO7tdjP Content-Type: text/plain; charset="UTF-8"; format=flowed Hello David, On 7/8/2023 4:00 PM, David Roberts wrote: > Dear Kristina, > > Am I correct in assuming that the "syllepsis for syllepsis" is the > equality of (4) and (5) in your paper? Indeed, we show the equality between (4) and (5). > > Is this related to the fact stable pi_2 is Z/2? We do not yet understand the implications of this result, that's another interesting question I guess. Do you have a conjecture here? Kristina > > Best, > > On Sat, 8 July 2023, 10:46 pm Kristina Sojakova, > wrote: > > Dear Andrej, > > Indeed, my message could have been more user-friendly. The file > contains > alternative proofs of Eckmann-Hilton and syllepsis, together with the > proofs of the coherences described in Section 8 of > > https://inria.hal.science/hal-03917004v1/file/syllepsis.pdf > > The last coherence outlined in the paper is what I referred to as > "syllepsis for syllepsis". > > Best, > > Kristina > > On 7/8/2023 2:22 PM, andrej.bauer@andrej.com wrote: > > Dear Kristina, > > > > any chance you could spare a few words in English on the content > of your formalization? Not everyone reads Coq code for breakfast. > > > > Many thanks in advance! > > > > Andrej > > > > -- > 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/8e549102-49ca-407f-e95f-22d971f4b9fe%40gmail.com. > -- 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/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.com. --------------sYWMP8435ZnvbSge3TO7tdjP Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Hello David,

On 7/8/2023 4:00 PM, David Roberts wrote:
Dear Kristina,

Am I correct in assuming that the "syllepsis for syllepsis" is the equality of (4) and (5) in your paper?
Indeed, we show the equality between (4) and (5).

Is this related to the fact stable pi_2 is Z/2?

We do not yet understand the implications of this result, that's another interesting question I guess. Do you have a conjecture here?

Kristina


Best,

On Sat, 8 July 2023, 10:46 pm Kristina Sojakova, <sojako= va.kristina@gmail.com> wrote:
Dear Andrej,
Indeed, my message could have been more user-friendly. The file contains
alternative proofs of Eckmann-Hilton and syllepsis, together with the
proofs of the coherences described in Section 8 of

https:= //inria.hal.science/hal-03917004v1/file/syllepsis.pdf

The last coherence outlined in the paper is what I referred to as
"syllepsis for syllepsis".

Best,

Kristina

On 7/8/2023 2:22 PM, andrej.bauer@andrej.com wrote:
> Dear Kristina,
>
> any chance you could spare a few words in English on the content of your formalization? Not everyone reads Coq code for breakfast.
>
> Many thanks in advance!
>
> Andrej
>

--
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 H= omotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https:= //groups.google.com/d/msgid/HomotopyTypeTheory/8e549102-49ca-407f-e95f-22d9= 71f4b9fe%40gmail.com.

--
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/msg= id/HomotopyTypeTheory/7a08f997-1433-177d-ab99-b45ea4a14a8f%40gmail.com.=
--------------sYWMP8435ZnvbSge3TO7tdjP--