Post #975655
2026-04-01 21:56 UTC
Replies (3)
-
@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.
-
@oantolin@mathstodon.xyz 2026-04-01 23:12
@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.