Re: [HoTT] Euler characteristic of a type

[Michael Shulman <shulman@sandiego.edu>]

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.
On Mon, Sep 17, 2018 at 4:07 PM Ali Caglayan <alizter@gmail.com> wrote:
>
> This would be some subuniverse of "compact" spaces I assume.
>
> On Monday, 17 September 2018 23:37:03 UTC+1, Floris van Doorn wrote:
>>
>> Clearly we cannot define E on the whole universe, but only on a subuniverse.
>> For example, we could define it on the subuniverse of types with finitely generated homology groups. For the Euler characteristic we will also need that the betti numbers are eventually 0. Other than that, I agree that these properties should hold in HoTT.
>
> --
> 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.

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