2026-04-01 21:56 UTC
Suppose 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.
Replies (2)
-
@jcreed@mastodon.social 2026-04-01 21:57
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.
-
@rntz@recurse.social 2026-04-01 22:10
@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.