I'm having real trouble understanding how the following definition of spheres can coincide with the suspension-based one:
(emphasis mine)
This seems to say that the 3-sphere is generated by a single point "base" and a single 3-loop "loop3" that says the identity of the identity of base has a path to itself. But if this is the case, what does can the Hopf fibration possibly look like from the 3-sphere to the 2-sphere? Well, maps f from the 3-sphere should be definable by its recursion principle, yeah? So we have to say:
f(base), how S3's base maps into a point in S2
f(loop3), how S3's 3-cell from id_(id_base) to id_(id_base) maps into S2, as a 3-cell id_(id_f(base)) to id_(id_f(base)).
But S2 only has trivial 3-cells, so loop3 must map to id_(id_(id_base)).
So any putative Hopf fibration must be the constant function λx.base. Surely this can't really be the S3 and S2 we know and love, can it?
In fact, we have two definitions of the n-sphere (which should coincide, but we haven’t proved this yet). The first is by induction on n: S1 is the circle, and the (n+1)-sphere is the suspension of the n-sphere. The second uses a fancy form of higher inductive types: First, we define the n-fold iterated loop space of a type, Ωn(A), by induction on n. Then, we define the n-sphere to be a higher inductive type with one point and one element of Ωn. The circle is generated by a point and a single 1-dimensional loop; the 2-sphere by a single point and a single 2-dimensional loop, and so on. This form of higher-inductive type is a bit unusual (and has not been formally studied): for each instantiation of n, the n-loop constructor is an element of a path type of Sn, but the level of iteration of the path type depends on n, and when n is a variable, Ωn is not syntactically a path type. However, the fact that the homotopy groups have come out right so far provides some indication that this is a sensible notion.
(emphasis mine)
This seems to say that the 3-sphere is generated by a single point "base" and a single 3-loop "loop3" that says the identity of the identity of base has a path to itself. But if this is the case, what does can the Hopf fibration possibly look like from the 3-sphere to the 2-sphere? Well, maps f from the 3-sphere should be definable by its recursion principle, yeah? So we have to say:
f(base), how S3's base maps into a point in S2
f(loop3), how S3's 3-cell from id_(id_base) to id_(id_base) maps into S2, as a 3-cell id_(id_f(base)) to id_(id_f(base)).
But S2 only has trivial 3-cells, so loop3 must map to id_(id_(id_base)).
So any putative Hopf fibration must be the constant function λx.base. Surely this can't really be the S3 and S2 we know and love, can it?