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 27188 invoked from network); 8 Mar 2021 16:38:17 -0000 Received: from mail-wm1-x339.google.com (2a00:1450:4864:20::339) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 16:38:17 -0000 Received: by mail-wm1-x339.google.com with SMTP id n22sf2249318wmo.7 for ; Mon, 08 Mar 2021 08:38:17 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615221495; cv=pass; d=google.com; s=arc-20160816; b=m5eTSqqvrgdP5VYyJOB9TZEhRf05EcSUZv3BWB8E/SAiii7r0Akaycypujiztmn4dG muj+3u2AmnjZ4IVkFEwwAAtDX3ht9EksLrIygjTn2kNcoGwxvFZkQsq9Vtavs8bxVFsv v9aRkbeZsbNQvSfWgndChY+de0oniyUqmxPiiqIh8OJvq8Kzjnqzp3oeqeoBUUNymmJP BQHU0aCfmUz3TYia83O8ybu9JbGEOXDUhmQMpzvxua1T+gY4N1Diy3tOFmWWa4GBAnX/ w3cLtmgAtxhTJ/mFllzxekR1bGxe/VM1VEw0VOvE9A/36agUIJQibzeCTU1gTAYyB+zT Mw5w== 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=gB8G+Hvu9LiVwLBZ794qW3FHqKPJYdGASwVTheHEu9w=; b=BpOXtdtEdy9YKcSCtvHoPq/0pH92cKqOZ/8tD1yQwkUiZlFAnphp1Oec3vm80AUJYE glweDY4Ol1+fHozjlK5VbfztJaoY5fa3IdRsdxoqMdatn4tNN73JZF4zZYkd0arChuT3 JH4r9DoDG5L/qj47xRnMXFX9nSDiNSl76Nl+q0y8KGkcA82RpxMg6161fYY/6zP6frDF J/YjVffzo6o3dyFu1ga4Y2Qv+zEN0ur8MR/3Z31b2g7GnH64ahESmHIjR2eHppEfit8y Ytu3TlwbaPLGGoLHFLorKsKRQ+b+3ngHysdogbvg8PYcFhb7K8TuifFXDYrcyUKWj8bl EH7Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=F39k+qg6; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::434 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=gB8G+Hvu9LiVwLBZ794qW3FHqKPJYdGASwVTheHEu9w=; b=HtmaPx/8iYmjmVBz6s6IVyk1nenCSpTwvpzGMsvdzk0eD9uGpiVjo6naRwrXvRCdQj 8Vq+7vbbdQ4ygXzWx0XtvFk3cd79hoy403fQBwO5ECnKxQ8uFe9CLzV2irPTTvjnpwJ+ 0zHg662prAuV6x+VQF1EMJv+TT9sZ9vghgFsDGvr+DGvDwi+926pdPXiQS4FNFV11mXF UvNv5uw9XDgaJKT1k9xJ98DFjzVQvx1yyrD5VOd5D1eB1pymW9Js/5y6kXMsbq13tu6m XXrTFuU8oFUcAVpIho4VHOg+QAczYGITUxfCPArib7BLmJGTqT3xSbrhXODh6QHSQrIg /oXQ== 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=gB8G+Hvu9LiVwLBZ794qW3FHqKPJYdGASwVTheHEu9w=; b=Nr4xvOiTpctW4cQ/qW1IRgM3GrNWyjZO1dc035tRCPIyqD6yuVSlboXNDuSf+8Jn9j ouBK7d314aT7vtk7Yz82gUXE7jhU4W44znvoA1d9IeNyY/NQ28mvq3qP8+pVHy1UENii jX9gokWFxqouW8bLMfT/j6DH7N0EAAZEfAG4s3tDFGwDQJjFUM7XuL/AupfKnKjuzaJx rzZSSpo37F0IliRE990h62Sn8Tov/34lS1qqkziy1e8U3pVQrUMtxKEcOcj9F7EIookM ApQhq4ae+8znRI1dQohiGYwNSHuLs1tGhVTqgqVFaOtmTabZQHAv3fsIVIiMjTqmILDd BTrw== 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=gB8G+Hvu9LiVwLBZ794qW3FHqKPJYdGASwVTheHEu9w=; b=QnS0WZq9EgkhwYdkN4j31wNgnMp4Q8qL0A62lt2+FhJV7QoZpCFT56evvfBwF5AvvN LLyTnR6zd6kwo2gh27EuiGIrn1hL/iWjJs4qQIkBJSar/sOkRShGZxMHYZ7DvAHt8ucu vrtuhD8Q8OBzG3WIvJypKEL02V4z8lG0fV+wN9yq9d/W965+qjhhn6mxzvycvRsCotD6 kvYEZ+G3O67UO4s5CUKi5L97IeA5POAU3l0wFNK40HYig9bPm8sgw6ss1udZUS+THo9g 3aZYQMvyxVq15rSSNcVl/DDQ1hB9uvWfQsEUsYaUnfU/rFK0/HdLDwu2ixNbywfJlFvS 8UVg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530nt2pROhueZFvBoZpzJ6gZ2tv7ZjhrsdRIaOlBSqscti4PvyIi ql/60/O7rzn62bGcrAlCyIs= X-Google-Smtp-Source: ABdhPJy5CpxmwSJ2u35BJFls50oSDg5a4/XNvPCuLWy9raWlcSc1OJV+u79RRo/M6H1TT/6AjTW5Bw== X-Received: by 2002:a05:600c:289:: with SMTP id 9mr23236307wmk.135.1615221495515; Mon, 08 Mar 2021 08:38:15 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:58f0:: with SMTP id f16ls10525457wrd.0.gmail; Mon, 08 Mar 2021 08:38:14 -0800 (PST) X-Received: by 2002:a5d:6b47:: with SMTP id x7mr24316242wrw.170.1615221494500; Mon, 08 Mar 2021 08:38:14 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615221494; cv=none; d=google.com; s=arc-20160816; b=rg276w0lML50MiuiO4jt1gjToqkU6cnbncFXcdG2PJOrDauGEJNl0ZKx4XX6HOiIoz dkEzyw9nYStdY/B2DdPkTh6FABdNC5jXKdoyCstWC/f8uguzQZjgfCFd9Tkt9YUzFSLZ hZnJtTX0wymtrsfzafSNtP/ESMhGhXmQO8CCoweh6B9o3ZQbQgSc70CynIgUG/ZapuNj WjuF6PgPe505ajLfA/54O5qQvb+IWDP0mL/JRubEAZAwKsZVBprrCyA6LEAE8jsDiGHQ to0RBUvx2rHchhSOC2hSS7imNNpH33pL0AezPBuXGayInTq/hQJmsa7R2DbIMLJGrj63 Zi0g== 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=CzwaL3fs4U/LnqQZOw3wq5p/UMp195ls/V1PReI3r6o=; b=n65q2gtRXkwmu8jMPOReSxmxFQG3zdmmuSUxTavnKmAgQlNbTXCE0NttalJKq6FpCN ly8Ba++/Nf8SR/7sr+tBkTfR+cxwYOSUP+Tlp21bBrqciAEwdivKBP0iyesyY2/dJexn vSjx7zBY4nPMBgT2yUyDK95qUtUXYkS19GfEXNsESuy2aPdpy99R3V32kRspUTR+lwqS OljkhPpUMJvZnxtWBA+oga/YQkCyAfKe9NgKvc5PajqFpEwWm62fdfy4gi4TycebEoxD LydrpfJ0G6k/t4S2GnJJgl5j4RbPex/q9q4gbGyn/bud5RbQt5Ofjs8qo5IJQqui7eaF gy6g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=F39k+qg6; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::434 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-x434.google.com (mail-wr1-x434.google.com. [2a00:1450:4864:20::434]) by gmr-mx.google.com with ESMTPS id s8si516076wrn.5.2021.03.08.08.38.14 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 08:38:14 -0800 (PST) Received-SPF: pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::434 as permitted sender) client-ip=2a00:1450:4864:20::434; Received: by mail-wr1-x434.google.com with SMTP id v15so12138799wrx.4 for ; Mon, 08 Mar 2021 08:38:14 -0800 (PST) X-Received: by 2002:adf:f186:: with SMTP id h6mr23952914wro.290.1615221493693; Mon, 08 Mar 2021 08:38:13 -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 j16sm605674wmi.2.2021.03.08.08.38.12 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Mon, 08 Mar 2021 08:38:13 -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: <8de81acf-3a00-ae98-7003-9eaf404d0b89@gmail.com> Date: Mon, 8 Mar 2021 17:38:12 +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=F39k+qg6; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2a00:1450:4864:20::434 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: , If I'm not mistaken, Favonia also found a very short proof of EH some=20 years ago. 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/8de81acf-3a00-ae98-7003-9eaf404d0b89%40gmail.com.