Definition of a map of (pre)spectra in HoTT

homotopy-theory homotopy-type-theory spectra

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$.)

Related

Calculus for the Practical Man: Chapter 4, Problem 16
Definition of Conjugacy Class
Computing $\lim_{n \to \infty}\frac{n-H_{n}-\sum_{j\le n}\frac{\Omega\left(j\right)}{j}+\sum_{j\le n}\frac{\omega\left(j\right)}{j}}{n}$
Probability of getting certain score in Drop Dead
How to calculate the radius of the curved side of a triangle?
A Generalization of Beatty's Theorem
Solving the following Diophantine equation: $m^2=n^5-5$
What is $\mathcal{R}$?
Finite Groups with a subgroup of every possible index
What is the Galois group of the splitting field of $X^8-3$ over $\mathbb{Q}$?
A structural proof that $ax=xa$ forms a monoid
Formula for $\int_0^\infty \frac{\log(1+x^2)}{\sqrt{(a^2+x^2)(b^2+x^2)}}dx$