Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Juan Ospina <jospina65@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: [HoTT] Re: Characteristic Classes for Types
Date: Thu, 27 Sep 2018 18:00:55 -0700 (PDT)	[thread overview]
Message-ID: <ed272cda-60ca-455c-a862-f49eba5fb6ac@googlegroups.com> (raw)
In-Reply-To: <d48b3ec2-c96d-412c-bb6b-0c3fa0a96586@googlegroups.com>


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

Many thanks for your comments which are very instructive.   Actually I am 
trying to understand  anything in the Floris van Doorn's thesis, 
particularly the formalization in HoTT for the *Atiyah*-*Hirzebruch 
spectral* sequence  and the  *Leray*-*Serre spectral* sequence.

On Thursday, September 27, 2018 at 7:38:09 PM UTC-5, Ali Caglayan 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.

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

  reply	other threads:[~2018-09-28  1:00 UTC|newest]

Thread overview: 12+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2018-09-27 13:10 [HoTT] " Juan Ospina
2018-09-28  0:38 ` [HoTT] " Ali Caglayan
2018-09-28  1:00   ` Juan Ospina [this message]
2018-09-28  1:04   ` Juan Ospina
2018-09-28  2:51   ` Michael Shulman
2018-09-28  5:59 ` [HoTT] the weak infinite groupoid in Simple Type Theory José Manuel Rodriguez Caballero
2018-09-28 19:21   ` Michael Shulman
2018-09-28 20:27     ` José Manuel Rodriguez Caballero
2018-10-01 14:43       ` Michael Shulman
2018-10-01 14:53         ` Steve Awodey
2018-10-01 23:14           ` José Manuel Rodriguez Caballero
2018-10-02 16:20             ` Michael Shulman

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=ed272cda-60ca-455c-a862-f49eba5fb6ac@googlegroups.com \
    --to=jospina65@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).