Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeNov 2nd 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have added pointer to Mike's discussion of spectral sequences [here](http://ncatlab.org/nlab/show/homotopy%20spectral%20sequence#Shulman13) at "homotopy spectral sequence" and in related entries. But now looking at this I am unsure what the claim is: has this been formalized in HoTT? (Clearly a question for Mike! :-)

   I have added pointer to Mike’s discussion of spectral sequences here at “homotopy spectral sequence” and in related entries.

   But now looking at this I am unsure what the claim is: has this been formalized in HoTT?

   (Clearly a question for Mike! :-)

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeNov 2nd 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexNot in the sense of being implemented in a proof assistant, no.

   Not in the sense of being implemented in a proof assistant, no.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeNov 2nd 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexOkay, thanks. How about the long homotopy fiber sequences of homotopy groups? I hear that Voevodsky has formalized this? Is the code publically available? I was wondering, more specifically, what's the status in HoTT of computing, in principle, homotopy groups of finite cell complexes (i.e. of HITs) more general than spheres.

   Okay, thanks.

   How about the long homotopy fiber sequences of homotopy groups? I hear that Voevodsky has formalized this? Is the code publically available?

   I was wondering, more specifically, what’s the status in HoTT of computing, in principle, homotopy groups of finite cell complexes (i.e. of HITs) more general than spheres.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeNov 2nd 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI'm not well-up on what Voevodsky has done, but you could look through the [UniMath library](https://github.com/UniMath/UniMath) that he works on. I don't know of much work on finite cell complexes other than spheres; I think most everyone has considered that spheres are hard enough to start with. Except for the really easy cases like a finite wedge of circles.

   I’m not well-up on what Voevodsky has done, but you could look through the UniMath library that he works on.

   I don’t know of much work on finite cell complexes other than spheres; I think most everyone has considered that spheres are hard enough to start with. Except for the really easy cases like a finite wedge of circles.

5. • CommentRowNumber5.
   • CommentAuthorCharles Rezk
   • CommentTimeNov 3rd 2014
   • PermaLink
   Author: Charles Rezk
   Format: MarkdownItexWhat is a "finite cell complex" in HoTT? What does "finite cell complex" correspond to in terms of an $\infty$-topos model?

   What is a “finite cell complex” in HoTT? What does “finite cell complex” correspond to in terms of an $\infty$-topos model?

6. • CommentRowNumber6.
   • CommentAuthorCharles Rezk
   • CommentTimeNov 3rd 2014
   • PermaLink
   Author: Charles Rezk
   Format: MarkdownItexI'm really asking: how do you construct the "type" of finite cell complexes in HoTT?

   I’m really asking: how do you construct the “type” of finite cell complexes in HoTT?

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeNov 3rd 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOne definition is that a finite cell complex is a non-recursive HIT whose constructors take no inputs. That's a meta-theoretic definition, so it doesn't let you construct "the type of finite cell complexes". Another definition is that a finite cell complex is an iterated pushout of maps $S^n \to 1$. That can be internalized, e.g. the type of $k$-cell complexes is defined recursively on $k$ where a $(k+1)$-cell complex is specified by choosing a $k$-cell complex $X$, a natural number $n$, and a map $S^n\to X$. Either way, the finite cell complexes in an $\infty$-topos model will be the tensors of $1$ by ordinary finite cell complexes in $\infty Gpd$, or equivalently the images of ordinary finite cell complexes under the left adjoint $\Delta : \infty Gpd \to \mathbf{H}$ to the global sections functor.

   One definition is that a finite cell complex is a non-recursive HIT whose constructors take no inputs. That’s a meta-theoretic definition, so it doesn’t let you construct “the type of finite cell complexes”. Another definition is that a finite cell complex is an iterated pushout of maps $S^n \to 1$. That can be internalized, e.g. the type of $k$-cell complexes is defined recursively on $k$ where a $(k+1)$-cell complex is specified by choosing a $k$-cell complex $X$, a natural number $n$, and a map $S^n\to X$.

   Either way, the finite cell complexes in an $\infty$-topos model will be the tensors of $1$ by ordinary finite cell complexes in $\infty Gpd$, or equivalently the images of ordinary finite cell complexes under the left adjoint $\Delta : \infty Gpd \to \mathbf{H}$ to the global sections functor.

