I'm trying to pick up some homotopy theory by reading various HoTT sources (I find it much easier than reading classical homotopy theory books). In Floris Van Doorn's PhD thesis he defines (pre)spectra as shown below:
It seems that a map of (pre)spectra is not required to be degreewise pointed. Is this a typo (he missed the star on the highlighted arrow?), or is this intentional?
This is surely a typo. Pretty much everything about spectra takes place in the pointed category and every map in sight is pointed. I'm not familiar with this particular exposition in the context of HoTT, but I've never seen any similar definition in any other context that would use unpointed maps. (And if the $f$ maps were not pointed, it is not clear what $\Omega f_{n+1}$ would even mean in the specification of $p$.)