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 ΩS²ⁿ⁺¹₍₂₎, this is an important space because it appears in the James fibration from classical algebraic topology:

Sⁿ₍₂₎ --> ΩSⁿ⁺¹₍₂₎ --> ΩS²ⁿ⁺¹₍₂₎

This is the fibration that gives the EHP spectral sequence at p=2 and allows one to compute homotopy groups (at least 2-primary parts) inductively.

So, in HoTT one can hope for a type family ΩS²ⁿ⁺¹₍₂₎ --> U, which has the proper fiber and base space. Now as far as I know, the only homotopy theoretic fibrations that 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 ΩS²ⁿ⁺¹₍₂₎

   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) = k if k is prime and k =/= 2. S(k) = 1 otherwise. Now by theorem 4.20, we can define s : N -> N by s(k) = prod 0<=n<=k 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 ΩS²ⁿ⁺¹. The colimit of this diagram should be our desired space ΩS²ⁿ⁺¹₍₂₎.

If you recall 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 details but this should give us some higher inductive type which is (at least) equivalent to ΩS²ⁿ⁺¹₍₂₎. 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 topology will work in HoTT?