jcreedSuppose I assume the existence of a countable sequence of types A₀, A₁, A₂, … such that A₀ = ΣA₁, A₁ = ΣA₂, etc., a tower of suspensions going down.
Is A₀ necessarily contractible? Be careful not to think I'm asking a very similar-sounding but distinct question: I know if the sequence was ordered the other way around, with A₀ = 0, A₁ = ΣA₀, A₂ = ΣA₁, etc. then the colimit of the sequence ("the infinite-dimensional sphere") would be contractible.
Naïm Camille Favier@jcreed at least yes assuming Whitehead's principle, since A₀ is n-connected for all n.
rntz@jcreed I don't think I understand the notation here. What is ΣA₁? I know what (Σ(x:X) P x) is. But I don't know what (ΣA) is when A is just a type.
@rntz https://en.wikipedia.org/wiki/Suspension_(topology) (but I'm thinking of it in terms of HoTT. It is confusing that sigma is also the standard symbol for this in addition to dependent sum types)
Omar Antolín@jcreed Take the following with a grain of salt, since I'm a homotopy theorist, not a homotopy type theorist. Classically, what you would get, if these were spaces, is that A₀ is weakly contractible: for any n, it is (n-1)-connected because A₀ = Σⁿ Aₙ. This much should also be true in HoTT, so πₙ(A₀) = 0 for all n.
Now, I gather that HoTT has models in every (∞,1)-topos. But not every (∞,1)-topos is hypercomplete. In a hypercomplete (∞,1)-topos an object like A₀ with all homotopy groups vanishing would have to be contractible, but not so in a non-hypercomplete (∞,1)-topos.
I think this probably means that in HoTT A₀ is not necessarily contractible —but it still has vanishing homotopy groups, so, for example, all it's truncations ‖A₀‖ₙ are contractible.