From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBBHP26HNAKGQEIWXI37I@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,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.1 Received: from mail-oi0-x237.google.com (mail-oi0-x237.google.com [IPv6:2607:f8b0:4003:c06::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 4b3ef44f for ; Sat, 28 Jul 2018 14:26:38 +0000 (UTC) Received: by mail-oi0-x237.google.com with SMTP id j189-v6sf6508960oih.11 for ; Sat, 28 Jul 2018 07:26:38 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=ABTkvGb+K8jWgYMg+Sn88FhXK0K78avjl9r+VkjE3M4=; b=n+7lf0Rg6gYuNmQ3e7h+nDc7K7DQOeiJfrVl2sSwPXRZW8e8RTSrMxzhbCautmIPn4 FrNNFF7TYEOuIOL13BwpvvHdkAElLbvZtE3T0F6G+ZjmAsoqsuguRFVFgk88p7Iw5Vc5 BigFyIqNemrCmm1oKI/5pXe1ee7AMpuHJ3dKAjs4Pdpa/FXIbgNLRGvnf+PrOiyi+fC0 z2rb8QRqiqWd9YcL83Ddo8HmCKje/glbhRsoEe6qcfnINE7h1WtJfAH/c+hyXC+/qvgF iayHFhDuSQBele8ztbzZH5kxPwIeKqjfjc4WtxUys0IqQbP5weHDqq1CyeZNPSVjno5a 1A3Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=ABTkvGb+K8jWgYMg+Sn88FhXK0K78avjl9r+VkjE3M4=; b=c1u75YrwHhe6OxRY8aObqlroDPvBw6V9+GjGvWIHjbSNG8hNHMbWX0+1QKoAi05hhp 3sqzv+Yy8p/ax34qit4fSHUjQaidT9flx63rZGvP7OUiUTwm9hdSLDSNzyBOn18E0hhE ry2mV7xzwQJ1JJTXfVu72tcm2hP5NhGk9x3hz3TSQOkhTq8nM4Sn6dQTah6jAaA8PF6/ W07wqKBVVCTzULiw7NP/+Qc1PN+R8rt9tWECcq4pzKFY9h3CkaC/dViIzzN6Fiqr8Zg8 Aqvu1AtFgT0UyC0JR5JjWLVtK9LiZXYi53Wo5eRc2658mVVYniMq9KgY3elJinxgHB+e sjyA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=ABTkvGb+K8jWgYMg+Sn88FhXK0K78avjl9r+VkjE3M4=; b=K8IUd7Jc1uvwC0v8cRpXYcSFRoWs6rSRpVZmBTpELCHCPUMwL07u4rL2B5ujCiTK9T lZTGUVvvwd3CTPQoP+RWxsmD8767zzIe8v7faeawP5ZW0oNAC0v1s6aq+XLBLG7HV7h/ m+fQcH/zNXdZaRHjTJJGT005W0w00S1uD5zDzs62zM8i4Q4NIQx1txszkCmXsAnRlkvZ iXgelOXAvvMefQgkOwd0M6yaBzcIZ2kygOmlUPfM/dHLhVSRUUKlBJTL54B1E5gzFDR6 XjlUTtB5zpCipd82hYyzAHgCD/iB/sw/qZyfPdabXqnGsHmbpdbqn6xFHepFJ9/6Z2qk QkHA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlGDzLCVop29SLqv6h8XOCFr0b4gBFvmGrA0DOazV0inyL5VPuFx kGV2MFVGPqfJz+1r+oD/QiU= X-Google-Smtp-Source: AAOMgpefU+JKlbaUXc0gAV7krLbqMzjGcguMTBQJrhtVZXauTTlcNLtzCA287BWVJNZHqfECiydpIA== X-Received: by 2002:aca:4787:: with SMTP id u129-v6mr204456oia.4.1532787997222; Sat, 28 Jul 2018 07:26:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:389:: with SMTP id 131-v6ls2887243oid.22.gmail; Sat, 28 Jul 2018 07:26:36 -0700 (PDT) X-Received: by 2002:aca:de07:: with SMTP id v7-v6mr202028oig.5.1532787996749; Sat, 28 Jul 2018 07:26:36 -0700 (PDT) Date: Sat, 28 Jul 2018 07:26:36 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: Subject: [HoTT] Localization in Homotopy Type Theory and status of synthetic homotopy theory in HoTT MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_14626_958167201.1532787996264" X-Original-Sender: alizter@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: , ------=_Part_14626_958167201.1532787996264 Content-Type: multipart/alternative; boundary="----=_Part_14627_643135416.1532787996264" ------=_Part_14627_643135416.1532787996264 Content-Type: text/plain; charset="UTF-8" There is a preprint on the arXiv about a notion of locaisation of homotopy types in HoTT. So far from what I have skimmed it seems that in the future it will be possible to calculate p-primary parts of homotopy groups. Especially since the Spectral library in Lean is having sucesses with the Serre spectral sequence, it should be too long before we see an EHP SS. Being far from an expert I am quite interested in knowing what obstacles stand in the way of formalising, say, Toda's work. I know that the Toda bracket has been resistant to defining (although I am unsure about the specifics). And I've found it quite strange that there hasn't been any siginificant development of stable homotopy theory in HoTT. What are your thoughts on this recent preprint and general thoughts about synthetic homotopy theory in HoTT? -- 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. For more options, visit https://groups.google.com/d/optout. ------=_Part_14627_643135416.1532787996264 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
There is a=C2=A0preprint on the arXiv=C2=A0about a notion of locaisation of homotopy= types in HoTT. So far from what I have skimmed it seems that in the future= it will be possible to calculate p-primary parts of homotopy groups. Espec= ially since the Spectral library in Lean is having sucesses with the Serre = spectral sequence, it should be too long before we see an EHP SS.=C2=A0
Being far from an expert I am quite interested in knowing w= hat obstacles stand in the way of formalising, say, Toda's work. I know= that the Toda bracket has been resistant to defining (although I am unsure= about the specifics). And I've found it quite strange that there hasn&= #39;t been any siginificant development of stable homotopy theory in HoTT.<= /div>

What are your thoughts on this recent preprint and= general thoughts about synthetic homotopy theory in HoTT?

--
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.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_14627_643135416.1532787996264-- ------=_Part_14626_958167201.1532787996264--