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 15551 invoked from network); 8 Feb 2022 20:20:25 -0000 Received: from mail-ot1-x33a.google.com (2607:f8b0:4864:20::33a) by inbox.vuxu.org with ESMTPUTF8; 8 Feb 2022 20:20:25 -0000 Received: by mail-ot1-x33a.google.com with SMTP id g24-20020a9d6198000000b005a620c9727bsf72191otk.6 for ; Tue, 08 Feb 2022 12:20:25 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1644351623; cv=pass; d=google.com; s=arc-20160816; b=yH+oRRNt6a+Ym6oDNFyOnQ67OeH0QybP/g5zuuD1ROCNPV+sbybe8mYyo425lPV4ms qSvaKkTRHHnbK8WZf1Br/csonNxAIBdYVc5ounQV5n3XLKr0/I9FnzioCnJ8LLPXkF6u jqoBfcTdIxAZbSeZ+T0hJBCCM59FI8JmTXaH6M4vq7FVazJ0fDLLXVYAZX7OmjCPdXw+ Wj36CGsmuoeIt/2dyPkHNYXPyuPapPbTbLxPu0RtlaU9T1mfjrasbauee2gYLUL8Cvpf jEX9N4ONbrbl1U+lRD9ifstXGq6NYi6c9KqlV4suQnSJukQhG8EC9R6gY7m3jproBl00 Mknw== 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:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=4aJ3czCc97Yr06QcQaL+vQuWuBCGTSSz1UuZozIRQXI=; b=yfLi1V85DQfB1cJxbQVrYi1HVCYGmKeIuVlsFGfGtoEZPLxNPE0ePEFEySnOKCmC+A gAWLcinLP2N6to3vWnKZbD+eOK9CxpzILUTaKvvuTTme4Yg9IC66+tTQNrU8XJwEt0on 9BfFb0vCjphJqWR4bJfDpCk6xPyp2Bmam2nbLxeINlMki9wnVW6Is4hlm/6IyU/kX1r7 Q5jMYHRrTuRFAnBi0u1HDgfWmD0+7tbwcokGAG+gu47oK3qgfcwvsLXccjulLISBF92m i0FQTaraFtxr5hp2XuQthxI9HYwvpzuCfU5zxknT43V7m+PNmsxNWgUD35qHXLm85sNV 6Paw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=QRSTyhl4; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::e2f as permitted sender) smtp.mailfrom=andersmortberg@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=20210112; h=sender:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-subscribe:list-unsubscribe; bh=4aJ3czCc97Yr06QcQaL+vQuWuBCGTSSz1UuZozIRQXI=; b=WjCeVL56DEFO453r/7rtpAh/4G+HLf+svkGOWQkg9t/R3sp2SL6NS10hvSneYdcLE7 XDVMuvkXH99oekSoTiWXjKxCyGxH2YrE7QZEqUGzsMNbc2j963BMQhv64Z3EJzyZSsLx UVtx7Lt/u4awtGaQ6oWCrwX6EuvdqIveUi0/0ktnPdMJPZjg8FLjhaP5yUx6z9tphzWp 0j2GFVUoapwszOvIOyTUYAmjWP3JNZ1gs+L7hEDFF89+/2sqqBS55s2c1bxyZZBtZvJZ m8U/p13+yUWVzR5E8uOXuu3WER97ZEsiwXbzhdF6CcuQPUI5wh3/gq1tvODFrDKYTO98 XA6Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20210112; h=mime-version:from:date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=4aJ3czCc97Yr06QcQaL+vQuWuBCGTSSz1UuZozIRQXI=; b=byytktJfMPPcCziSw7N227HV24Obwqv/P+dMnSP1FwTC/AFaZFfguzXsZuorC2S/Nu G1vdNohlhdZpgGIwo36ZY4ZJe38WPC5JipGTrWnbJaDc+oa9sNltbX+CCWcMqw4IbGoq hrvdCeMYJxh7dRYfhTHvV0eYZpoNe8CWn0BUHmLlmPnVuxEBSoHeu9az8Mi2ddh7GqW7 ThsgIhxINfoNxsrp70rW1m3vrLJCnwoBF3sXmpFqbjvOQ7m5g6CK0Pxe4bpYbvaKwChK G6LkQYZ6Np9nx/qtrLY8lmx8HfryNjmLFqam71BkKLAxIT4rspQAAA3zggZ8J/frSVWs lE1Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-subscribe:list-unsubscribe; bh=4aJ3czCc97Yr06QcQaL+vQuWuBCGTSSz1UuZozIRQXI=; b=hd8cx0gz0zu4iN87h9Gj/gwFOc7qPXeYeXM0GiIfZweUVQhtL6tpgQKKSNWT+iakp6 buIt3n+OzE7aaozxQzw2fUWAdKKDFEjDYK1s0K35EC4RCQTVOnF/m0wybiuqQM3UuSJW i6pmTXLijYmlKq0fQGIDLE+vnJeHLqbhmaanXlPUEh3R8P0V39eonTsHcvbWUjE/W06/ wc7GrqhBDEWVZLvzXwUIa5TDjFD6vubmmMZ88cScVTJlC8Y+iokE68Ejl3R41bTZ+lOy p3xDZGribqEcrG6UEJcB2Hne4FzhgXrePIYYsyb16JFqCbTDz2HzLdgtA9mV58cJG1LQ +h0g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM530L7Mce+ZbuoGDSwM/Y40sGVEm8qP4K2bYNnvdK+Z9uwKb8iyyd H9dURhZFn3Lww/BPEqPda6g= X-Google-Smtp-Source: ABdhPJzzfu8uH4KFg9EtThwP7jx2FtBYzltXD+CXleR0sGhvVJWWzNGdvh1XUG/Zuq8U0PhYyJe25Q== X-Received: by 2002:a05:6830:1084:: with SMTP id y4mr2487058oto.42.1644351623101; Tue, 08 Feb 2022 12:20:23 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6830:44a2:: with SMTP id r34ls1944239otv.4.gmail; Tue, 08 Feb 2022 12:20:22 -0800 (PST) X-Received: by 2002:a9d:6f8d:: with SMTP id h13mr2505626otq.309.1644351622051; Tue, 08 Feb 2022 12:20:22 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1644351622; cv=none; d=google.com; s=arc-20160816; b=aWlzoV4HH8rRDN22viAhhZyvyvw3ZwWPuXOTN23t0nqUaOoGNl/v1fTrug7YXV0VPs zb4TQl3TDHcodd1CCdLSM/c3Vxvmown0DlF2LhTwL7AnNXrEELAXCxEcasl22M1meB9A tCZKZdgtfju4t2nlfNGeSalj1f1tQukujE7gAUrobv/J3r8hRdL/Iv880OFxoGuHabxc yVdkb1MJLHjyr1JAOIQq8hTuFo6vf/BSQzIkjyQ5Ie8OP7kx7dP3diEBgop3cgWj1Mlc 3L1+8xUFLU4/BkH94UhSlopLtS3lxaNy6XHFDrkDdLtLnjH9P9TsHEdf0oyrxRpBUzmA f1OQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=kiC/CAUp2FimUvKzcuahxRjxCru1JXRx9f8cvOxSBWA=; b=QdwvpagqmQssUI3XnK/GJpQDgKtOb8TkUEU4HWSlg6w8QrLxoww8R9tDQo6r9nN7WL ZsbARraVd/wXbOwYVePPsN9IBBgGVxU9NsXWxYiKVrgGdB26DqG61zE/17X7Uq41GzMV LD6YCHZ4eM06OJv991KJz3CFghaCSOfknxgPb1QTOR113kYy81FXMw+kYsVl9vuuUB45 V/lccVOH09JnibzFjPzxItI913KdXGBtvsW4SiLFnAyWnQQ6UoZBsT10/Z8Ssb07sVH4 FoJ3+VfTwc/3dssqyHwhTm5JMyiOrSYZ1OjBLK3FFHQ5ZkKP4Enk9hKIWd3LEt55Wv6Q 8aMg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=QRSTyhl4; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::e2f as permitted sender) smtp.mailfrom=andersmortberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-vs1-xe2f.google.com (mail-vs1-xe2f.google.com. [2607:f8b0:4864:20::e2f]) by gmr-mx.google.com with ESMTPS id cv39si92111oab.2.2022.02.08.12.20.22 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 08 Feb 2022 12:20:22 -0800 (PST) Received-SPF: pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::e2f as permitted sender) client-ip=2607:f8b0:4864:20::e2f; Received: by mail-vs1-xe2f.google.com with SMTP id v6so245272vsp.11 for ; Tue, 08 Feb 2022 12:20:22 -0800 (PST) X-Received: by 2002:a05:6102:3590:: with SMTP id h16mr2037904vsu.63.1644351621296; Tue, 08 Feb 2022 12:20:21 -0800 (PST) MIME-Version: 1.0 From: Anders Mortberg Date: Tue, 8 Feb 2022 21:19:45 +0100 Message-ID: Subject: =?UTF-8?B?W0hvVFRdIEZvcm1hbGl6YXRpb24gb2Ygz4DigoQoU8KzKeKJheKEpC8y4oSkIGluIEN1Yg==?= =?UTF-8?B?aWNhbCBBZ2RhIGNvbXBsZXRlZA==?= To: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000045f6ec05d78772f5" X-Original-Sender: andersmortberg@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20210112 header.b=QRSTyhl4; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::e2f as permitted sender) smtp.mailfrom=andersmortberg@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: , --00000000000045f6ec05d78772f5 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable We are happy to announce that we have finished a formalization of =CF=80=E2=82=84(S=C2=B3)=E2=89=85=E2=84=A4/2=E2=84=A4 in Cubical Agda. Mos= t of the code has been written by my PhD student Axel Ljungstr=C3=B6m and the proof largely follows Guillaume Bruner= ie's PhD thesis. For details and a summary see: https://github.com/agda/cubical/blob/master/Cubical/Homotopy/Group/Pi4S3/Su= mmary.agda The proof involves a lot of synthetic homotopy theory: LES of homotopy groups, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey, Z-cohomology (with graded commutative ring structure), Gysin sequence, the Hopf invariant, Whitehead product... Most of this was written by Axel under my supervision, but some results are due to other contributors to the library, in particular Lo=C3=AFc Pujet (3x3 lemma for pushouts, total space= of Hopf fibration), KANG Rongji (Blakers-Massey), Evan Cavallo (Freudenthal and lots of clever cubical tricks). Our proof also deviates from the one in Guillaume's thesis in two major ways: 1. We found a direct encode-decode proof of a special case of corollary 3.2.3 and proposition 3.2.11 which is needed for =CF=80=E2=82=84(S=C2=B3). = This allows us to completely avoid the use of the James construction of Section 3 in the thesis (shortening the pen-and-paper proof by ~15 pages), but the price we pay is a less general final result. 2. With Guillaume we have developed a new approach to Z-cohomology in HoTT, in particular to the cup product and cohomology ring (see https://drops.dagstuhl.de/opus/volltexte/2022/15731/). This allows us to give fairly direct construction of the graded commutative ring H*(X;Z), completely avoiding the smash product which has proved very hard to work with formally (and also informally on pen-and-paper as can be seen by the remark in Guillaume's thesis on page 90 just above prop. 4.1.2). This simplification allows us to skip Section 4 of the thesis as well, shortening the pen-and-paper proof by another ~15 pages. This then leads to various further simplifications in Section 5 (Cohomology) and 6 (Gysin sequence). With these mathematical simplifications the proof got a lot more formalization friendly, allowing us to establish an equivalence of groups by a mix of formal proof and computer computations. In particular, Cubical Agda makes it possible to discharge several small steps in the proof involving univalence and HITs purely by computation. This even reduces some gnarly path algebra in the Book HoTT pen-and-paper proof to "refl". Regardless of this, we have not been able to reduce the whole proof to a computation as originally conjectured by Guillaume. However, if someone would be able to do this and compute that the Brunerie number is indeed 2 purely by computer computation there would still be the question what this has to do with =CF=80=E2=82=84(S=C2=B3). Establishing this connection forma= lly would then most likely involve formalizing (large) parts of what we have managed to do here. Furthermore, having a lot of general theory formalized will enable us to prove more results quite easily which would not be possible from just having a very optimized computation of a specific result. Best regards, Anders and Axel --=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/CAMWCppmb%2BAt_Bwp_2USKH9dAigFGx0GBrcG3XQQaqZmkr-kHog%40= mail.gmail.com. --00000000000045f6ec05d78772f5 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
We are happy to announce that we have finished a formaliza= tion of=C2=A0=20 =CF=80=E2=82=84(S=C2=B3)=E2=89=85=E2=84=A4/2=E2=84=A4=C2=A0 in Cubical Agda= . Most of the code has been written by my=20 PhD student Axel Ljungstr=C3=B6m and the proof largely follows Guillaume=20 Brunerie's PhD thesis. For details and a summary see:

