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

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