Post #1441649
2026-04-01 22:10 UTC
@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.
Replies (1)
-
@jcreed@mastodon.social 2026-04-01 22:11
@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)