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. On Tuesday, 18 September 2018 17:13:26 UTC+1, Michael Shulman wrote: > > Some introductions are: > https://ncatlab.org/nlab/show/trace > https://arxiv.org/abs/1107.6032 > -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.