From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORB2E373NAKGQET7I6GMI@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.8 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-it0-x23a.google.com (mail-it0-x23a.google.com [IPv6:2607:f8b0:4001:c0b::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 78d9f06f for ; Mon, 30 Jul 2018 22:15:06 +0000 (UTC) Received: by mail-it0-x23a.google.com with SMTP id w196-v6sf860282itb.4 for ; Mon, 30 Jul 2018 15:15:05 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1532988905; cv=pass; d=google.com; s=arc-20160816; b=tgPIk2mRXafuqUf0hWJiaaND/BUtZn9a/BmI7umGunEtrAwZ57LmoLq7BfZIKbtZM9 w+vx8+WWMA65CKcINGR1jDQdjd71TYVcfVS6/eJQqBusuPxzI/GEG+rrhKjNekteHwqv lrgYIxftaKt7fvPqin7RgB9XxKdCFU974SGKmgfpVPpUyXBF+Q9y5wULakikyrM/OS7N /xdNOrH+adKJ4D0mnNwuOOy6OLW5HAOJyNqpAvm3JZG0dASm9G5RyK6l4Cw7y0YxPyhd QsmYa0VaX3eUfhnw7uEpyohuIvgwdbF20AYNCbblR2IkyPFXhF1BEy8jpcVqSwxeeP0+ WUBQ== 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 :references:in-reply-to:mime-version:arc-authentication-results :arc-message-signature:sender:dkim-signature :arc-authentication-results; bh=43E/Fz84N8fDj7wDIvJCjEVrttxp2WbYlv9iKmti8gY=; b=ltAhlYuFvIbDFcCw0VhcR46vL7U037P9et/K+FlfJMNBzapCoL0Svf7Kw8D8iAz7vo i+HsnUB7HORNurw0vNfEKGWMHDMArMOOTGbKGtC/D4LFk1v8+Tg7G7ewnTS1XI5K/tBo RqfVcGxeAowGBbuh7RL2/DXjm1KENrEniedO3zOntH4rX5/QvVqY/oFtCKC1YTuYBRht s0/tWPXyl5dyvm0sTIrwFj3vqphXVYfTzlFEMk0KtUTvomfJ5hE8IaKk1Xac0Y9i45NR Rq2LyBal2SbBzIPAaJ/VfJRAVdk7lv0fhjLN0BugE4uOyI1jgBxRSrgQZlYUQTk534eV u+BA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=a6LI9ru4; spf=neutral (google.com: 2607:f8b0:4002:c05::22a is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:in-reply-to:references: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=43E/Fz84N8fDj7wDIvJCjEVrttxp2WbYlv9iKmti8gY=; b=VkUoJI/98NqY1kZUgvvidS8HkMUl+K7cnQ46eD3sWRcOlD1mz2NIgKG2rKW92CiJOi Mvlv2QXXA3fsVpOcyqbsyRw/Z29euE11fe4iVidVzw2cRCFZ42+YuElFTaQKp+aGgI9M wEOsdI0XbmrU6ocJGuuusX4Ay3K2nD/UVGydjoIPGFbUJ1/dNuj4MzfdHWHVa9KR+KsQ GO9XYdZ1xfebVwOduoA/p/aoxWu44uSOl6rui7NV4KiQf4gs+XbPt4xtaouoQmuTA+pE u3Diz/nSWuWY/uVNttV5suMzJExdEEoRhi8qq8qIhxGeklKA9PXWJpd07HhPEhSMQqOy Nm6w== 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:in-reply-to:references: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=43E/Fz84N8fDj7wDIvJCjEVrttxp2WbYlv9iKmti8gY=; b=jAX9NMEh0igmeJREVpNyvEIZwwofdnhtxcsVmSWnrke70bPinv4CUn3v207FtMTmpH nwZUklk03FGbZvoYRPkVhU/aax2Wfh4c7DqJaonCdenurilVeSDILBmJELy2ARlpUiDc pG+XjOhq91UBiqoGar92wn3rrBodcAiJ/zv3mwaRiZed01SNN/yMURiZhzhLpNEeDwUh WW/FTFiKZ9r9J4ajnOe0Fr0u/DTJHhDL63BqB5GyECkX/GAm+McXt0XByVMKX6Dixjso 2WIiP5Kc5MF5qUmM9TLTVDb0CHbgbIfLjKpTnerIh5HPFtDjAiT00rDD6FCLwBRPDtgr x6MA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlFGDJqOw8h19bFPtC2K8Vb9m6P2/UMsnIYBuljP56vwqiqSv/qb LCdaA/3po3s3LekKZThFsnA= X-Google-Smtp-Source: AAOMgpeiwW2tqI8RVAGaRHXunVS61pcn5rphwJ/NsqeHxSMHcogJYonYy5LA6N6c1WRKo8wfQFq2tQ== X-Received: by 2002:a24:45d9:: with SMTP id c86-v6mr65179itd.1.1532988904813; Mon, 30 Jul 2018 15:15:04 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5e:9e06:: with SMTP id i6-v6ls796520ioq.15.gmail; Mon, 30 Jul 2018 15:15:04 -0700 (PDT) X-Received: by 2002:a6b:7d47:: with SMTP id d7-v6mr3953182ioq.18.1532988904514; Mon, 30 Jul 2018 15:15:04 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1532988904; cv=none; d=google.com; s=arc-20160816; b=zceMOO7TwSafRZSzl6FfZk1UghY6oGGB5TPAj4oBI6BbBZH+i+faBjqcsJobputNXb SnH34hWqrf1WBsD3HSOIdMlZMbEbeXLpTB1Xsxw3PcCbfxnb8OatLTjwhKCdhz871vSk qY9RYAFs7lsFdUit7P/+BCTR9rXvrqRtHnIZcpdlqDpfHESw1DMSO1C88yyYQfGMKtFL Dqe9+7UgAv9l5Gw6Ecn/uT5AGcSn1kUhYUNfF+fPK/FXwPIn9F9jefM1Jzdlfxt/2EBv W17JpnM801OMODPDCASW5WUwOeDByhPb/Y2GoN2kA6OFx7ZD2TXVOmVKPPjZ15PUjWag tEWw== 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:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=21qqKfublKWBZqH7a1A8n13I1E0MfAp3RkYkwNoEKhk=; b=l8WWFsiqnSY6ASdc8JjajXEbpc7aM8pfNn0jj+JM2v5apAVlfCl7cEn0Iv5xCMF0Rt HKyDJy0swyB652YKGPW37g/qQpBU8Vxw0ruH76FLc/YYVK34Hq+tQR5trxhhWMycqW/j 1w4l5wVjcFypJqjYFjqCX8swwDE3x1Q0OoKlOnz9SxAGFrfyHI0P65KgdHC9WdQ3HRdr QXrqQsna7KOlxjQpRDoHwo/xdD/QK98sHHktyH3uaGz1hI+l9c1KcgdMlUqJOHQBWuVC c7edDhU6OaP5IXyr4RaJBx9yYZ+s1ZZO9gOI+vCh8G5cGJFpy1dZ1uXGOTZcRCckoSET LPjw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=a6LI9ru4; spf=neutral (google.com: 2607:f8b0:4002:c05::22a is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw0-x22a.google.com (mail-yw0-x22a.google.com. [2607:f8b0:4002:c05::22a]) by gmr-mx.google.com with ESMTPS id c5-v6si20904itj.0.2018.07.30.15.15.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 30 Jul 2018 15:15:04 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22a is neither permitted nor denied by domain of shulman@sandiego.edu) client-ip=2607:f8b0:4002:c05::22a; Received: by mail-yw0-x22a.google.com with SMTP id y203-v6so4995889ywd.9 for ; Mon, 30 Jul 2018 15:15:04 -0700 (PDT) X-Received: by 2002:a81:9a16:: with SMTP id r22-v6mr10036836ywg.119.1532988903699; Mon, 30 Jul 2018 15:15:03 -0700 (PDT) Received: from mail-yw0-f177.google.com (mail-yw0-f177.google.com. [209.85.161.177]) by smtp.gmail.com with ESMTPSA id j16-v6sm5539151ywa.28.2018.07.30.15.15.02 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 30 Jul 2018 15:15:03 -0700 (PDT) Received: by mail-yw0-f177.google.com with SMTP id r3-v6so4998063ywc.5 for ; Mon, 30 Jul 2018 15:15:02 -0700 (PDT) X-Received: by 2002:a81:84cb:: with SMTP id u194-v6mr9600200ywf.246.1532988902761; Mon, 30 Jul 2018 15:15:02 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:4094:0:0:0:0:0 with HTTP; Mon, 30 Jul 2018 15:14:42 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Mon, 30 Jul 2018 15:14:42 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Localization in Homotopy Type Theory and status of synthetic homotopy theory in HoTT To: Ali Caglayan Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=a6LI9ru4; spf=neutral (google.com: 2607:f8b0:4002:c05::22a is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu 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: , A quick comment about stable homotopy theory. The current HoTT approach to spectral sequences does use spectra fundamentally, so the formalization of the Serre SS involves a certain amount of theory of spectra. There is however an issue with stable homotopy theory in that (at least in "Book HoTT") there is no "strict equality". Thus, for instance, the only notion of pushout is a homotopy pushout (with specified homotopies), and similarly for smash products, which makes them rather hard to deal with; to my knowledge there is not yet a fully formalized proof that the smash product of *spaces* is coherently associative, let alone spectra. Similarly, it seems that the only available notion of spectrum is an Omega-spectrum with a sequence of spaces equivalent (not "isomorphic", which has no meaning) to each other's loop spaces -- there seems no likely possibility of "structured spectra" like symmetric spectra, orthogonal spectra, or EKMM spectra -- and even worse, the only notion of map between such spectra involves a sequence of explicitly *homotopy*-commutative squares. So the technical difficulties in dealing with all of this are an issue, although people are definitely working on it. On Sat, Jul 28, 2018 at 7:26 AM, Ali Caglayan wrote: > 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. -- 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.