From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pf1-x437.google.com (mail-pf1-x437.google.com [IPv6:2607:f8b0:4864:20::437]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6f6cf62c for ; Tue, 30 Jul 2019 15:37:15 +0000 (UTC) Received: by mail-pf1-x437.google.com with SMTP id 6sf41061311pfz.10 for ; Tue, 30 Jul 2019 08:37:15 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1564501034; cv=pass; d=google.com; s=arc-20160816; b=pDhT5Cf1xJ62IBw2pO1ER9IRw0SoUL2YQtX0hwAchXCHcwp6sUdK67B/G/o7c7iuQn Ln4874sMsl5FOGxhzca6f/Alo80S8KNvOaE+OHja1P8qXKGgi20/ZibsjkQfH9w+eNHG ME+bXTRrBl+QpyhdHV0aEkuVQ0W3NsRjN2038vkIJpYtZ8TJKe9mT4AEl3oW4WGwUQp6 hry2uhGzKbD9Z4amgDTGb4eFTWk3rwORvTMkUfenxJQOPH4jATlRWOipAnU1zm+gFMdw FTQEnqwH/cN6A7SFo3NnN7Qcrviku8395mae3iteomGlWOTbh5MhwO7KFiVU1RtauC1S jLIg== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=xuTY9UmT4ArEI9RYxoQlSmtcWdKaXMBlEeV1TfakMKQ=; b=mDkGib9fguBQhXtFRdf2lA3OF7rhHpQ10eCqJ/f/XXzKt5BMfV7N0GX1Q0xjxKZ0BB p8ZMvCra0d8HS0bS/jJ8JquaA4cBPLOae8I3omzSe1Ms4WljkJW4KdTnlF3GLqHtP2qb LzC9iQuezrA6KVS6/fCOewpQM/rAkUWSz/OHVN5RDswvT8C1Krl24y+jRC/7kct7hMsT WvqJi5ShvKa611yovTLpWxpSnwnIL5iRWyDT/7u3wOJqYKLTF5SEyA2OlLgiPbprCl/C 9ZESqRJAn2S9K0i2kqq42mzStTnNyJhhIqKMeOT0PlfaR5w1fiqxJCQWaLL5bnWNOdDz u1wg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=KPZNz8Xe; spf=pass (google.com: domain of luis.scoccola@gmail.com designates 2607:f8b0:4864:20::92e as permitted sender) smtp.mailfrom=luis.scoccola@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:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=xuTY9UmT4ArEI9RYxoQlSmtcWdKaXMBlEeV1TfakMKQ=; b=Ubavmgf+KZJZRs9a1IdLURxeqCMpS9sjaEECOOkfzE3AxvGPrL2lA4mjL9VWU14cNq XTjQjamFsEntZqtHQeSuSW3Q88Dsc2ykhJs3xCueiR1+DKsTkfK4YhHQJdIaClfi3fPq aH6t0APNTneuuGc1SvKec4dkULQxcVhc3NZ0L4B4c5YtY3pn/RDKI+vTlTk3PmGOATfh MUHYoBq53CTt5/NQMKGBvNK7og3PQ9xIHgO4Nn+QYZRAMsplv2xDUPZ1VqgrC0jEDjKV 5QgWQ5aPWJE2i+8MhIq3hFZ9TYsymgylJDMB+OJHBs5/YCbSG3mCR6V0/BUxBVVuzPYB 9Pyg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=xuTY9UmT4ArEI9RYxoQlSmtcWdKaXMBlEeV1TfakMKQ=; b=jRUa2sFQh7+2mVBPG/2HQzc9ICGWS+/zsCzyux65IXPjD4cJcnPaT9P5K9gZ0vgQ49 DCwaur/nSJDycF7qDEeLgjhK9rrQ2Oz3h8EGp+e7lFLlp8ifdw7S4UBPaPOE32FQNKFW hiS1KOJVaUGWuopQc82Sw+RYkQLngSNjUTZCWTVrCyf+zdgK1hZHX3kwbyquD2x6j9jq Y1MAhg3TNYaY55bdN82Mc/Yo2ztbfcTkk2ZAWh/fXqxzMrmU6McF0tZEcnPI7ufL0MAT sfiTBzkq4t9xiY8BwmunIqQ/Hh8TriJdrkuZ1eNA3wlPy+ZlqZPM5tqyCUgbyrkyLpZ6 8RPA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc: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=xuTY9UmT4ArEI9RYxoQlSmtcWdKaXMBlEeV1TfakMKQ=; b=DDQ4yJFPR3MfL3UfN73NBnI3fnrd1kJtoSia+R19FnvNx93KgaYK7NSk8FSbCwouyL 04o5Zj5cA7idKpP2izmjgXnj4FFBIt3aVPU84Qc0Dh0NEiYPN2+X17X+COpU6tP3ReWd dLjfizE90tpk8XzGD/OqseYkYPqexJv7fFleZufVWoBIvhI39moY0cs9SmL0RZXEG10Q BVBryOxYiHYp6RHbE3kPw8uBVb+oYnmTY/Ll7UL7XHdf2YRrWz+Pupk/4n2M4Yq7x8w7 ejypqepBN9SD3mwLLSyFa5cW+LLd0zFqtvwOXCCKNqJDqoM021WhJasrb2UPtAN1xhFz zIvw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVgWtQCEoz4LCa+4IYJ7jOgFUlFhJJl4wEvQyPRA60nQ4FQB5nY 8MJqdJZardLcDfBbbAnfS10= X-Google-Smtp-Source: APXvYqwF3xABjFMRcekfb5wqrp0f+rIogFPm5nYHUhlsSuDbhLWhbyYmsYTQdbpWE3kMG6zQ0HW8KQ== X-Received: by 2002:a65:46cf:: with SMTP id n15mr15603845pgr.267.1564501033692; Tue, 30 Jul 2019 08:37:13 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:3043:: with SMTP id w64ls13316543pgw.15.gmail; Tue, 30 Jul 2019 08:37:13 -0700 (PDT) X-Received: by 2002:aa7:8619:: with SMTP id p25mr21872122pfn.220.1564501033252; Tue, 30 Jul 2019 08:37:13 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1564501033; cv=none; d=google.com; s=arc-20160816; b=lXSBMwBXhnny1b8DF2ibTz5/YEP72/8vdOBzaswz/0ma76vfL6oCZAMpOUzSGthl4p sxlySslUT8iymHb9/z7dmG3QFDnNylMQhNeL4TXwWl9kJvnWMYOJrOs/jt8D++vzFNHk wa8igvDiWOb04sqiZPdJKwY7NzYsBGiQQrwUiO/R5B9IlFZ0Rl1wrKTi34ErgmG2dHVY T3hnDnmPSPYVqayh8nbjFNnMXiQdO6tXuoTjMA59s4a+Kwq+bP3wIVYybADqFEoILZbb N6XZU0NFf1WpqR3RVUHVPs/7kRSEdFduiI4BDRxtwkFoYUgOPLYUO05toX8A2jGa2FDX kuMg== 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=hlVDhlZt9FQdjQaHPRAPltW/nnpmJsj9icayEaL4lhg=; b=b6jVKTR9sOPjK6CCDmnHw1KkrUzz3P1eGlQfjGpxnhysKxL/QyAJy/p+QgrAQ+5YfA eZBdpSjP5YP3FbjbbB/vfO1oObnCGNVrMQuTNBwRouAmYo8j5x80HqBgN3UBixKNK/fz s9qBMc8lgWnkDhgeeClmAR4tFb3A3ITQhG8yaNfEz8EIWmyHZeWsXWOavpWX6xwbN5KW UmSHqGZq3D4xK9Ry+MhhwnhMTEqVmfhoKZcfKbjH7sn4Ggb8OaKIhDfYHVvdns0qqf9i 3JIAmOJJDqrfQG5XHxyv4Xcf3838V6CjzrmrW9cMDzLLBq7cw+JiXoC2pPI95+UY8O2M jqjg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=KPZNz8Xe; spf=pass (google.com: domain of luis.scoccola@gmail.com designates 2607:f8b0:4864:20::92e as permitted sender) smtp.mailfrom=luis.scoccola@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ua1-x92e.google.com (mail-ua1-x92e.google.com. [2607:f8b0:4864:20::92e]) by gmr-mx.google.com with ESMTPS id d67si2272645pgc.1.2019.07.30.08.37.13 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Tue, 30 Jul 2019 08:37:13 -0700 (PDT) Received-SPF: pass (google.com: domain of luis.scoccola@gmail.com designates 2607:f8b0:4864:20::92e as permitted sender) client-ip=2607:f8b0:4864:20::92e; Received: by mail-ua1-x92e.google.com with SMTP id j8so25588408uan.6 for ; Tue, 30 Jul 2019 08:37:13 -0700 (PDT) X-Received: by 2002:a9f:248b:: with SMTP id 11mr73636948uar.9.1564501032345; Tue, 30 Jul 2019 08:37:12 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Luis Scoccola Date: Tue, 30 Jul 2019 16:44:33 +0100 Message-ID: Subject: Re: [HoTT] Hurewicz theorem in HoTT To: Ali Caglayan Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000048a6cf058ee7c826" X-Original-Sender: luis.scoccola@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=KPZNz8Xe; spf=pass (google.com: domain of luis.scoccola@gmail.com designates 2607:f8b0:4864:20::92e as permitted sender) smtp.mailfrom=luis.scoccola@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: , --00000000000048a6cf058ee7c826 Content-Type: text/plain; charset="UTF-8" Hello Ali, Dan Christensen and I have a draft paper that proves the Hurewicz isomorphism theorem in HoTT, and we plan to make it available sometime soon. We have not formalized the proof, and it also relies on the adjunction between pointed mapping spaces and smash products and some coherences of the associativity of the smash product that have not been completely formalized. Our starting point is similar to yours, so to answer your question, I would say that yes, that idea can be made to work. However, at least in our approach, most of the work is in proving that the Hurewicz map is actually a group homomorphism. In that argument we really need the fact that homology is defined as a colimit and we can't just use some sufficiently large t. Another key ingredient in the approach is the relation between smash products of types and tensor products of their homotopy groups, which we had to develop for this purpose. For completeness, note that Floris van Doorn points out in his thesis that another possible approach is to use the Serre spectral sequence for homology. In this approach one still has to prove the dimension 1 case. Best, Luis On Sat, Jul 27, 2019 at 2:18 PM Ali Caglayan wrote: > Is there any progress on proving the Hurewicz theorem in HoTT? > > I stumbled across this mathoverflow question: > https://mathoverflow.net/questions/283199/an-abstract-nonsense-proof-of-the-hurewicz-theorem > > I wonder if we can adapt the following argument: > > Define H_n(X; Z) as [S^{n+t}, X /\ K(X, t)] for some large t and pointed > space X. The Hurewicz map is induced by a generator g : S^t->K(Z, t) of > H_n(S^n). Given by postcomposition with (id_X /\ g). > > H : [S^{n+t}, X /\ S^t] ---> [S^{n+k}, X /\ K(Z, t)] > > Now since X is (n-1)-connected and it can be shown that g is n-connected > (an (n+1)-equivalence in the answer), then it follows that (id_X /\ g)_* is > an isomorphism. > > The only trouble I see with this argument working is the definition of > homology. Instead of having a large enough t floating around we would have > to use a colimit and that might get tricky. Showing that g is n-connected > is possible I think using some lemmas about modalities I can't name of the > top of my head. > > Do you think this argument will work? Let me know what you all think. > > Thanks, > > Ali Caglayan > > -- > 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/f50d39d3-0017-4820-9c76-877760449e78%40googlegroups.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/CAKBukGjsZ6g_D2Xs%3D5V3Ak%2BAQWgXvV%3D%2Bqh%3DScMY2AXgMNJv64w%40mail.gmail.com. --00000000000048a6cf058ee7c826 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hello Ali,

Dan Christensen and I have a draft paper that proves the Hurewicz
isomorphism theorem in HoTT, and we plan to make it available sometime
soon. We have not formalized the proof, and it also relies on the
adjunction between pointed mapping spaces and smash products and some
coherences of the associativity of the smash product that have not been
completely formalized.

Our starting point is similar to yours, so to answer your question, I
would say that yes, that idea can be made to work.=C2=A0 However, at least = in
our approach, most of the work is in proving that the Hurewicz map is
actually a group homomorphism. In that argument we really need the fact
that homology is defined as a colimit and we can't just use some
sufficiently large t.

Another key ingredient in the approach is the relation between smash
products of types and tensor products of their homotopy groups, which
we had to develop for this purpose.

For completeness, note that Floris van Doorn points out in his thesis
that another possible approach is to use the Serre spectral sequence for homology.=C2=A0 In this approach one still has to prove the dimension 1 cas= e.

Best,
Luis

On Sat, Jul 27, 2019 at 2:18 PM Ali Caglayan <alizter@gmail.com> wrote:
Is there = any progress on proving the Hurewicz theorem in HoTT?

<= div>I stumbled across this mathoverflow question: https://mathoverflow.net/questions/283199/an-abstrac= t-nonsense-proof-of-the-hurewicz-theorem

I won= der if we can adapt the following argument:

Define= H_n(X; Z) as [S^{n+t}, X /\ K(X, t)] for some large t and pointed space X.= The Hurewicz map is induced by a generator g : S^t->K(Z, t) of H_n(S^n)= . Given by postcomposition with (id_X /\ g).

H= : [S^{n+t}, X /\ S^t] ---> [S^{n+k}, X /\ K(Z, t)]

=
Now since X is (n-1)-connected and it can be shown that g is n-connect= ed (an (n+1)-equivalence in the answer), then it follows that (id_X /\ g)_*= is an isomorphism.

The only trouble I see with th= is argument working is the definition of homology. Instead of having a larg= e enough t floating around we would have to use a colimit and that might ge= t tricky. Showing that g is n-connected is possible I think using some lemm= as about modalities I can't name of the top of my head.

<= /div>
Do you think this argument will work? Let me know what you all th= ink.

Thanks,

Ali Cagl= ayan

--
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 ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/f50d39d3-0017-4820-9c76-= 877760449e78%40googlegroups.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 h= ttps://groups.google.com/d/msgid/HomotopyTypeTheory/CAKBukGjsZ6g_D2Xs%3D5V3= Ak%2BAQWgXvV%3D%2Bqh%3DScMY2AXgMNJv64w%40mail.gmail.com.
--00000000000048a6cf058ee7c826--