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.