@bergarius Yes, correct.

That's why you should care about all topoi: a definition that doesn't advance our understanding of topoi is just a dirty hack. Of course, my PoV is that all good mathematics is based on homotopy theory, the rest either didn't catch up or isn't important. An extreme view, certainly.

@Mike If I'm working with vector spaces then I most certainly want them to natively carry groupoid information, since I want arbitrary vector bundles, not discrete (=flat) ones. I want the full $\infty$-category of real/complex vector spaces, I want K-theory and bordisms. The same with Banach algebras. One can certainly take the PoV that HoTT is just a nice tool for formalization and the rest of mathematics should be done as before, but I firmly believe that there is much more to be gained with proper definitions.

"$\mathbb R^n$ is contractible so it's definable" - this is a non-answer. The reason to define $\mathbb R^n$ is to work with structures defined over it: vector spaces, Banach algebras, moduli spaces of points, linear groups etc. None of this is possible if we blindly set $\mathbb R^n = 1$, and the roundabout way through set-theoretic definitions makes one question the use of homotopy foundations in the first place, since we'd go back to dealing with the same problems. This problem is related to the compactification of $Spec\, Z$: homotopy theory is its open part, and we need fiber at $\infty$.

@MikeShulman The fact that HoTT proofs work in any topos is both a blessing and a curse: yes, once we write a proof we get a result automatically in any context, but we are also forced to prove it in all topoi at once, which implies a much higher standard of proof than usual. In particular, it's hard to use topos-specific properties and we certainly can't rely on model-dependent statements, even if they could be useful.

There are two big problems with defining geometric objects like $SU(n)$ in HoTT. The first is that HoTT works only up to homotopy equivalence, so many basic objects like $\mathbb R^n$ are not natively definable (other than by a verbatim reproduction of set-theoretic definitions). The second is that HoTT is the language of higher topoi, so if you can define things like K-theory, bordisms and chromatic filtration, then you know how to do it in arbitrary topos, including examples like equivariant and motivic topoi. I don't know what should be complex bordism in those categories.

As others have answered, the product itself is constructed very easily and explicitly, and coincides with the classic products on the category of spectra. The bulk of Lurie's proof goes to construct the $E_\infty$-structure, i.e. provide all required associators, commutators, twistors and higher coherences between different products. Even stating it precisely isn't simple, thus a very abstract approach is required. The classical theories encode $E_\infty$-action in explicit geometric objects like actions of orthogonal or symmetric groups, so remaining structure is commutative "on the nose".

@მამუკაჯიბლაძე Are there idempotent-complete examples of such categories? In any case, $T$ will be terminal for the subcategory of objects that admit a map to $X$, which is as good as we can expect.

@მამუკაჯიბლაძე It's the same as $\Sigma_{x,y} (y = f(x))$.

@MikeShulman My objections are the same as against indiscriminately applying any other kind of completion (Cauchy, Ind, Kan, ...), however good the result may be. Thou shalt not make choices. As I show above, groupoids are equivalent up to Rezk completion iff they are Morita equivalent. Morita equivalence isn't equivalence --- fine with me, it was always this way for non-groupoids.

@მამუკაჯიბლაძე $P_f$ is always a fibration, but you should remember that it is a homotopy fibration with homotopy fibers, not the geometric one (which isn't definable within HoTT anyway). $P_f$ and $f$ are equivalent, this is the object classifier theorem I mentioned above. $||y = f(x)||$ is also a fibration, but it loses most information. Its total space is essentially the image of $f$.

@MikeShulman Yes, I meant to say "homotopy coherent groups", sorry for the confusion. I have re-written the last part and expanded on the problems and proofs that I mentioned. Essentially it boils down to when and where we should feel free to demand univalence. The example with sheaves was indeed misguided and I have deleted it.