https://github.com/agda/cubical/blob/master/= Cubical/Homotopy/Group/Pi4S3/Summary.agda

The proof involves a lot of synthetic homotopy theory: LES of homotopy=20 groups, Hopf fibration, Freudenthal suspension theorem, Blakers-Massey,=20 Z-cohomology (with graded commutative ring structure), Gysin sequence,=20 the Hopf invariant, Whitehead product... Most of this was written by=20 Axel under my supervision, but some results are due to other=20 contributors to the library, in particular Lo=C3=AFc Pujet (3x3 lemma for= =20 pushouts, total space of Hopf fibration), KANG Rongji (Blakers-Massey),=20 Evan Cavallo (Freudenthal and lots of clever cubical tricks).

Our proof also deviates from the one in Guillaume's th= esis in two major ways:

1. We found a direct encode-decode proof of a special case of corollary=20 3.2.3 and proposition 3.2.11 which is needed for =CF=80=E2=82=84(S=C2=B3). = This allows us=20 to completely avoid the use of the James construction of Section 3 in=20 the thesis (shortening the pen-and-paper proof by ~15 pages), but the=20 price we pay is a less general final result.

2. With Guillaume=20 we have developed a new approach to Z-cohomology in HoTT, in particular=20 to the cup product and cohomology ring (see https://drops.dagstuhl.= de/opus/volltexte/2022/15731/). This allows us to give fairly direct construction of the graded=20 commutative ring H*(X;Z), completely avoiding the smash product which=20 has proved very hard to work with formally (and also informally on=20 pen-and-paper as can be seen by the remark in Guillaume's thesis on pag= e 90 just above prop. 4.1.2). This simplification allows us to skip=20 Section 4 of the thesis as well, shortening the pen-and-paper proof by=20 another ~15 pages. This then leads to various further simplifications in Section 5 (Cohomology) and 6 (Gysin sequence).

With these mathematical simplifications the proof got a lot more=20 formalization friendly, allowing us to establish an equivalence of=20 groups by a mix of formal proof and computer computations. In=20 particular, Cubical Agda makes it possible to discharge several small=20 steps in the proof involving univalence and HITs purely by computation.=20 This even reduces some gnarly path algebra in the Book HoTT=20 pen-and-paper proof to "refl". Regardless of this, we have not be= en able to reduce the whole proof to a computation as originally conjectured by Guillaume. However, if someone would be able to do this and compute=20 that the Brunerie number is indeed 2 purely by computer computation=20 there would still be the question what this has to do with =CF=80=E2=82=84(= S=C2=B3).=20 Establishing this connection formally would then most likely involve=20 formalizing (large) parts of what we have managed to do here.=20 Furthermore, having a lot of general theory formalized will enable us to prove more results quite easily which would not be possible from just=20 having a very optimized computation of a specific result.

Best regards, Anders and Axel

--
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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAMWCppmb%2BAt_Bwp_2USKH9dAigFG= x0GBrcG3XQQaqZmkr-kHog%40mail.gmail.com.
--00000000000045f6ec05d78772f5--