From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORBIGTZ7NQKGQEPRQELZI@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=-1.0 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-ua1-x938.google.com (mail-ua1-x938.google.com [IPv6:2607:f8b0:4864:20::938]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 11cf209b for ; Wed, 15 Aug 2018 08:51:45 +0000 (UTC) Received: by mail-ua1-x938.google.com with SMTP id 71-v6sf373900uas.18 for ; Wed, 15 Aug 2018 01:51:45 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1534323104; cv=pass; d=google.com; s=arc-20160816; b=M+1K3Sl03Qy/BPUJRL2SkXOQbrE29/y3XTaMBT+bf+4Q+VTRpqAXY5ObYa4xnHdQPD 6ZBDGun0MvH6qC53cKGtl//G75eA7lXh6weVzJUBS4WsTuwnhp6RpwRm/jL7SEZsZU0L O6P6xtsOhvjnSAMVkFK2wPfeuEfSDMhtuTYfmr84c4WNVMQKzd3IWQPopTqJgTYZaTze mkhMpTzTIOHVPAaQtJI3JWItTJx5AejOTBdFqry7zpFB17u3IkBN6Y/PcZRY8jSKpcgE uu9zW/VMvmkHImNkV/iGOsQ2AlQcsdok9lBySGT5rj667h9OlAX0R8b/dVURAFzj/Us3 w6QA== 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:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version :arc-authentication-results:arc-message-signature:sender :dkim-signature:arc-authentication-results; bh=PJOnuBSsfOtY2vWuUsAnJYBvA26VbqJAVoN+PJFgXIo=; b=E5xy/qDsWuFGNzQkuVBGvKN45Qp4/MfBHvA8CRvyY9o1bnaq0U7rTWWZvy5HWk2BeT PZrxSwoHtW9IHGDiz07MA1blerrxtb1P6hIQmvIEO3s4X9gTPMka4eABDIrNAajVAVSt rr0tQE330XSTiwdR3PTIAe8V9eE/GWxWhEaxOPkIyhxhIwRG2AGDk6Tx8WuhHvl4/E24 db4j+3U5hFQLwtacmrtQ9x/16yqs7OTaRRY2PHdBL/gDtbjV5quNVeZVA/Kk/l9zNjHL booGdlbZBoo+V0wypqhQGyCs2QIHCUX76In5xNPH/j+HcUi63UVoyO0m93y1VdhM9Bzv 7KXQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="PNk/ITIe"; spf=neutral (google.com: 2607:f8b0:4864:20::c2a 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:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=PJOnuBSsfOtY2vWuUsAnJYBvA26VbqJAVoN+PJFgXIo=; b=o4Wf6Xcq3Iuu7Bnw8LVI3KNKIAIvYAfvWnfg1w3tXSX0VeRyygBFSwWKAjiJCJ3m58 Q1bXsSV97sOA3JttTuaOW0Io5AmYy8yGD42m0Bxr9Qc9nYgGUnzyi3g2huTINqMdNh/m LP2UtGENplg+rnWgJRVbd3759Bz9Pokl9aDI3x733WJIyUyzWxheh/bcv9VY6pXP4VjL fsoqzwZtCZL6kYfOlqNK/7kPL8aYPLrqrbPh5yVOVQSEjh3xRnjT4QxlDOk8jxWLx+JO brOdnFHFNJWogPFqAKUIFHOGhed8U/m7q1AN/C2YyYPI7F7t+Ga3UHQFZ25xnK9F0Z7p J1Bw== 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:content-transfer-encoding :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=PJOnuBSsfOtY2vWuUsAnJYBvA26VbqJAVoN+PJFgXIo=; b=gaC9s/f9pEcMtRSozNWxnuXz55QpNRDyzUbvZTave77f8YYWwcsKuowaYsEgxQLPnk RFOUz8QE54wZkqD7AYuD0xNSZ0frTVFJX3Z5cf2/kLyLrukWZOK6i6J4mzq2s0gyEsUI US5vRKeuNjFX3Wn+l5xifVr2kYrOrqjDjF7iiJwXeSDl2/WbpKp8CC/cFTAfa7FfS7IR OMYkaMb+LgG4bXTAJh6kdi07/k96L4Zpd5OPaLtLwLJqvScnfzKWRgvnJpJw9WHpBwvt 3q7I9yXvjBmrnkJdNW+55puWn6lxxvLDe2WP7+zcbv5GOwnHsF8HYiQd7ar64VqzQmN+ pA2w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlGOmv9Dtm5weS9r8buvhC1uULFbYuWqhCwkfYiYyv/YG0PPfPAh LfCs1tf0Z0Mp05nmOmKiU/o= X-Google-Smtp-Source: AA+uWPz//NCg4FnaSbmcr5NrD+gBWz1amiVkWRif77gNVrvJVuIdSgwy34RoQpxrUPubU8yAjiPFKQ== X-Received: by 2002:a1f:9746:: with SMTP id z67-v6mr205081vkd.2.1534323104348; Wed, 15 Aug 2018 01:51:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:9b85:: with SMTP id d127-v6ls74536vke.18.gmail; Wed, 15 Aug 2018 01:51:44 -0700 (PDT) X-Received: by 2002:a1f:2305:: with SMTP id j5-v6mr14464838vkj.47.1534323103978; Wed, 15 Aug 2018 01:51:43 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1534323103; cv=none; d=google.com; s=arc-20160816; b=ObMcQCxRi17GriedtX8iXkFeiWpcjwDJTEtl68CO/pggQ5/yBzQqFyqIb7UMXUNXr8 V7b1DUEXlNm7jHsEqBHYk7rIx9P5dl9raLd4m29buHvUcqwo7i2IyankJLB2Pkkb9A8C +V+2XKpvhzCQrsloFenIQ3HIGCrILMLW9cqg2fcYhJvly8A+2MScjmaWTmxMhiTVA0Qk hRT6bsljlXO1/R+6rwGv6HD69F8JAdzgBP9T5MhO5tfAGhNytI8leCLpkQxeHBv/Kq4p nF/5RpfspX2YjkowkxWfRQpi+avFXN0txsA9fXHbUz8sXm02DSpRguqZe6HfTekLa5iu WVTA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature :arc-authentication-results; bh=pHUwWhhDUXiAdAkYr5cxteb+zIj/V/s6AA1vDJV+oy0=; b=iZebwfHHEAQ+Pime9is0lAyX5YYkFW/5+ZVw0ijxLnStGT9QVrWLUmg/k0bREra3CZ 33WLPyyCkOCIKpE4xUXBZXtAxLWa0RVnsbL9ga2hpPYGtF0lPeZZOvpAl+2F47j2+rV5 kyj8SNCn6af0nnG2j+Bit8jN2bzXqgXub6CEXhQsWmCH/SOh+HSo/XusfMNA8kHEfgJv Cn2m9KGFmF/Najge0qacRCSVWQkS7/pPTik8dpDVhdmYuAp5TbgvNLbZZIYCyQuwhbKP eX6Iqa/AIgSAqwH1+hoCUPGuJNOmXkd6hsGJW4IkSn0iAl/sTJizfCao2iq6DIXSL1oN R3jw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="PNk/ITIe"; spf=neutral (google.com: 2607:f8b0:4864:20::c2a is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc2a.google.com (mail-yw1-xc2a.google.com. [2607:f8b0:4864:20::c2a]) by gmr-mx.google.com with ESMTPS id x11-v6si1077456uap.4.2018.08.15.01.51.43 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 15 Aug 2018 01:51:43 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4864:20::c2a is neither permitted nor denied by domain of shulman@sandiego.edu) client-ip=2607:f8b0:4864:20::c2a; Received: by mail-yw1-xc2a.google.com with SMTP id q129-v6so327247ywg.8 for ; Wed, 15 Aug 2018 01:51:43 -0700 (PDT) X-Received: by 2002:a81:c60c:: with SMTP id l12-v6mr13016991ywi.169.1534323103371; Wed, 15 Aug 2018 01:51:43 -0700 (PDT) Received: from mail-yw1-f44.google.com (mail-yw1-f44.google.com. [209.85.161.44]) by smtp.gmail.com with ESMTPSA id i204-v6sm11211767ywe.102.2018.08.15.01.51.42 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 15 Aug 2018 01:51:42 -0700 (PDT) Received: by mail-yw1-f44.google.com with SMTP id z143-v6so329466ywa.7 for ; Wed, 15 Aug 2018 01:51:42 -0700 (PDT) X-Received: by 2002:a5b:44b:: with SMTP id s11-v6mr13139604ybp.505.1534323102521; Wed, 15 Aug 2018 01:51:42 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Wed, 15 Aug 2018 01:51:30 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Localising spheres in HoTT To: Ali Caglayan Cc: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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="PNk/ITIe"; spf=neutral (google.com: 2607:f8b0:4864:20::c2a 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: , Localizations at arbitrary families of maps are constructed in arXiv:1706.07526 using a recursive HIT. Egbert Rijke has shown that in the case of localizing at maps between omega-compact types, such as circles and spheres (therefore including this case), the localization can be constructed as a non-recursive sequential colimit which is at least similar to the classical construction as a telescope; but I don't think this work is published anywhere yet. On Sat, Aug 11, 2018 at 1:58 PM Ali Caglayan wrote: > > So I have been reading https://arxiv.org/abs/1807.04155 > > In it they detail a construction for localising types at a prime. I want = to construct =CE=A9S=C2=B2=E2=81=BF=E2=81=BA=C2=B9=E2=82=8D=E2=82=82=E2=82= =8E, this is an important space because it appears in the James fibration f= rom classical algebraic topology: > > S=E2=81=BF=E2=82=8D=E2=82=82=E2=82=8E --> =CE=A9S=E2=81=BF=E2=81=BA=C2=B9= =E2=82=8D=E2=82=82=E2=82=8E --> =CE=A9S=C2=B2=E2=81=BF=E2=81=BA=C2=B9=E2=82= =8D=E2=82=82=E2=82=8E > > This is the fibration that gives the EHP spectral sequence at p=3D2 and a= llows one to compute homotopy groups (at least 2-primary parts) inductively= . > > So, in HoTT one can hope for a type family =CE=A9S=C2=B2=E2=81=BF=E2=81= =BA=C2=B9=E2=82=8D=E2=82=82=E2=82=8E --> U, which has the proper fiber and = base space. Now as far as I know, the only homotopy theoretic fibrations th= at have been formalised in HoTT are the Hopf-fibrations and their general H= -space construction. > > So this is really two questions: > > 1. How to define =CE=A9S=C2=B2=E2=81=BF=E2=81=BA=C2=B9=E2=82=8D=E2=82= =82=E2=82=8E > 2. How to come up with the HoTT version of the James fibration > > Now the first one is kind of already done. Heres how to construct it: > > Let S : N -> N be defined as S(k) =3D k if k is prime and k =3D/=3D 2. S(= k) =3D 1 otherwise. Now by theorem 4.20, we can define s : N -> N by s(k) = =3D prod 0<=3Dn<=3Dk S(k). So s(k) is the product of all primes less than k= , excluding 2. > > Now consider the diagram: > 1 1 1 3 3 3.5 3.5 s(7) > X ----> X ----> X ----> X ----> X ----> X ----> X ----> X ----> .... > > Where the integers k denote the deg(k) map, and X is =CE=A9S=C2=B2=E2=81= =BF=E2=81=BA=C2=B9. The colimit of this diagram should be our desired space= =CE=A9S=C2=B2=E2=81=BF=E2=81=BA=C2=B9=E2=82=8D=E2=82=82=E2=82=8E. > > If you recall from the HoTT book, the colimit of a diagram has constructo= rs for each node in the graph, and each arrow. I haven't really worked out = the details but this should give us some higher inductive type which is (at= least) equivalent to =CE=A9S=C2=B2=E2=81=BF=E2=81=BA=C2=B9=E2=82=8D=E2=82= =82=E2=82=8E. I'm not even sure this is the kind of HIT that you can write = down. > > Here are my questions: > > 1. Can we write down a HIT for a type localised at a prime? > 2. Does anybody know any work on other fibration in HoTT? > 3. Do you think that localisation methods from classical algebraic top= ology will work 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. --=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. For more options, visit https://groups.google.com/d/optout.