8. • CommentRowNumber8.
   • CommentAuthorCharles Rezk
   • CommentTimeNov 4th 2014
   • PermaLink
   Author: Charles Rezk
   Format: MarkdownItexI don't think that can be right. Maps $S^p\to S^q$ in $\mathbf{H}$ need not always arise from $\infty\Gpd$. For instance, consider $\mathbf{H}=\infty\Gpd_{/T}$ for some space $T$. The internal mapping object $\Map_T(S^k,S^n)$ is the projection map $\Map(S^k,S^n)\times T\to T$. It's $0$-truncation is $(\pi_k S^n) \times T\to T$, so the "homotopy group" is what you expect. But the space of sections of $\Map_T(S^k,S^n)\to T$ is equivalent to $\Map(S^k\times T,S^n)$, so its $\pi_0$ could be much bigger. (Or smaller, if $T=\varnothing$.)

   I don’t think that can be right. Maps $S^p\to S^q$ in $\mathbf{H}$ need not always arise from $\infty\Gpd$.

   For instance, consider $\mathbf{H}=\infty\Gpd_{/T}$ for some space $T$. The internal mapping object $\Map_T(S^k,S^n)$ is the projection map $\Map(S^k,S^n)\times T\to T$. It’s $0$-truncation is $(\pi_k S^n) \times T\to T$, so the “homotopy group” is what you expect. But the space of sections of $\Map_T(S^k,S^n)\to T$ is equivalent to $\Map(S^k\times T,S^n)$, so its $\pi_0$ could be much bigger. (Or smaller, if $T=\varnothing$.)

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeNov 4th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexOh, yes, you're right. So there could be more finite cell complexes in some model than there are in $\infty Gpd$.

   Oh, yes, you’re right. So there could be more finite cell complexes in some model than there are in $\infty Gpd$.

10. • CommentRowNumber10.
    • CommentAuthorCharles Rezk
    • CommentTimeNov 4th 2014
    • PermaLink
    Author: Charles Rezk
    Format: MarkdownItexI guess it's complicated. There is a type $\mathrm{Fin}$ which is the recursive type you alluded to. An $F\colon \mathrm{Fin}$ knows all about its own attaching maps and stuff. This type comes with a "realization" map $R\colon \mathrm{Fin}\to \mathcal{U}$ to the type of types, which you can then factor through its $(-1)$-truncation: $\mathrm{Fin} \to \mathcal{U}_{\mathrm{Fin}} \hookrightarrow \mathcal{U}$. You might think of $\mathcal{U}_{\mathrm{Fin}}$ as the type of "types having the homotopy type of a finite complex", except that there is the odd problem that I can't necessarily lift a map $1\to \mathcal{U}_{\mathrm{Fin}}$ to a map $1\to \mathrm{Fin}$. I would guess that in a sheaf model, $\mathcal{U}_{\mathrm{Fin}}$ corresponds to objects which are "locally" finite complexes, e.g., whose stalks are equivalent to finite complexes.

    I guess it’s complicated. There is a type $\mathrm{Fin}$ which is the recursive type you alluded to. An $F\colon \mathrm{Fin}$ knows all about its own attaching maps and stuff. This type comes with a “realization” map $R\colon \mathrm{Fin}\to \mathcal{U}$ to the type of types, which you can then factor through its $(-1)$-truncation: $\mathrm{Fin} \to \mathcal{U}_{\mathrm{Fin}} \hookrightarrow \mathcal{U}$. You might think of $\mathcal{U}_{\mathrm{Fin}}$ as the type of “types having the homotopy type of a finite complex”, except that there is the odd problem that I can’t necessarily lift a map $1\to \mathcal{U}_{\mathrm{Fin}}$ to a map $1\to \mathrm{Fin}$. I would guess that in a sheaf model, $\mathcal{U}_{\mathrm{Fin}}$ corresponds to objects which are “locally” finite complexes, e.g., whose stalks are equivalent to finite complexes.

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeNov 5th 2014
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexRight, exactly. In fact $Fin$ and $R$ have to be defined mutually, either by mutual recursion or induction-recursion, since the type of attaching maps at stage $n+1$ depends on knowing the realization of stage $n$. Your guess about models seems plausible.

    Right, exactly. In fact $Fin$ and $R$ have to be defined mutually, either by mutual recursion or induction-recursion, since the type of attaching maps at stage $n+1$ depends on knowing the realization of stage $n$. Your guess about models seems plausible.