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,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 7929 invoked from network); 8 Jul 2023 14:00:32 -0000 Received: from mail-pf1-x43b.google.com (2607:f8b0:4864:20::43b) by inbox.vuxu.org with ESMTPUTF8; 8 Jul 2023 14:00:32 -0000 Received: by mail-pf1-x43b.google.com with SMTP id d2e1a72fcca58-66870a96b89sf3597562b3a.3 for ; Sat, 08 Jul 2023 07:00:32 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1688824831; cv=pass; d=google.com; s=arc-20160816; b=QTm3TFxlffJvrToQiE72BPRT9tPZxOlJNZugsta2RkdsRi8eAVNV0SEdzRKQGyA80G XDFpNnWZAEPexkNTIng+ZHMvhF96cJIxUfbxKV/hJ+BV5Z2TezH/mNsLnEWfVqCJmbRe svkPLxT/0z2hq/fqGnMevYXkofgvVu60OmYq09gdpedBFJemupi/IH8PjDt7NL3SqVGB 2S9cibwEmHpXOqwdGBrswz4JppewOlccn4gFfsDFZEffWoE+HxLQeUmay5pHytT41AYa w3jEZjq8LkdOo1AUB8seUBTW95b6Q1HHw7pAO3kofc495mX3kEIe29ML3iehTF7uFbSK hxkA== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=YIm/uKu6fweHh8lPXrGaGPu+xO52kRLxEHaFkcq5IZ4=; fh=qVWvkAOeECjGOkGdkHx/ySaLGbAPJfjqqL9HRu/jkCE=; b=Zxay+JZ8dY8hOQwat41BpJXn71UnPiasyf538wSTFcMt9kymB+T6jr31hBqFsz+ZmA vIw4hgMfGIDaI8eg/0kKxf4NJA8+a4SvO55xv1NxoS+BNcjXf6A2W1WdCDEsACjVY7jW 6QmzgnDigqVsGH23O0+YgXB6saKwiR0uQlaxZ1qCNv/QS6VMsh5LaUyRCpMTyFl9wTHi 6zUNqDgfnY4kBXOzI9yZaRHUrDazp0m3Q4kaCtFoQx+cGx5zHzE2XQKh+HuUDqb/6EFD +7mtMqXHUYeimzylaZ1x+KWuYtQRalgNPASwkRkgtfYMa7iOj72eLgpxXtObBqylSmSA 7pjQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=R2qAPNxC; spf=pass (google.com: domain of droberts.65537@gmail.com designates 2607:f8b0:4864:20::733 as permitted sender) smtp.mailfrom=droberts.65537@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=1688824831; x=1691416831; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:sender:from:to:cc:subject:date:message-id :reply-to; bh=YIm/uKu6fweHh8lPXrGaGPu+xO52kRLxEHaFkcq5IZ4=; b=YkV1yZt3/13MRLvEYSG81KZ9IapZcC+l/vjdkBLDJFcR+vzxbDvuVLxM70ZiqUksnJ AgNkWkKxJKufTZ0U4jhn/Ud3LWBf7JAlC0e2qI9hzoAZQIspbKc5FxHTB3e26TZszhgV pNak952J9ieugLboScLXdEgjzL7G8HHN6ceK44CpfBFdx4gN8nnFIuoLfDkbEyuPp0Pn YBPWHN0mPJi10Ubb3htJxbq5PQOU2fOIDxuptWVm6aXlQbbbrgzm14YgRKwn1AsMrv0n 7EJFT8U3wNop20mBnTPT4gr0526sjF2cvtybtNBtNySYs9G4VS7KLvxErfICji/9LASF Qc5Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20221208; t=1688824831; x=1691416831; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:cc:to:subject:message-id:date:from:in-reply-to :references:mime-version:from:to:cc:subject:date:message-id:reply-to; bh=YIm/uKu6fweHh8lPXrGaGPu+xO52kRLxEHaFkcq5IZ4=; b=a+aYxt27kv0AcICa2AwtiVPUz+5Vj+LRpdshKSzBY4Oj//rvBSHFrGdC7ToXPO4+7H swJbEbUTyWn3IgrNszd/qyuooVANrd9hEMH5TPVVjiGPqBDwvQ/lLANzaSqEdYyiiBZH ifSWR7zsOhb1KvBGKWIbniR9lYI5TheNRk4p/s8PNBwDLWQSbg/oMsgZPENOvwozMp3r jSPe8mTal0M4iBUJ5ttYKYeoTnRGOH+pFyB2AZHG+uwNT1DPPBPPnOTVtBIc1MWeWQ+y uCeMs6vJHaIW+NsTvsKfF2RCsYUKFlKsCOeuUamc/BQvGCQWGiKTBq8AaFqm7a+uJKze OMLg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1688824831; x=1691416831; 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:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version :x-beenthere:x-gm-message-state:sender:from:to:cc:subject:date :message-id:reply-to; bh=YIm/uKu6fweHh8lPXrGaGPu+xO52kRLxEHaFkcq5IZ4=; b=UJceay5kNebUA8ERsL2NuVMbNZ1YHE2gVKQnhlsFAdroTJ0uDFg2FnPo1ya2Rt/InL YOACPKIj32DDDsJTDt1FQgSoECuEedHfZBVt3FgKPdHeH4VVMiZSR0ZkV5apUoEuHuEI 4xK5R+rkWz4xwZcI6PxiBhU2a/2RX/OBF/NkFIMXqLOUfVaNYaePalSNB9PondAIcdgk pj0s6xX2cXBtLygOaui2vpj2g0IaSAm1Q+2jp9nSgnnWYo0hip4eWEMSIm2ooSZNyPAh 30DqhZTGXkB4SaJja++xRZ5gMQLU/dOQpDiTYLsdE6pxCPinq8/gMgVi4Dxm/FqeZlvF PdUA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABy/qLaO/np7RRYDJR1253wFfs6YSpxrGl4sRKkOfDNXQdj7Z66Dtrl9 nBXLpnjY0f9MSTsy6VhYck0= X-Google-Smtp-Source: APBJJlEJJqEgGrkQVAk5CxgJisyZWveG3pAOOVdoSz70fGlNVr0hFKoBOB4Jpbqn5GWfSw1rh/BRIg== X-Received: by 2002:a05:6a00:198a:b0:67e:4313:811e with SMTP id d10-20020a056a00198a00b0067e4313811emr6130031pfl.0.1688824830054; Sat, 08 Jul 2023 07:00:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aa7:9ae5:0:b0:669:e426:f211 with SMTP id y5-20020aa79ae5000000b00669e426f211ls1552429pfp.2.-pod-prod-09-us; Sat, 08 Jul 2023 07:00:28 -0700 (PDT) X-Received: by 2002:a05:6a00:1409:b0:66a:613f:87e1 with SMTP id l9-20020a056a00140900b0066a613f87e1mr7171556pfu.8.1688824828086; Sat, 08 Jul 2023 07:00:28 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1688824828; cv=none; d=google.com; s=arc-20160816; b=FzeiISt1YPSD8fzbnC3fdEm3wKMtgMWw7Gnrwyv+b/LDyJ5SKVmQfUwSqBar7bohyT r8y2Te6IMP0nVgQOvx8mrT4VBjbV5EEJMjKgziztjuL/zjOjc8mB2pKVqmdjSWPnR7Pb i/YNHOL0/2eoiosDwYw3GJOOm/Fplm+usO2c2Sy6Lw25MpkfQm3PQZ19ucM9ZE7kk0Vf ColarJ2vuqnldmkRpiCgYrEd4/OUHch//JcJ2PARfxQJpMYeVC8CzLjIvFsLNy69TUKu AHqcVnyzsDb+qZOGSqOc8oak5XsK1pbGvquOzF9PYtHXHsMbN4tCvNGkchPW7r7tMQth KixA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=NIpprSayhPP9iR94V8Nf2A6zuYWimGK1CgYTir8aTYI=; fh=qVWvkAOeECjGOkGdkHx/ySaLGbAPJfjqqL9HRu/jkCE=; b=MlI9+T0mxaqEvcmZJMaGwKj3SM/dQv1V1TdnLZiVn0rMnfzA07Hmh8kUYS5nIPSsNe +MAMcnqKQ2TifIMFAKMyOjucznRN84+j9IXHYbtYJbLQ2qnMk7B5IBotADL0zxMMXJT6 gfSwh6GDHxbjAkbTJkj4JHYs8LtzBUC7j+HqNCUKtitsTm5wBM3DNVz532C8tYDvELF8 d0rKPb+udCmgZGpMPSMvX1Gyv19H6jFroed7xiuAEv3WENjQlBJ7+ezYoj2CMBG9FWmo D5bC7tvrcTWD9SbhTqWAcnvKn0R9vvgHW+EFjU3amlMswd/nwM29AakdD6WquJU5x3yb UMFQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=R2qAPNxC; spf=pass (google.com: domain of droberts.65537@gmail.com designates 2607:f8b0:4864:20::733 as permitted sender) smtp.mailfrom=droberts.65537@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-qk1-x733.google.com (mail-qk1-x733.google.com. [2607:f8b0:4864:20::733]) by gmr-mx.google.com with ESMTPS id y14-20020a056a00180e00b00681f56016b9si317719pfa.4.2023.07.08.07.00.27 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 08 Jul 2023 07:00:27 -0700 (PDT) Received-SPF: pass (google.com: domain of droberts.65537@gmail.com designates 2607:f8b0:4864:20::733 as permitted sender) client-ip=2607:f8b0:4864:20::733; Received: by mail-qk1-x733.google.com with SMTP id af79cd13be357-7653bd3ff2fso298980985a.3 for ; Sat, 08 Jul 2023 07:00:27 -0700 (PDT) X-Received: by 2002:a37:ea1d:0:b0:765:a9d7:2ca2 with SMTP id t29-20020a37ea1d000000b00765a9d72ca2mr8067167qkj.48.1688824826989; Sat, 08 Jul 2023 07:00:26 -0700 (PDT) MIME-Version: 1.0 References: <5255bd6d-8b20-a4e5-bc6b-4f8418bc6700@gmail.com> <1F1A83E2-2EE9-42D6-BF30-D11DE1B12F56@andrej.com> <8e549102-49ca-407f-e95f-22d971f4b9fe@gmail.com> In-Reply-To: <8e549102-49ca-407f-e95f-22d971f4b9fe@gmail.com> From: David Roberts Date: Sat, 8 Jul 2023 23:30:15 +0930 Message-ID: Subject: Re: [HoTT] Syllepsis for syllepsis To: Kristina Sojakova Cc: homotopytypetheory Content-Type: multipart/alternative; boundary="000000000000e6935105fffa2bb5" X-Original-Sender: droberts.65537@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20221208 header.b=R2qAPNxC; spf=pass (google.com: domain of droberts.65537@gmail.com designates 2607:f8b0:4864:20::733 as permitted sender) smtp.mailfrom=droberts.65537@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: , --000000000000e6935105fffa2bb5 Content-Type: text/plain; charset="UTF-8" Dear Kristina, Am I correct in assuming that the "syllepsis for syllepsis" is the equality of (4) and (5) in your paper? Is this related to the fact stable pi_2 is Z/2? Best, On Sat, 8 July 2023, 10:46 pm Kristina Sojakova, < sojakova.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 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/CAFL%2BZM-%2Bkw%3D_VbtnLAkmdnEvmJSC8PCUf3NfK6hc%2ByYN_zuszQ%40mail.gmail.com. --000000000000e6935105fffa2bb5 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear Kristina,

Am I correct in assuming that the "syllepsis for syllepsis" is= the equality of (4) and (5) in your paper?=C2=A0
Is this related to the fact stable pi_2 is Z/2?

Best,

On Sat, 8 July= 2023, 10:46 pm Kristina Sojakova, <sojakova.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 yo= ur 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googl= egroups.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 &= 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 htt= ps://groups.google.com/d/msgid/HomotopyTypeTheory/CAFL%2BZM-%2Bkw%3D_VbtnLA= kmdnEvmJSC8PCUf3NfK6hc%2ByYN_zuszQ%40mail.gmail.com.
--000000000000e6935105fffa2bb5--