So I have been reading your exposition and it seems to me the following things will need to be done in order to define the euler characteristic:
1. Sort out the symmetric monoidal structure on the category of Spectra.
- The main obstacle is the cohereance of the smash product (for spectra this follows from spaces I believe?).
2. Define the suspension spectrum of a space
- This should be simple to define as a prespectrum which can be spectrified.
3. Define the "stable normal bundle" of a space
- Isn't this something usually done on a manifold?
4. Define the Thom spectrum of a vector bundle
- I have no idea what this is but I hope it can be defined. I have no idea what a vector bundle in HoTT is however.