Re: [HoTT] Re: Characteristic Classes for Types

[Michael Shulman <shulman@sandiego.edu>]

The Hurewicz theorem is actually a theorem about *homology*, which is
indeed undeveloped in HoTT.  Cohomology is much better understood.
The questions you're asking *do* have a significant homotopical
nature, and so I think it *is* reasonably likely that the synthetic
approach -- especially augmented with cohesion -- will have something
interesting to contribute to them.  But not yet.

I think really the best answer to questions like this is Ali's last
paragraph: start by reading up on the state of the art.  You'll get a
much better sense that way of what is known, what sort of things are
easy, what sort of things are hard, and what sort of things are likely
to be doable soon.  (If state-of-the-art papers are hard to
understand, then start with earlier stuff instead, like the HoTT
Book.)

On Thu, Sep 27, 2018 at 5:38 PM Ali Caglayan <alizter@gmail.com> wrote:
>
> 1. This could be possible once a vector bundle has been fully defined. The idea behind characteristic classes is to classify certain vector bundles with cohomology. This however may be a bit in the future as, for example, grassmannians have not yet been defined. Also orthogonal groups are not yet defined. So it is impossible to say right now if this can be done but it seems likely.
>
> 2. Cohomology in HoTT is not by default singular cohomology like in algebraic topology. In HoTT we take the definition of cohomology to be the (truncated) set of maps to an Eilenberg-Maclane space. Concering cohomology operations, this should definitely be possible. Literature on cohomology has come out in the last few years so expect more to be written about it.
>
> 3. Atiyah-Singer would need quite a lot of work, not to mention the fact it involves differential structure. Which at the moment it is expected that differential cohesive HoTT may be able to tackle such a theorem. HoTT on it's own is quite good at talking about purely homotopical structure. This is an important point because many topological/manifoldy theorems are not necesserily homotopical in nature. They may depend on extra structure that HoTT cannot really describe adequately yet. Take for example Riemann-Roch which can be considered a special case of Atiyah-Singer. It would need a good amount of algebraic geometry to be defined and/or proven in order to state the theorem. Which is unliekly to come around in the next few years. This doesn't mean it couldn't happen.
>
> Just to show you how underdeveloped cohomology in HoTT is at the moment, an "elementary" theorem of algebraic topology, the Hurewicz theorem, has not been proven yet. Though I believe it will be tackled soon.
>
> Types are not topological spaces, they are more literally homotopy types. This is why I personally, found "the Hodge structure of a type" to be not within our current viewpoint although Steve Awodey's point about the speed of the development of HoTT has been considered.
>
> And one final thing: One of the reasons algebraic topologists are exicited about using and developing HoTT is that it gives a synthetic foundation to many "purely homotopical" ideas used in algebraic topology that have proofs and constructions relient on outside ideas or formalisms. This isn't necesserily a bad thing (look at cobordisms in stable homotopy) however some simpler areas of the subject should be able to hold their own. (As I understand).
>
> Therefore it stands to reason that it is unlikely that HoTT will bring anything new to the table when it comes to the ideas you are talking about. HoTT essentially provides a synthetic way to reason about homotopy types, but it isn't an enlightening viewpoint for theorems not homotopic in nature.
>
> And really finally this time: Have a look around at what people are doing in HoTT at the moment. For example Floris van Doorn's thesis where spectral sequences for cohomology have been developed in HoTT and formalised in the Spectral library for the Lean proof assistant. The agda formalisation of HoTT also usually has a lot of the latest gadgets of snythetic homootpy theory. Which is a fascinating subject if I do say so myself, but it isn't algebraic topology. There is a massive intersection but don't take them to be the same thing.
>
> Anyway if you have read this for congratulations.
>
> Ali Caglayan
>
> On Thursday, 27 September 2018 14:10:09 UTC+1, Juan Ospina wrote:
>>
>> Recently, there was a post about the Euler characteristic of a type and other post about Hodge structure of a type.  Then my questions are:
>>
>> 1) It is possible to construct characteristic classes  (Wu, Stiefel-Whitney, Chern, Pontryagin classes)    for an arbitrary type in HoTT?
>>
>> 2) It is possible to construct singular cohomology for a type and the corresponding Steenrod operations?
>>
>> 3) It is possible to construct an Aityah-Singer index theorem for an arbitrary type (a type fibered with other type).
>>
>> 4) It is possible to construct integrality theores for the characteristic numbers of an arbitrary fibered type?
>>
>>
>> Many thanks.
>>
>> Juan Ospina
>> Medellín,  Colombia
>>
>>
> --
> 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.