So my next relatively less ambitious goal is just to prove that the suspension of a space X is equivalent to the "equatorial" suspension of X. The suspension S(X) is defined as the type with
n : S(X)
s : S(X)
for each x in X, a path n = s
and the equatorial suspension is defined as
n : ES(X)
s : ES(X)
for each x in X, a point e(x) : ES(X)
for each x in X, a path n = e(x)
for each x in X, a path s = e(x)
The suspension is a fundamental operation from topology: the suspension of a disjoint two-point set (also known as the 0-sphere) is the circle (aka the 1-sphere) and the suspension of the circle is the 2-sphere, and of the 2-sphere is the 3-sphere, and so on.
The "equatorial" version is only different in how it's defined. Topologically (and type-theoretically, by univalence) it should be identical.