[HoTT] Re: Characteristic Classes for Types

[Ali Caglayan <alizter@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 4589 bytes --]

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.

[-- Attachment #1.2: Type: text/html, Size: 5763 bytes --]