[-- Attachment #1.1: Type: text/plain, Size: 1243 bytes --] We currently have enough machinary to (kind of) define Betti numbers (for homology see Floris van Doorn's thesis <http://florisvandoorn.com/papers/dissertation.pdf>). I am confident that soon we can start compting Betti numbers of some types. This would allow us to define the euler characterstic E : U --> N of a type. If classical algebraic topology tells us anything this will satisfy a lot of neat identities. In fact consider U as a semiring with + and * as the operations. E is a semiring homomorphism to N (the initial semiring (is this relavent?)). In other words we should have E(X + Y) = E(X) + E(Y) E(X * Y) = E(X) E(Y) and even maybe, subject to some conditions, a given type family P : X --> U would satisfy E( (x : X) * P(x) ) = E(X) * E(P(x_0)) This would be a cool invariant to have. Unfortunately as it stands, homology is a bit unwieldy. Perhaps rationalising spaces would help? Any thoughts or suggestions? -- 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. [-- Attachment #1.2: Type: text/html, Size: 1577 bytes --]

[-- Attachment #1: Type: text/plain, Size: 1993 bytes --] 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. On Mon, 17 Sep 2018 at 21:11, Ali Caglayan <alizter@gmail.com> wrote: > We currently have enough machinary to (kind of) define Betti numbers (for > homology see Floris van Doorn's thesis > <http://florisvandoorn.com/papers/dissertation.pdf>). I am confident that > soon we can start compting Betti numbers of some types. This would allow us > to define the euler characterstic E : U --> N of a type. If classical > algebraic topology tells us anything this will satisfy a lot of neat > identities. > > In fact consider U as a semiring with + and * as the operations. E is a > semiring homomorphism to N (the initial semiring (is this relavent?)). In > other words we should have > > E(X + Y) = E(X) + E(Y) > E(X * Y) = E(X) E(Y) > > and even maybe, subject to some conditions, a given type family P : X --> > U would satisfy E( (x : X) * P(x) ) = E(X) * E(P(x_0)) > > This would be a cool invariant to have. Unfortunately as it stands, > homology is a bit unwieldy. Perhaps rationalising spaces would help? > > Any thoughts or suggestions? > > -- > 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. [-- Attachment #2: Type: text/html, Size: 2743 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 787 bytes --] 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. [-- Attachment #1.2: Type: text/html, Size: 1136 bytes --]

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.

[-- Attachment #1.1: Type: text/plain, Size: 1142 bytes --] 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. [-- Attachment #1.2: Type: text/html, Size: 1493 bytes --]

Some introductions are: https://ncatlab.org/nlab/show/trace https://arxiv.org/abs/1107.6032 On Tue, Sep 18, 2018 at 3:54 AM Ali Caglayan <alizter@gmail.com> wrote: > > 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. -- 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.

[-- Attachment #1.1: Type: text/plain, Size: 530 bytes --] Thank you for the paper Mike, it is very cool indeed! 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. [-- Attachment #1.2: Type: text/html, Size: 1790 bytes --]

[-- Attachment #1.1: Type: text/plain, Size: 1217 bytes --] 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. [-- Attachment #1.2: Type: text/html, Size: 2623 bytes --]

From an abstract homotopical point of view, the "finite types", i.e. those that have Euler characteristics, are *by definition* those whose suspension spectrum is dualizable. The dual object is then just part of the definition of "dualizable". Formal arguments applicable to any symmetric monoidal stable homotopy theory (e.g. (oo,1)-category or derivator, but which would have to be formalized differently in HoTT) should imply that such dualizable objects are closed under finite colimits, hence include all "finite cell complexes" represented as HITs. The dual in such a case is constructed formally as a corresponding limit of duals (since dualization is a contravariant equivalence on the dualizable objects). The business of stable normal bundles and Thom spectra is how one shows that the oo-groupoid presented by a manifold has this formal dualizability property. Book HoTT has no known way to go from a point-set-topological object, like a manifold, to a type (i.e. synthetic oo-groupoid) that it presents. It may be possible in a two-level type theory to construct the "fundamental oo-groupoid" of a point-set-level space internally as a semisimplicial type and then take its "realization" to get a single type. Alternatively, Cohesive HoTT provides an abstract context in which to talk about point-set-level spaces "synthetically" in parallel to homotopy-level spaces, where this presentation operation is represented by the "shape" modality. In either of these contexts, one could attempt to prove, using some analogue of Thom spectra of normal bundles, that the "shape" of a manifold is a dualizable type. It may also be possible to study in Book HoTT something with the "homotopical content" of a vector bundle, e.g. a corresponding cohomology class regarded as a map into some classifying space, as in the work of Rijke and Buchholtz on projective spaces. I don't know whether this would be helpful for dualizability, however. On Tue, Sep 18, 2018 at 5:04 PM Ali Caglayan <alizter@gmail.com> wrote: > > 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. -- 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.