I think Noah's answer is mostly right, but partly misleading, and explaining why will take too much space for a comment, so I'm posting a separate answer.

As Noah says, the main *conceptual* point is that HoTT forces us to un-confuse ourselves about the difference between a topological space and an $\infty$-groupoid, which are conceptually distinct but historically have been conflated in algebraic topology. (Actually, higher topos theory already pushes us in that direction, but HoTT is more insistent.)

On the other hand, the main *technical* point is that in "Book HoTT" we don't know how to define the "fundamental $\infty$-groupoid" functor that takes a topological space to its associated $\infty$-groupoid. Two important things to emphasize about this sentence are (1) it's a statement about a particular formal system (the one used in the HoTT Book), which is just one piece of the subject area of HoTT, and (2) it's (currently) a statement about ignorance rather than impossibility. However, it does have two important upshots:

In Book HoTT, to define a particular $\infty$-groupoid, you have to define it *as an $\infty$-groupoid*, i.e. using purely $\infty$-groupoidal notions; you can't "cheat" by defining it to be the fundamental $\infty$-groupoid of some topological space. (The definition also has to be "finitary" in some sense — it can use infinitary constructions, but they have to be finitely expressible such as by induction over the internal natural numbers.)

In Book HoTT, you are out of luck if you want to use topological spaces to prove things about their fundamental $\infty$-groupoids, or use fundamental $\infty$-groupoids to prove things about their originating topological spaces.

These problems, though significant, are part of the reason I said in the linked-to answer that "the promise of HoTT is not yet fully realized". Keep in mind that HoTT is only a few years old; we are already working on various ways to solve them.

The first of them is much less of an an insurmountable obstacle than you might think. Quite often, it turns out that an $\infty$-groupoid that's classically defined from some topological space also has a very natural presentation in purely $\infty$-categorical language, which can sometimes yield important new insight about it and enables new clean proofs in synthetic homotopy theory. The simplest example is the spheres: as Qiaochu mentioned in a comment, $S^n$ can be defined as freely generated by a point and an $n$-automorphism. Any CW-complex decomposition of a space is also a free presentation of its fundamental $\infty$-groupoid, though to be expressible in HoTT such a decomposition must be finite or "finitarily definable" (by internal induction). And classifying spaces can easily be defined using the univalent universe; see this blog post for instance. And recently, Ulrik Buchholtz and Egbert Rijke have made an important advance in unifying the latter two approaches to classifying spaces, using classification information as a way to finitarily present a CW-complex decomposition; in this paper they apply it to real projective spaces, but I think similar ideas should work rather more generally.

I don't know whether anyone has written down a definition of the $\infty$-groupoid $SU(n)$ in particular, but I'm confident that it will be possible. In fact it will probably be better to directly construct its classifying space $BSU(n)$ and then define $SU(n) = \Omega BSU(n)$, since that way the group structure of $SU(n)$ will arise automatically (delooping arbitrary $\infty$-groupoids is another thing we don't know how to do inside Book HoTT). I disagree with Noah that this would "not be constructing $SU(n)$ but something else equivalent to it": it would be a perfectly valid construction of *the $\infty$-groupoid* $SU(n)$, and an $\infty$-groupoid is only *defined* up to equivalence. What it wouldn't be is a proof that that $\infty$-groupoid is the fundamental $\infty$-groupoid of some topological space. Of course the name "$SU(n)$" for this $\infty$-groupoid is derived from the topological space of which classically it is the fundamental $\infty$-groupoid, but that accident of history is no reason to denigrate the existence of the $\infty$-groupoid in its own right.

The second problem above is rather more problematic, and there are various ways one might try to solve it. To start with, one might hope to prove that fundamental $\infty$-groupoids *are* definable in Book HoTT; but I don't know of anyone working on this, and I think the general feeling seems to be that it's probably not possible.

The other possibility is to introduce formal systems that are better than Book HoTT. Since the obstacle to defining fundamental $\infty$-groupoids in Book HoTT is their infinitary nature (you have to say "continuous maps $D^k \to X$ induce $k$-dimensional paths in $\Pi_\infty(X)$" for all $k$, coherently), the "obvious" way to proceed is to enhance it with ways to talk about infinitary things more cleanly. Here I think the state of the art is two-level type theory, a constellation of formal systems and ideas revolving around the idea of re-introducing (in a controlled way) the sort of "strict point-set-level equality" that Book HoTT mostly eschews. I don't think anyone has just yet applied this to defining fundamental $\infty$-groupoids, but it should be quite possible.

Another possibility is cohesive HoTT, which is less obvious and requires more re-training of our intuition, but in my opinion yields a more elegant result. Contrary to the former approach (and what Noah implied), cohesive HoTT does *not* require you to explicitly define manifolds, topological spaces, or even fundamental $\infty$-groupoids! In fact this is precisely the point: just as "plain" HoTT is a foundational theory whose basic objects can be regarded as $\infty$-groupoids, cohesive HoTT is a foundational theory whose basic objects can be regarded as *topological* $\infty$-groupoids (the motivating model consists of $\infty$-stacks on the site of Euclidean spaces $\mathbb{R}^n$). So just as in plain HoTT you don't need to define all the "$k$-simplices" of $S^n$ separately but they arise automatically from its presentation via generators and relations, in cohesive HoTT you don't need to define the topology of $\mathbb{R}^n$ explicitly but it arises automatically from the definition of the *set* $\mathbb{R}$ using Dedekind cuts. Moreover, you don't need to define the fundamental groupoid functor by explicitly specifying its $k$-paths either; it has a simple universal property relating this sort of "intrinsic topology" to the "intrinsic $\infty$-groupoidness" of plain HoTT.

So in conclusion, in cohesive HoTT you can define the $\infty$-groupoid $SU(n)$ *more easily* than in classical algebraic topology. Define $\mathbb{R}$ using Dedekind cuts, define $\mathbb{C}$ in the obvious way, and define the *set* $SU(n) \subseteq \mathbb{C}^{n^2}$ using the usual algebraic formulas, then apply the fundamental $\infty$-groupoid functor (which in cohesive HoTT is called its "shape", written ʃ $SU(n)$). You don't need to think about the topology of $\mathbb{C}$ or the manifold structure of $SU(n)$ at all; that gets carried along for the ride automatically. (You do, however, need to be a little careful to do things in the correct "constructive" way, which for instance means using the correct constructive notion of "Dedekind cut".)

or"groupoid" information in either case, then it happens automatically in cohesive HoTT that maps $\mathbb{S}^1 \to \mathrm{Vect}$ represent (not necessarily flat or trivial) continuous vector bundles over the topological circle. So I believe that (cohesive) HoTT really does do what you want. $\endgroup$11more comments