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 S

^{3}'s base maps into a point in S

^{2}

f(loop3), how S

^{3}'s 3-cell from id_(id_base) to id_(id_base) maps into S

^{2}, as a 3-cell id_(id_f(base)) to id_(id_f(base)).

But S

^{2}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 S

^{3}and S

^{2}we know and love, can it?