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.
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)
