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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 18805 invoked from network); 8 Mar 2021 19:55:57 -0000 Received: from mail-pj1-x1040.google.com (2607:f8b0:4864:20::1040) by inbox.vuxu.org with ESMTPUTF8; 8 Mar 2021 19:55:57 -0000 Received: by mail-pj1-x1040.google.com with SMTP id w34sf279948pjj.7 for ; Mon, 08 Mar 2021 11:55:57 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1615233353; cv=pass; d=google.com; s=arc-20160816; b=sfU6gteJnSr2eJ2avcS/6jY6HFqwu4GF+0tecfEDTu6J8k+Xh2MgS7GtDl0Dt1LBc2 SB7Q/e99xDKApq0iBIB1sj3N9jk7ep1PuxRb5meh0ph411RCUCOcl71fyAE/mMmcwOeE qizDho4negEvN7z5QlxweMmd8KvNbxtb3ff8sJoA2wp+sDPT92zfVHoFu93DuC6PDapj BXua4OXLOF2bFl9O7DDJbYhrx5onJE7oJhdB79UWAonahLk9SvtLct8PEoUKbEV6gJUs 0rf72te/8GxnGce7jQbf/hm3ibIqUXsnLurvb6D7dcdP0tlkIweYiiVPMFE0somXLjgI 2Dvg== 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:reply-to:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-filter:dmarc-filter :dkim-signature; bh=yqlNM8EItvM8zJB0PE0zrSJ77dRutFAVjala64p8Gj8=; b=Vdt9AC8186PHRplve6NAFc30kI+cSf2hnltVIvXBmSKJjsXNSDyJ1nIfUR1N9dXWoM exbBPo5Pf1q4ZG+PHvufXUEg3nWpsTFbiUzSy7PGy/ZOt30dJ2M/E9E756kzwbFE1qmI PpvL5spf7BKVZb/TgsY+8GcdIM0g87ud5rVueYdI1vCgsc0m7tDMuPYXzaRogXEnPoOC 5y77iZsGaGDNJc9b0nYR83e/G4Skl8jwjf+wt9EwXU8VHvUyhGbczDR5HLMG3jU2IKyU jnV2ZzbJn9QOQFuqPHjN23+0n8D+YtuvuEp8t2qRYORlPMj1vrIFw+hQygFQXq8gQjMS ZI9w== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@umn.edu header.s=google header.b=c3b4uuM2; spf=pass (google.com: domain of kbh@umn.edu designates 134.84.196.206 as permitted sender) smtp.mailfrom=kbh@umn.edu; dmarc=pass (p=QUARANTINE sp=NONE dis=NONE) header.from=umn.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=dmarc-filter:dkim-filter:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:reply-to:precedence:mailing-list :list-id:list-post:list-help:list-archive:list-unsubscribe; bh=yqlNM8EItvM8zJB0PE0zrSJ77dRutFAVjala64p8Gj8=; b=aEU2vaKjaEzua/QUffcu1ygKHxh2AsNrlbTL2WITdQtJq0JSAmFBvK7KLR7QKC3emj u7PffjEFl+SXiKSlootHQa/sGPq0Wz+xG1AfofnmTIt/1MbUNuyJDYtTI+YTmDRUArnJ r/nYqEdZwHNnV94li5Kg38YdjpktCOXiicKEGlmDMzIBVrfCLdSGpEd73vztzjSr3jy7 Wgvsm+drDuowGA3oKOcSes6K3bNXV+eqW72NOxz8Rqh0GtSjrcV0r8tg62CYDfHdJ7Y+ HAJj0ijBfCIEVKZXQvcaDzlTebFCxaX5tlcMaVggsKNiBdKZAtrl2OFdPRHIgLbvjEtM vNNQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:dmarc-filter:dkim-filter:mime-version:references :in-reply-to:from:date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:reply-to:precedence:mailing-list :list-id:x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=yqlNM8EItvM8zJB0PE0zrSJ77dRutFAVjala64p8Gj8=; b=GZTXysdvKJlcEnfsQkJ+oKZNl5mUaouYud1ay0lHbOGDMibhDsJ4uUw4K9Llg842Un EIiWHAIMGN6IWGhPwCFmEMsa9c0XxJOMabb3SMSCpC+CdyW/Da+Bh6o/ckC7R/l2wEzp zOHK4A1mfoVLz4b6fUN4Fuil75trkoHRGlOAwX3sxWuycOiSeqILj8NxQBo6/ibVBw2p 2UncagYSXvg/Jc+QzjKR0+8odw2nqguk6jaOum0Nq/MP+uvcpSLRLTzDaP2I5pn/8k/V hAAEhgjlm1gw5rEtYy7YOIAT7MeS3N6ZN7poN+XTVSTBTNqmnULHMQgBwrXb9QA3ks5/ NkPw== X-Gm-Message-State: AOAM533x2S+zHAkLTYitxrDWXqCQ6PibReRVjQQMSQJI5Dh7sqXC/Oph mnknVIrGj+o1WSj46RMPvB0= X-Google-Smtp-Source: ABdhPJx7UnxB3IfxceBaiO/OHmbjHxBqRRuvM1vP6QNcZq7ebHR+mozxzGoB0Cu+ufBT3fkkONIUVw== X-Received: by 2002:a17:90b:798:: with SMTP id l24mr504060pjz.63.1615233353310; Mon, 08 Mar 2021 11:55:53 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:eb43:: with SMTP id i3ls8869457pli.7.gmail; Mon, 08 Mar 2021 11:55:52 -0800 (PST) X-Received: by 2002:a17:902:f702:b029:e3:5e25:85bb with SMTP id h2-20020a170902f702b02900e35e2585bbmr528654plo.56.1615233352627; Mon, 08 Mar 2021 11:55:52 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1615233352; cv=none; d=google.com; s=arc-20160816; b=e3u5hfRfmo8boTfC7PAnjBoJFsJqUP47eLRniapRK4LH4BYmVQDsPFRLec6hPPXZbz b7DxeAP8OroYokmX2z/4PXr1UfCdFjKIej2Lhlsgahzk/hMVHSbvWi8JUZj5MQUkxxrw oXOx2BzNHwDnL6yv5QcyAeP2OSVkel6/rxOtjS5pgBU3vUXCbC0gTfm9qMY+cvfegGbo bOa4G14+Y5+vHo8ZctLHV719UxQ1WDCCCzO5P7BmkagTiTso1beSjwy4/E/OmJX12y6V JpKEal+OreTioQCH9mrRFO6/VhA7tel2B8vPufg/RSkpcge0XyJ7SSMKouCH2JI0ZPNq Idgg== 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:dkim-filter:dmarc-filter; bh=ZBYOqkNMajBj5LavW94asopeP64BKsqpkuxy2HAizSc=; b=MUzb1fH20/qqtOV/Adkvp+a0SPfiHB0RjldDAlhAVoc9FKkOyn5h7k8OLn01ygPgmp 5Z/F+HXpUOwYqeUDpaw2v677BgJCaOcHT4M1gC/b2qDefWkAQ6v3whkRWreY6xRWD4yY v2n3aDMdsuq5H0fQcA2Jn6L8cD9U7lVQJfYMRXW9q8bUBmjLWF4jrxH6QGvZnDx40WAl cfgJ+zYvqK+RXor9AGKepC4lP0HNKFywhv66in4/HZR348R2e7b0ls5H5/JoOBhP7+D7 ZBxtZxEikH7hV9vENMkIaoWoJRZ8meMr0yA9T+gvZHrrAUxIUQ3IhHUBWhVEzwRT+zh3 06iw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@umn.edu header.s=google header.b=c3b4uuM2; spf=pass (google.com: domain of kbh@umn.edu designates 134.84.196.206 as permitted sender) smtp.mailfrom=kbh@umn.edu; dmarc=pass (p=QUARANTINE sp=NONE dis=NONE) header.from=umn.edu Received: from mta-p6.oit.umn.edu (mta-p6.oit.umn.edu. [134.84.196.206]) by gmr-mx.google.com with ESMTPS id r7si94886pjp.3.2021.03.08.11.55.52 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 08 Mar 2021 11:55:52 -0800 (PST) Received-SPF: pass (google.com: domain of kbh@umn.edu designates 134.84.196.206 as permitted sender) client-ip=134.84.196.206; Received: from localhost (unknown [127.0.0.1]) by mta-p6.oit.umn.edu (Postfix) with ESMTP id 4DvTbr0BZwz9vC7r for ; Mon, 8 Mar 2021 19:55:52 +0000 (UTC) X-Virus-Scanned: amavisd-new at umn.edu Received: from mta-p6.oit.umn.edu ([127.0.0.1]) by localhost (mta-p6.oit.umn.edu [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id P1fN0BuJzP7v for ; Mon, 8 Mar 2021 13:55:51 -0600 (CST) Received: from mail-yb1-f198.google.com (mail-yb1-f198.google.com [209.85.219.198]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mta-p6.oit.umn.edu (Postfix) with ESMTPS id 4DvTbq3Z3hz9vC82 for ; Mon, 8 Mar 2021 13:55:51 -0600 (CST) DMARC-Filter: OpenDMARC Filter v1.3.2 mta-p6.oit.umn.edu 4DvTbq3Z3hz9vC82 DKIM-Filter: OpenDKIM Filter v2.11.0 mta-p6.oit.umn.edu 4DvTbq3Z3hz9vC82 Received: by mail-yb1-f198.google.com with SMTP id j4so13942656ybt.23 for ; Mon, 08 Mar 2021 11:55:51 -0800 (PST) X-Received: by 2002:a25:6e02:: with SMTP id j2mr34893666ybc.247.1615233350883; Mon, 08 Mar 2021 11:55:50 -0800 (PST) X-Received: by 2002:a25:6e02:: with SMTP id j2mr34893640ybc.247.1615233350591; Mon, 08 Mar 2021 11:55:50 -0800 (PST) MIME-Version: 1.0 References: <0aa0d354-7588-0516-591f-94ad920e1559@gmail.com> <7d4b6fd7-3035-e0b9-c966-97dd89d8b457@gmail.com> <87blbtk7ey.fsf@uwo.ca> <8de81acf-3a00-ae98-7003-9eaf404d0b89@gmail.com> In-Reply-To: From: "'Favonia' via Homotopy Type Theory" Date: Mon, 8 Mar 2021 13:55:14 -0600 Message-ID: Subject: Re: [HoTT] Syllepsis in HoTT To: Egbert Rijke Cc: Kristina Sojakova , Homotopy Type Theory , Dan Christensen Content-Type: multipart/alternative; boundary="000000000000177d0b05bd0bd21d" X-Original-Sender: kbh@umn.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@umn.edu header.s=google header.b=c3b4uuM2; spf=pass (google.com: domain of kbh@umn.edu designates 134.84.196.206 as permitted sender) smtp.mailfrom=kbh@umn.edu; dmarc=pass (p=QUARANTINE sp=NONE dis=NONE) header.from=umn.edu X-Original-From: Favonia Reply-To: Favonia 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: , --000000000000177d0b05bd0bd21d Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I remember multiple people (including me) discovered relatively short proofs. Some history on GitHub: https://github.com/HoTT/book/issues/27 Best, Favonia they/them/theirs On Mon, Mar 8, 2021 at 10:54 AM Egbert Rijke wrote: > My agda file with the the interchange laws and EH is here > > https://github.com/HoTT-Intro/Agda/blob/master/extra/interchange.agda > > And the coherence law is here > > https://github.com/HoTT-Intro/Agda/blob/master/extra/syllepsis.agda > > For anyone who is interested. > > On Mon, Mar 8, 2021 at 5:38 PM Kristina Sojakova < > sojakova.kristina@gmail.com> wrote: > >> If I'm not mistaken, Favonia also found a very short proof of EH some >> 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 ha= s >> >> 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 dividin= g >> >> 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 w= hy >> >> I asked the follow-up question. >> >> >> >> Note that putting formalization aside, that EH gives the generat= or >> >> of \pi_4(S^3) and the syllepsis the proof that it has order 2, a= re >> >> well-known among mathematicians via framed bordism theory (alrea= dy >> >> Pontryagin knew these two facts almost a hundred years ago). So >> >> informally it=E2=80=99s clear to mathematicians that the sylleps= is shows >> >> this number is 1 or 2. Formalizing this well-known result remai= ns >> >> 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 give= s >> >> you that a certain element of pi_4(S^3) has order 1 or 2, bu= t >> >> 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, h= as >> >> 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_bas= e, >> >> 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 generati= ng >> >> a 3-loop on S^2, namely refl_refl_base --> surf \cir= c >> >> surf \circ \surf^-1 \circ surf^-1 --EH whiskered ref= l >> >> 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 proble= m >> >> could be of interest >> >> to some people >> >> ( >> https://www.youtube.com/watch?v=3DTSCggv_YE7M&t=3D4350s): >> >> >> >> >> >> 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 receivin= g >> >> 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/0aa0d354-7588-0516-= 591f-94ad920e1559%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/CAO0tDg7MCVQWLfSf13= PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.com >> . >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email 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 >> . >> > -- > 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/CAGqv1ODEzmBLWmOvgVm= tBO7D_xttUKDW6NSNF2Q2_3K7wfYcCA%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/CAH_%2Brvd184QS__yNafR5835opTA6DiZ1Wy%2BuGsDKp3%3DtG0TWP= w%40mail.gmail.com. --000000000000177d0b05bd0bd21d Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I remember multiple people (including me) discovered = relatively short proofs. Some history on GitHub: https://github.com/HoTT/book/iss= ues/27

Best,
Fa= vonia
they/them/theirs
<= /div>


On Mon, Mar 8, 2021 at 10:54 A= M Egbert Rijke <e.m.rijke@gmail.com> wrote:
My a= gda file with the the interchange laws and EH is here

https://github.com/HoTT-Intro/Agda/blob/master/extra= /interchange.agda

And the coherence law is= here


For anyone who is interested.

On Mon, Mar 8, 2021 at 5:38= PM Kristina Sojakova <sojakova.kristina@gmail.com> wrote:
If I'm not mistaken, Favonia= also found a very short proof of EH some
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.<= br> >
> Dan
>
>
> Definition horizontal_vertical {A : Type} {x : A} {p q : x =3D x} (h := p =3D 1) (k : 1 =3D q)
>=C2=A0 =C2=A0 : h @ k =3D (concat_p1 p)^ @ (h @@ k) @ (concat_1p q). > Proof.
>=C2=A0 =C2=A0 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)
>=C2=A0 =C2=A0 : h @ k =3D (concat_1p p)^ @ (k @@ h) @ (concat_p1 q). > Proof.
>=C2=A0 =C2=A0 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
>=C2=A0 =C2=A0 :=3D (horizontal_vertical h k) @ (horizontal_vertical'= ; k h)^.
>
>
>
> On Mar=C2=A0 8, 2021, Kristina Sojakova <sojakova.kristina@gmail.com> = wrote:
>
>> Dear all,
>>
>> I formalized my proof of syllepsis in Coq:
>> htt= ps://github.com/kristinas/HoTT/blob/kristina-pushoutalg/theories/Colimits/S= yllepsis.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:
>>
>>=C2=A0 =C2=A0 =C2=A0 The generator of \pi_4(S^3) is the image of th= e generator of \pi_3
>>=C2=A0 =C2=A0 =C2=A0 (S^2) under stabilization.=C2=A0 This is just = the surjective the part
>>=C2=A0 =C2=A0 =C2=A0 of Freudenthal.=C2=A0 So to see that this gene= rator has order dividing
>>=C2=A0 =C2=A0 =C2=A0 2 one needs exactly two things: the syllepsis,= and my follow-up
>>=C2=A0 =C2=A0 =C2=A0 question about EH giving the generator of \pi_= 3(S^2).=C2=A0 This is why
>>=C2=A0 =C2=A0 =C2=A0 I asked the follow-up question.
>>
>>=C2=A0 =C2=A0 =C2=A0 Note that putting formalization aside, that EH= gives the generator
>>=C2=A0 =C2=A0 =C2=A0 of \pi_4(S^3) and the syllepsis the proof that= it has order 2, are
>>=C2=A0 =C2=A0 =C2=A0 well-known among mathematicians via framed bor= dism theory (already
>>=C2=A0 =C2=A0 =C2=A0 Pontryagin knew these two facts almost a hundr= ed years ago).=C2=A0 So
>>=C2=A0 =C2=A0 =C2=A0 informally it=E2=80=99s clear to mathematician= s that the syllepsis shows
>>=C2=A0 =C2=A0 =C2=A0 this number is 1 or 2.=C2=A0 Formalizing this = well-known result remains
>>=C2=A0 =C2=A0 =C2=A0 an interesting question of course.
>>
>>=C2=A0 =C2=A0 =C2=A0 Best,
>>
>>=C2=A0 =C2=A0 =C2=A0 Noah
>>
>>=C2=A0 =C2=A0 =C2=A0 On Mon, Mar 8, 2021 at 3:53 AM Egbert Rijke &l= t;e.m.rijke@gmail.= com>
>>=C2=A0 =C2=A0 =C2=A0 wrote:
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Dear Noah,
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 I don't think that your clai= m that syllepsis gives a proof
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 that Brunerie's number is 1 = or 2 is accurate. Syllepsis gives
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 you that a certain element of pi= _4(S^3) has order 1 or 2, but
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 it is an entirely different matt= er to show that this element
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 generates the group. There could= be many elements of order 2.
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Best wishes,
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Egbert
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 On Mon, Mar 8, 2021 at 9:44 AM E= gbert Rijke
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 <e.m.rijke@gmail.com> wrote:
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Hi Kristina,
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 I've been on i= t already, because I was in that talk, and
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 while my formaliza= tion isn't yet finished, I do have all
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 the pseudocode alr= eady.
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Best wishes,
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Egbert
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 On Sun, Mar 7, 202= 1 at 7:00 PM Noah Snyder
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 <nsnyder@gmail.com> wrote: >>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 On t= he subject of formalization and the syllepsis, has
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 it e= ver been formalized that Eckman-Hilton gives the
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 gene= rator of \pi_3(S^2)?=C2=A0 That is, we can build a
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 3-lo= op for S^2 by refl_refl_base --> surf \circ surf^
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 {-1}= --EH--> surf^{-1} \circ surf -->=C2=A0 refl_refl_base,
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 and = we want to show that under the equivalence \pi_3
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 (S^2= ) --> Z constructed in the book that this 3-loop
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 maps= to \pm 1 (which sign you end up getting will
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 depe= nd on conventions).
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Ther= e's another explicit way to construct a generating
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 a 3-= loop on S^2, namely refl_refl_base --> surf \circ
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 surf= \circ \surf^-1 \circ surf^-1 --EH whiskered refl
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 refl= --> surf \circ surf \circ surf^-1 \circ surf^-1 -
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 ->= ; refl_refl_base, where I've suppressed a lot of
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 asso= ciators and other details.=C2=A0 One could also ask
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 whet= her this generator is the same as the one in my
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 firs= t paragraph.=C2=A0 This should be of comparable
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 diff= iculty to the syllepsis (perhaps easier), but is
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 anot= her good example of something that's "easy" with
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 stri= ng diagrams but a lot of work to translate into
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 form= alized HoTT.
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Best= ,
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 Noah=
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 On F= ri, Mar 5, 2021 at 1:27 PM Kristina Sojakova
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 <= sojakova.k= ristina@gmail.com> wrote:
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Dear all,
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Ali told me that apparently the following problem
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 could be of interest
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 to some people
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 (https://www.youtube.com/watc= h?v=3DTSCggv_YE7M&t=3D4350s):
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Given two higher paths p, q : 1_x =3D 1_x,
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Eckmann-Hilton gives us a path
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 EH(p,q) : p @ =3D q @ p. Show that EH(p,q) @ EH(q,p)
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 =3D 1_{p@q=3Dq_p}.
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 I just established the above in HoTT and am
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 thinking of formalizing it,
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 unless someone already did it.
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Thanks,
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Kristina
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 --
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 You received this message because you are
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 subscribed to the Google Groups "Homotopy Type
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 Theory" group.
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 To unsubscribe from this group and stop receiving
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 emails from it, send an email to
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 HomotopyTypeTheory+unsubscribe@googlegroups.com.=
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 To view this discussion on the web visit
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0 https://groups.google.com/d/msgid/HomotopyTypeTheory/0aa0d354-7= 588-0516-591f-94ad920e1559%40gmail.com.
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2= =A0 =C2=A0
>>
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 -- >>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 You = received this message because you are subscribed
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 to t= he Google Groups "Homotopy Type Theory" group.
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 To u= nsubscribe from this group and stop receiving
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 emai= ls from it, send an email to
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 HomotopyTypeTheory+unsubscribe@googlegroups.com.
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 To v= iew this discussion on the web visit
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 https://groups.google.com/d/msgid/HomotopyTypeTheory/C= AO0tDg7MCVQWLfSf13PvEu%2BUv1mP2A%2BbbNGanKbwHx446g_hYQ%40mail.gmail.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/msgid= /HomotopyTypeTheory/8de81acf-3a00-ae98-7003-9eaf404d0b89%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/msgid/HomotopyTypeTheory/CAGqv1ODEz= mBLWmOvgVmtBO7D_xttUKDW6NSNF2Q2_3K7wfYcCA%40mail.gmail.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/msgid/HomotopyTypeTheory/CAH_%2Brvd184QS__yNafR5835o= pTA6DiZ1Wy%2BuGsDKp3%3DtG0TWPw%40mail.gmail.com.
--000000000000177d0b05bd0bd21d--