I'm sorry if this is well-known. I'm new to stable homotopy theory.

There are many models of spectra, and an answer to this MO post says most of them are equivalent, even equivalent while taking the symmetric monoidal structure (smash product) into account.

My question is motivated by wanting to know how these equivalences are established. There's a clean development of the stable $\infty$-category of spectra and the smash product thereof in Lurie's Higher Algebra, and both are characterized by universal properties, but it seems anachronistic to say that checking these universal properties is the way to establish the equivalence of different models.

Finally, even if one is able to establish that the different model categories of spectra with smash product (symmetric, orthogonal, what have have you) are equivalent, it seems like this doesn't easily construct a functor from one model to another--for instance, it's not obvious how to take two arbitrary Omega spectra (more or less the model in Higher Algebra) and spit out a pair of symmetric spectra while verifying that their smash products in either model are equivalent.

Is there a written account of:

- Historical efforts that failed, and in particular, attempted models for spectra that are
*not*equivalent to modern models, - A list of equivalent models,
- How we know the models are equivalent, and
- When known, functors between the models?