Tinkered a little bit more in the evening with Agda. Instead of flailing around wildly, I went through the proof that the two-point interval is contractible and saw how to build paths from transport-expressions to ap-expressions. Having ap-expressions being important because then I can actually use the β-conversions that constitute the induction principle's content for the paths in a higher inductive type.

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.
Tags:
• Post a new comment

#### Error

Anonymous comments are disabled in this journal

default userpic