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 16654 invoked from network); 8 Mar 2021 15:15:38 -0000 Received: from mail-wr1-x440.google.com (2a00:1450:4864:20::440) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 15:15:38 -0000 Received: by mail-wr1-x440.google.com with SMTP id m9sf4969284wrx.6 for ; Mon, 08 Mar 2021 07:15:38 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615216537; cv=pass; d=google.com; s=arc-20160816; b=YFDAauTaGk+xEuCE2JXbzQJS1eI6WhPHzBbd6xCroylU0CMwTEM7mBKjof6FdAUDzm M8bBHny6/V5tEgOBk/olLZM7J7kp8E3JP061RVf6b7BOoqTfuwYXA8aVWgbjB9UCnUx8 PCvRAyEfOKFhwTDnO81cfa7JhT0SBUFhfznDmQu6QXQP5t55pmwX5LJIV9Ub1bs1a9Sl gyzI0K0FkrolqnEhuQEnKYkDWX/lT4sa/sd9rLMsrA0CbK/eMNFAnuxwE6Wx5APN653X rjcF4PAxj/X9VK7YD26sqVGlMIO6VDkCVuYDRFmqPSjwj4EOOdxkTXKjmpOaqdPwXvv4 c5aw== 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:content-transfer-encoding :in-reply-to:mime-version:user-agent:date:message-id:from:references :to:subject:sender:dkim-signature:dkim-signature; bh=8PEaLn46Q7Ib+rm8Gkf1SLNGpK4M9k7qbNVOgtAjjf8=; b=qA4q4DidU6ebDA6rT/yEkGWVfPJJuGs+LyoTbYAHMN7Gy6XazoV1X22082urOOiran A893OcyQYYEwXAIDjKfxOZQH7Kn66/C5CcrIer72JuOXUUB6xMk2nox9ZblenCvAymrz Ml2IGDmOzTtYbYMIxlYh+RJyDoGTMR/yy08yvPAZ7uIhFBoRfefOi5n3jSSB3fW+x2jX wDpaPPC2C4BZ954az1sW9zcrTJFPiCXX2HnPLplduCn5twpv++JmRsv/X11T+YI7luMF 0KBTIHG/CyTjK+AYcqzhPUOpFSUP9ZUyBH+edwooA/5KO6APNQQGIdbUtNVoyzNkIWo5 fMXg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=UTa4SIzh; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::432 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-transfer-encoding:content-language :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=8PEaLn46Q7Ib+rm8Gkf1SLNGpK4M9k7qbNVOgtAjjf8=; b=q595H/4hbNhfl5WxLZ+vN5K99nYakT7/3Oy0UyfdSrmfWN3K2EOfAuigiVf4FfmeJ0 yBtSeJ4ryoct/hTaES3igJCixO1ygB+BKWit9Ph449+prkLLenNYC/wEPz33lnFaJsYy z2CPO8C048bTYFLtr+ALVGpx6pqVkEowyTqPKhZT+rhTKe1hfEPh6h6tngjdmIMNYpWD 9Q9YHpp85pp/i7U7whKs2HPCzwosaTfYRW9afAmn5jMFq4fnRXBc+96X8p6lIVnwlcxx CIulfM5dDP3qdey7ht5WcqddDKLnOxvJr849A+Yu3gQCdL7ILoYtzpYn7R37EIMQKREZ Y36w== 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-transfer-encoding:content-language :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=8PEaLn46Q7Ib+rm8Gkf1SLNGpK4M9k7qbNVOgtAjjf8=; b=FuieAnnb8fVV6swNaQv2LyTX7hU4cy11QUwGD/Fk25GG7p6gfxYoK/QDPfQBwAfACb EB4N36nSwzarqwOX+cOI450oi02zOClWyGr0TsidwWhookfEYU7EuDDalGzZdtAygJQm AqV0/y0IgnVxyxY51HmTiqRcDGtzgeI4oIgKIAegffNOi56LfG5DFoBJLqY3HLjGagMp lSK1tDx3vxJDHYVpdQMk+39EVmxGLQB7/CfZeAq7Gxd7X0hi3biJ7Bi0AaLDgRuP6IMw WiQf8NgUJAGRMc8cXR1gZXVgHLZ2QnpVwmKxl6q1xXxPH70/Nt+1sK+Fk0/mYNUcwSp8 Jgag== 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-transfer-encoding :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=8PEaLn46Q7Ib+rm8Gkf1SLNGpK4M9k7qbNVOgtAjjf8=; b=sgE0MXNuH+Ihewf9NGhQyba+zvYg1zsQCw7Gmhz5fAx+I00UGIx5bSyYBWoyRVgznO uyQgHDCwbh9DryupwVnNxMSpSxNHwxiS6aOloHogLJTHPWkEVz2L1NqS5+SRvbPVwcPn OKjkxYvf1AocEU02Pp4BWPSzN/drXfDTR/OY7tstQ2iCXR0y3C0clBYtTHkCRWX0IN8t +qhyakdXF2oRbPl2T27zqrpySCtIjeK/td1D7DVPVnUvUgPT8+qkYAmws9OhAhFO1oJw nJT/fARe8tGEknkSg7XZPanR0ReyUBFN5YpzBo4qQCowaxo2VCs2ddsZ+7Sc1oqU+zoe w+Fw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM5334DavUeSeUMF3nKalzyFkRdJmjNZZ5Z5QdyBX9piL6PV19NvJb 7DnTxNAHNM2+XhlP6Y2sYdU= X-Google-Smtp-Source: ABdhPJw9wMkrRrk/fg1JShdyDQb+SgqnzS9XvxqoR3ZoYIkkV8i0pMA9q6BZlLNhHZWWKK7MITN1dA== X-Received: by 2002:a5d:5744:: with SMTP id q4mr24067587wrw.390.1615216537487; Mon, 08 Mar 2021 07:15:37 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:1546:: with SMTP id f6ls1720195wmg.3.canary-gmail; Mon, 08 Mar 2021 07:15:36 -0800 (PST) X-Received: by 2002:a7b:c4c1:: with SMTP id g1mr22165530wmk.145.1615216536554; Mon, 08 Mar 2021 07:15:36 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615216536; cv=none; d=google.com; s=arc-20160816; b=0eK0XJ3D0cC802CYgT4x7vG+M5+zZwfW9bZ5X0AQDwfzGHRGK8NMickMf2+iMvXny7 5gg3Xp8HOiVbXiiyeNaMUQ3qS0jHT6ZCGDVwK/68xXXAhuBnjhtm+421IlrHU1LMuXts 6OW762Kv5H0zyeUt1bdz3UyBploat8ILHVJmB1Ka0KbI1AunlJowdSsJMMznmhkSLh5F SPW1MvT1Di+ZoH25CB3XXhEekBw+I9qLaw7Jrt4jyNyEphG+Rk1h+zb/Ayq02g5Y4KVC saUM/dUaYpD5qSfnRMgUdvihOTOYlWbXSC5hxT30knivuQ2ti1yv6MP8Md0boCBzpwah 6c6Q== 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=rEm778oWRkF6c8soY94J5LYvLZ0BGNp/oniOD82n4Hg=; b=dynf3vceFHmR7DQSaqzpqeNJUpVOEzQfV3+jlnHBpbjQpTseYZva25Fpgr0xaWiqNb kiB5CF3UPMoBB/ij98sv34eWeImZJAbKHhGZmu5Xyrtd7SiXQv+KqPZcHLkE0vIgy5dy c8J+PX0gznNf24jhuFYhI6wxCy3oh38+3IOnq/ntX4iaiJ5BNZGjHeeiIU4AwSAWhed3 xHyky0sN7ICi0qdkZXhc1+UmG6C+5hKUrCmxXzaXknarEq4t6kF0KQqqlTtP3KpL0vtv 76Ux4WLOOF1IOuA6PToegjgIFmvQX6TNUQtjMt7hgpAYvZeUCCJxEEyN5Ue+YKW+R/eO 2ETA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=UTa4SIzh; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::432 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-x432.google.com (mail-wr1-x432.google.com. [2a00:1450:4864:20::432]) by gmr-mx.google.com with ESMTPS id i22si571105wml.2.2021.03.08.07.15.36 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 07:15:36 -0800 (PST) Received-SPF: pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::432 as permitted sender) client-ip=2a00:1450:4864:20::432; Received: by mail-wr1-x432.google.com with SMTP id v15so11843103wrx.4 for ; Mon, 08 Mar 2021 07:15:36 -0800 (PST) X-Received: by 2002:a5d:43cc:: with SMTP id v12mr23251605wrr.287.1615216535795; Mon, 08 Mar 2021 07:15:35 -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 s23sm19056297wmc.35.2021.03.08.07.15.35 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 07:15:35 -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> From: Kristina Sojakova Message-ID: <1f7bbcb8-ee50-0c24-174e-d3852e52bbee@gmail.com> Date: Mon, 8 Mar 2021 16:15:34 +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: <87blbtk7ey.fsf@uwo.ca> Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable 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=UTa4SIzh; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::432 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: , Thanks Dan! I think we should have no trouble showing that what I used=20 is equal to your proof but packaged a bit differently. On 3/8/21 4:10 PM, Dan Christensen wrote: > It's great to see this proved! > > As a tangential remark, I mentioned after Jamie's talk that I had a > very short proof of Eckmann-Hilton, so I thought I should share it. > Kristina's proof is slightly different and is probably designed to > make the proof of syllepsis go through more easily, but here is mine. > > Dan > > > Definition horizontal_vertical {A : Type} {x : A} {p q : x =3D x} (h : p = =3D 1) (k : 1 =3D q) > : h @ k =3D (concat_p1 p)^ @ (h @@ k) @ (concat_1p q). > Proof. > by induction k; revert p h; rapply paths_ind_r. > Defined. > > Definition horizontal_vertical' {A : Type} {x : A} {p q : x =3D x} (h : p= =3D 1) (k : 1 =3D q) > : h @ k =3D (concat_1p p)^ @ (k @@ h) @ (concat_p1 q). > Proof. > by induction k; revert p h; rapply paths_ind_r. > Defined. > > Definition eckmann_hilton' {A : Type} {x : A} (h k : 1 =3D 1 :> (x =3D x)= ) : h @ k =3D k @ h > :=3D (horizontal_vertical h k) @ (horizontal_vertical' k h)^. > > > > On Mar 8, 2021, Kristina Sojakova wrote: > >> Dear all, >> >> I formalized my proof of syllepsis in Coq: >> https://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Coli= mits/Syllepsis.v >> >> >> I am looking forward to see how it compares to the argument Egbert has >> been working on. >> >> Best, >> >> Kristina >> >> On 3/8/2021 2:38 PM, Noah Snyder wrote: >> >> The generator of \pi_4(S^3) is the image of the generator of \pi_3 >> (S^2) under stabilization. This is just the surjective the part >> of Freudenthal. So to see that this generator has order dividing >> 2 one needs exactly two things: the syllepsis, and my follow-up >> question about EH giving the generator of \pi_3(S^2). This is why >> I asked the follow-up question. >> >> Note that putting formalization aside, that EH gives the generator >> of \pi_4(S^3) and the syllepsis the proof that it has order 2, are >> well-known among mathematicians via framed bordism theory (already >> Pontryagin knew these two facts almost a hundred years ago). So >> informally it=E2=80=99s clear to mathematicians that the syllepsis = shows >> this number is 1 or 2. Formalizing this well-known result remains >> an interesting question of course. >> >> Best, >> >> Noah >> >> On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke >> wrote: >> >> Dear Noah, >> >> I don't think that your claim that syllepsis gives a proof >> that Brunerie's number is 1 or 2 is accurate. Syllepsis gives >> you that a certain element of pi_4(S^3) has order 1 or 2, but >> it is an entirely different matter to show that this element >> generates the group. There could be many elements of order 2. >> >> Best wishes, >> Egbert >> >> On Mon, Mar 8, 2021 at 9:44 AM Egbert Rijke >> wrote: >> >> Hi Kristina, >> >> I've been on it already, because I was in that talk, and >> while my formalization isn't yet finished, I do have all >> the pseudocode already. >> >> Best wishes, >> Egbert >> >> On Sun, Mar 7, 2021 at 7:00 PM Noah Snyder >> wrote: >> >> On the subject of formalization and the syllepsis, has >> it ever been formalized that Eckman-Hilton gives the >> generator of \pi_3(S^2)? That is, we can build a >> 3-loop for S^2 by refl_refl_base --> surf \circ surf^ >> {-1} --EH--> surf^{-1} \circ surf --> refl_refl_base, >> and we want to show that under the equivalence \pi_3 >> (S^2) --> Z constructed in the book that this 3-loop >> maps to \pm 1 (which sign you end up getting will >> depend on conventions). >> >> There's another explicit way to construct a generating >> a 3-loop on S^2, namely refl_refl_base --> surf \circ >> surf \circ \surf^-1 \circ surf^-1 --EH whiskered refl >> refl--> surf \circ surf \circ surf^-1 \circ surf^-1 - >> -> refl_refl_base, where I've suppressed a lot of >> associators and other details. One could also ask >> whether this generator is the same as the one in my >> first paragraph. This should be of comparable >> difficulty to the syllepsis (perhaps easier), but is >> another good example of something that's "easy" with >> string diagrams but a lot of work to translate into >> formalized HoTT. >> >> Best, >> >> Noah >> >> On Fri, Mar 5, 2021 at 1:27 PM Kristina Sojakova >> wrote: >> >> Dear all, >> >> Ali told me that apparently the following problem >> could be of interest >> to some people >> (https://www.youtube.com/watch?v=3DTSCggv_YE7M&t=3D= 4350s): >> =20 >> >> Given two higher paths p, q : 1_x =3D 1_x, >> Eckmann-Hilton gives us a path >> EH(p,q) : p @ =3D q @ p. Show that EH(p,q) @ EH(q,p= ) >> =3D 1_{p@q=3Dq_p}. >> >> I just established the above in HoTT and am >> thinking of formalizing it, >> unless someone already did it. >> >> Thanks, >> >> Kristina >> >> -- >> 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/HomotopyTypeTheor= y/0aa0d354-7588-0516-591f-94ad920e1559%40gmail.com. >> =20 >> >> -- >> 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= O0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/1f7bbcb8-ee50-0c24-174e-d3852e52bbee%40gmail.com.