This is a nice idea. If we could somehow overcome the lack of coherance of smashes how would we go about defining the trace of an object in a symmetric monoidal category? 

On Tuesday, 18 September 2018 07:26:04 UTC+1, Michael Shulman wrote:

A more "homotopical" way to define the Euler characteristic is as the
trace of an identity map of a suspension spectrum in the symmetric
monoidal category of spectra.  It also generalizes to a definition of
the Lefschetz number, and many of the formal properties of Euler
characteristic follow formally from this definition and the properties
of trace.  I suspect this would also be a useful version of the
definition in HoTT, although of course there are currently technical
obstacles to working with such things as the symmetric monoidal smash
product of spectra.