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.
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?