From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBBD44XXNQKGQEC5DDCCQ@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.1 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-x23a.google.com (mail-oi0-x23a.google.com [IPv6:2607:f8b0:4003:c06::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 890c52e4 for ; Sat, 11 Aug 2018 20:58:57 +0000 (UTC) Received: by mail-oi0-x23a.google.com with SMTP id j189-v6sf12644898oih.11 for ; Sat, 11 Aug 2018 13:58:56 -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=7cW6TbrOoFJcxl/yMJkbPgGijZwIDj3Jb9U757rmEoA=; b=HpuoK+bFAMMwe6c8y5f3+qWWa/wpzryT4YhO5qs/T1Z1haoXwYJHizptl24E4F75ub F8rXdTAhvoy9EwEfS6KtgRTxAddkkFvBcawRJkOH5beSnSgZjOYuMisCi/rGP/sGoBG8 /E9AL3PnC2DpHQKM9s6WqdMNlo6+V50/Tat/Fi8vmqTc8DDdvVn/Khb2X/h/m6XksRMO ot90w9pKCL9x32x20YpwdRjgZ645+Gpb+V0A+gjB0QIVrUQkL9RQL07BuJPruKYvcwkc 5RGZIlqV+uTM3J7jAkru6tvCIYcDBKbq0vkazjdh2lj0f5gZlgozFmVmKw1HdsHASVee tTjA== 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=7cW6TbrOoFJcxl/yMJkbPgGijZwIDj3Jb9U757rmEoA=; b=gxupnmTHCDh8dZ+UqxDrwYGMyNCuj3CUi+1PbE0xAyJiO8XHjL6hJbvqY8LN3VkK7U MVW25ZVosJSaNXD5J+Ql05+NR+NaEAwPAJpJrZ+S+pVPQUPooY9pW9O9WETiHcSjDviI VRxJDPV516u0q6VmxWANA6GCywq72izLpj/1/FhXV3PImssddp/JXKaHbuNMI6U+HwjF Tij1o4QyOvmL4LkhUOAB+babwPjnT6Xf/s5DuHOlgkxlMSq+t+98awrJFPXseRajR4tR 1Jah5OJynFdqt4Als60x9Dm32CSnw8PiEBBwxAy1s6qevSgt0V0d3J7Xve/51XaE1bnj ltGw== 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=7cW6TbrOoFJcxl/yMJkbPgGijZwIDj3Jb9U757rmEoA=; b=AkWZ4/kkNGbCTjDZnWhRyxbjiDiO3Qh9MIv8wPTjEFr6Ed0wmY/Z8pcpYg6go441+q ZTIWhf9P7wgBdSiqAwl4THME+KEkBexOoP9bxu+q3gGjRXMvu4qGHNtGR34FrDnvMWO+ KYTKk/BpmIyUTC2Rgp+xltUAbEpK10FFkAaPayrdc+FrClCYC/kPRLU8fArocniatu66 bmT//ZlLiRI1f7IyxextnRaJIu87gHD+ONXM4qfXHlVq+evFuE3J5mi7VdxOF///CPSc 5BMZf7iVhXb5U7fI3GVa2J/q7ZvS8QkDC2Fh34h3kgY2HFryIUihsfQU/1Ag4+dNemc6 tLOg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlGFyWZP2CfKEd0GwweyqYMdsoF5FPhXyn+weXue+FCJtp867O77 Gme+ZMB+HPUTuKQai8WNygI= X-Google-Smtp-Source: AA+uWPynuqVkGCDtcpuZxmNwp+41sxdY7VZPlVcorV0nainslzlAl8NXKP65jyjwMWzdM+oCLY2BUA== X-Received: by 2002:aca:c744:: with SMTP id x65-v6mr328724oif.2.1534021135380; Sat, 11 Aug 2018 13:58:55 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:1304:: with SMTP id e4-v6ls5303224oii.17.gmail; Sat, 11 Aug 2018 13:58:55 -0700 (PDT) X-Received: by 2002:aca:de07:: with SMTP id v7-v6mr315207oig.5.1534021134763; Sat, 11 Aug 2018 13:58:54 -0700 (PDT) Date: Sat, 11 Aug 2018 13:58:54 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: Subject: [HoTT] Localising spheres in HoTT MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1099_798679965.1534021134120" 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_1099_798679965.1534021134120 Content-Type: multipart/alternative; boundary="----=_Part_1100_1216819106.1534021134120" ------=_Part_1100_1216819106.1534021134120 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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= =20 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=20 James fibration from 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=20 allows one to compute homotopy groups (at least 2-primary parts)=20 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=20 proper fiber and base space. Now as far as I know, the only homotopy=20 theoretic fibrations that have been formalised in HoTT are the=20 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:=20 Let S : N -> N be defined as S(k) =3D k if k is prime and k =3D/=3D 2. S(k)= =3D 1=20 otherwise. Now by theorem 4.20, we can define s : N -> N by s(k) =3D prod= =20 0<=3Dn<=3Dk S(k). So s(k) is the product of all primes less than k, excludi= ng 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=20 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 constructors= =20 for each node in the graph, and each arrow. I haven't really worked out the= =20 details but this should give us some higher inductive type which is (at=20 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=20 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=20 topology will work in HoTT? --=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. ------=_Part_1100_1216819106.1534021134120 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
So I have been reading https://arxiv.org/abs/1807.041= 55

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 appea= rs in the James fibration from 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 f= ibration that gives the EHP spectral sequence at p=3D2 and allows one to co= mpute 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 prope= r fiber and base space. Now as far as I know, the only homotopy theoretic f= ibrations that have been formalised in HoTT are the Hopf-fibrations and the= ir general H-space construction.

So this is really= two questions:

=C2=A0 =C2=A01. How to define =CE= =A9S=C2=B2=E2=81=BF=E2=81=BA=C2=B9=E2=82=8D=E2=82=82=E2=82=8E
=C2= =A0 =C2=A02. 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:=C2=A0

Let S : N -> N be defin= ed as S(k) =3D k if k is prime and k =3D/=3D 2. S(k) =3D 1 otherwise. Now b= y 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:
=C2=A0 =C2=A0 = =C2=A0 =C2=A01=C2=A0 =C2=A0 =C2=A0 =C2=A0 1=C2=A0 =C2=A0 =C2=A0 =C2=A0 1=C2= =A0 =C2=A0 =C2=A0 =C2=A0 3=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A03=C2=A0 =C2=A0 = =C2=A0 =C2=A0 3.5=C2=A0 =C2=A0 =C2=A03.5=C2=A0 =C2=A0 =C2=A0s(7)
= =C2=A0 X ----> X ----> X ----> X ----> X ----> X ----> X = ----> X ----> ....

Where the integers k deno= te the deg(k) map, and X is =CE=A9S=C2=B2=E2=81=BF=E2=81=BA=C2=B9. The coli= mit 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 re= call from the HoTT book, the colimit of a diagram has constructors for each= node in the graph, and each arrow. I haven't really worked out the det= ails 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 do= wn.

Here are my questions:

=C2=A0 =C2=A01. Can we write down a HIT for a type localised at a prime?<= /div>
=C2=A0 =C2=A02. Does anybody know any work on other fibration in = HoTT?
=C2=A0 =C2=A03. Do you think that localisation methods from= classical algebraic topology will work 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_1100_1216819106.1534021134120-- ------=_Part_1099_798679965.1534021134120--