Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 11 of 11
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! :-)
Not in the sense of being implemented in a proof assistant, no.
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.
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.
What is a “finite cell complex” in HoTT? What does “finite cell complex” correspond to in terms of an ∞-topos model?
I’m really asking: how do you construct the “type” of finite cell complexes in HoTT?
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 Sn→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 Sn→X.
Either way, the finite cell complexes in an ∞-topos model will be the tensors of 1 by ordinary finite cell complexes in ∞Gpd, or equivalently the images of ordinary finite cell complexes under the left adjoint Δ:∞Gpd→H to the global sections functor.
I don’t think that can be right. Maps Sp→Sq in H need not always arise from ∞Gpd.
For instance, consider H=∞Gpd/T for some space T. The internal mapping object MapT(Sk,Sn) is the projection map Map(Sk,Sn)×T→T. It’s 0-truncation is (πkSn)×T→T, so the “homotopy group” is what you expect. But the space of sections of MapT(Sk,Sn)→T is equivalent to Map(Sk×T,Sn), so its π0 could be much bigger. (Or smaller, if T=∅.)
Oh, yes, you’re right. So there could be more finite cell complexes in some model than there are in ∞Gpd.
I guess it’s complicated. There is a type Fin which is the recursive type you alluded to. An F:Fin knows all about its own attaching maps and stuff. This type comes with a “realization” map R:Fin→𝒰 to the type of types, which you can then factor through its (−1)-truncation: Fin→𝒰Fin↪𝒰. You might think of 𝒰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→𝒰Fin to a map 1→Fin. I would guess that in a sheaf model, 𝒰Fin corresponds to objects which are “locally” finite complexes, e.g., whose stalks are equivalent to finite complexes.
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.
1 to 11 of 11