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.
If it's possible for A₀ to not be trivial, then I have a hunch it ought to behave kind of like a "negative point"; I think for any function B → C I can naturally construct a map from a colimit of C many copies of A₀ to B many copies of A₀.