From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORBR5OW3OQKGQEKJMCGRA@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qt1-x83f.google.com (mail-qt1-x83f.google.com [IPv6:2607:f8b0:4864:20::83f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0cdaa0e8 for ; Fri, 28 Sep 2018 02:51:53 +0000 (UTC) Received: by mail-qt1-x83f.google.com with SMTP id h26-v6sf4308338qtp.18 for ; Thu, 27 Sep 2018 19:51:52 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1538103112; cv=pass; d=google.com; s=arc-20160816; b=X8pr4eLfHZ7hET8VtlbfNamE3X0rQ2o+xZgX2vXM5uhYDGhtjGvk2wWqZXLY9UntrE //77ekRYANqlw7DRsPN4yQ62aITjVTxXXWaFF2xHSjCIXSq2ParZPfl7GuRvntTZrOw0 78A867ED1/pU/dCPgSgpYqIyI5dCrBtCjXo0j6HnBiMF1ZFZxGHg6c5S+Lt/DOX3FlqZ +oVP1wuRuSY03Clu7a+KhJRMu/+RyrRowxQXIV4W+tPeVwlGe94SYf2kyBW1DYQxWbmm J+FwWVVdjKnx6zFuM5CVf3wWPdcaVoA99PDuTRUhtJBiJGVVww9/NSuD8nU+t5TAsA6i 0IfQ== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=LdSouXbEbs61OQjIaePBGs25kUno88TbfBrAQCmHjIw=; b=e7O17YQXkerwGICEwHZtwDPQLxbOOkp5ZXw8uxjvkZ68yZ9yi0Ubswzv3xU5ib9ZcX B1Oj84CqcFvOkZNlt6Cj/A+uRTJiFk5q1IW4Zg7XoA3cc/9/We6zNelKf9WT9Tx69ZGk 0/hhHmDimCcyL1M5Zathh1zsM4XO7UEQqWrovu78PR1jmvZF+sgyl1bF76U6gOM6Cx83 +Sb42ZxCQ4Dz9k6B1dwLNFWwCElXFiTEG1eb0bSxgUqEXITSKl4ydQ7XBucm5Qgemrtx I/X3z8rxxNdfY86T4RyBzZOr/1ZfFJVHVN2/WswaX2fuJGRdtKSLjntM1O39bfX+U9A3 NXKg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WduL7uQJ; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b30 as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=LdSouXbEbs61OQjIaePBGs25kUno88TbfBrAQCmHjIw=; b=RfRCn5ahjIRPyLOdbL4IHZwwfEvwKbq8QUiW2KAnGhZuf4yigx7JZtuXBGsmOS1PQ1 CGyv6kpbiJu8l/w9s15/W1MJCHRhkRz24MPBWAGrvrVQAbi+x5K7E0U37eY4RBfCY+gm HntMjBxmvaS5G7gBQ8lDnDRvx2awLPabaHgkYrTLwUfrIi1IS07+RoFGS1j6tRvxOXMy BJoAWwSU0EmbR0NbyA+DGRJPM1zvtxTVyQZwidPMs+1qataLs6eLzptGS91bktoAoVzo B/0C8oEpsy9drsa1TasdKVA3t3Fl2xAaMlHI8pPpq+qJ8ECF11tx2chQnSqtlxZ0TEB4 3DTA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=LdSouXbEbs61OQjIaePBGs25kUno88TbfBrAQCmHjIw=; b=PzCJiuhR9C9XlUD+sPmmJQRlLto4cCMsQ/CTQPK2lGEOEEyjZ56wVmerGbdE8GD2vi qW05l00iDG8z7LBURbc/lp3caGsTsMMYXa8W6o4QauLB6kXqVWXKRFH5cIO2JymHP8hH Osfx/X6VzwONThz2CBrsfYzNxRcxIA/0eYxQY5bYH6uoPEfSwxa8zgfvWPCxV1dVrToE JlgURouiyf5y8trZqIuAyHnsOql/GofFIQznzCJOEOhmwuLw2qnMNSNx2fMAH0GvNjEa 5WB3JzmfJ2pzHawgGQnLMcCUtzI7DZ6i5qnj/iMiCmzl1+Y2Ju4IaxwdOvgLArJ0q5rd +KvA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfojXFMIx39SJHMUzEPRZutpaazx5ZUyKiBv1uBUdiJEElOrLUdo5 1qEMsYpSwu5qoOYm8P6kS6M= X-Google-Smtp-Source: ACcGV62oSwT2LWE4gs8M8hxo4kisj051hjwhmizMK7+4c+qVqUxmTqFA7d6e4LZcaacerFd/wsXzbg== X-Received: by 2002:a37:6514:: with SMTP id z20-v6mr79740qkb.2.1538103111937; Thu, 27 Sep 2018 19:51:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:ba1d:: with SMTP id w29-v6ls2992373qvf.3.gmail; Thu, 27 Sep 2018 19:51:51 -0700 (PDT) X-Received: by 2002:a0c:e792:: with SMTP id x18-v6mr6842589qvn.32.1538103111594; Thu, 27 Sep 2018 19:51:51 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1538103111; cv=none; d=google.com; s=arc-20160816; b=cZe8lHfOEsCCb3xG2NV77N6x9utvbxepbW4Quo8ZhW7Xt8GAWLukfFvtObd8UHP1nn OW9CEGEDbsVkhNAMFrSY8w/DRHj6dLWD5hDzL70iNtV8bJk9THoa0o7eYPMl9Tun1Kn8 w9f8Zrj5DfhibhsZwTyGAFHCoYddzfvEyIuAMQVnGzgCUul8PusaOLC95zM3Ha4pkDBW aeVitFyncurYCnOf78YpUtfs20KgwdolZgEovMCpyaCMJeOKHUJoY/agOK407UTavPL0 QFkxWqCLwL8cFlVBBS5Lo/wTo1DFfZA5Fs3M5sIf/qVCz+HfXe+IKVn1gVI8F1d7aUs4 CVUg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=bCaU3E/6VZibbs69Fg9KyS7GMUBfxwiamlhPldWYCME=; b=mWOhjn3zLbzPbMkx71yy+6exMP7sWEtKh5RjnjK5KJGsa1xBt2caxND45q/raKLpmn RqoqgUFTwRZJZn+2ddb8ZVetwmps2PGhmCCtVXnPpjC/K9dzB7uYb0DpK1WaY9nhzimU 2LcOA9s/ZbISmB9I7Mm3k2dmkhGSSA7Di371kGnmAmABDz0MuIyTeQQAmTPZcIpQBos8 hsd3lxH4K18nimjsfcaFAQyjTODtA18N9FkN9I3i8uYNIo/uS2I2NI2GSLiA2I0Dt8e4 3KxeziCjriQocnTcZxseXJ2NsKmnakeyxkxfUK6RYhK5yj2OfoS4nUoic0VPSQoHYrsz Rolg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WduL7uQJ; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b30 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb30.google.com (mail-yb1-xb30.google.com. [2607:f8b0:4864:20::b30]) by gmr-mx.google.com with ESMTPS id l15-v6si214063qta.0.2018.09.27.19.51.51 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 27 Sep 2018 19:51:51 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b30 as permitted sender) client-ip=2607:f8b0:4864:20::b30; Received: by mail-yb1-xb30.google.com with SMTP id p74-v6so2031736ybc.9 for ; Thu, 27 Sep 2018 19:51:51 -0700 (PDT) X-Received: by 2002:a25:7396:: with SMTP id o144-v6mr7660782ybc.103.1538103111154; Thu, 27 Sep 2018 19:51:51 -0700 (PDT) Received: from mail-yw1-f53.google.com (mail-yw1-f53.google.com. [209.85.161.53]) by smtp.gmail.com with ESMTPSA id d6-v6sm1413509ywa.85.2018.09.27.19.51.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 27 Sep 2018 19:51:50 -0700 (PDT) Received: by mail-yw1-f53.google.com with SMTP id y76-v6so2021375ywd.2 for ; Thu, 27 Sep 2018 19:51:50 -0700 (PDT) X-Received: by 2002:a0d:ea03:: with SMTP id t3-v6mr7583847ywe.496.1538103109801; Thu, 27 Sep 2018 19:51:49 -0700 (PDT) MIME-Version: 1.0 References: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> In-Reply-To: From: Michael Shulman Date: Thu, 27 Sep 2018 19:51:36 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Characteristic Classes for Types To: Ali Caglayan Cc: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WduL7uQJ; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b30 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , 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 wrote: > > 1. This could be possible once a vector bundle has been fully defined. Th= e idea behind characteristic classes is to classify certain vector bundles = with cohomology. This however may be a bit in the future as, for example, g= rassmannians 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 se= ems likely. > > 2. Cohomology in HoTT is not by default singular cohomology like in algeb= raic topology. In HoTT we take the definition of cohomology to be the (trun= cated) set of maps to an Eilenberg-Maclane space. Concering cohomology oper= ations, this should definitely be possible. Literature on cohomology has co= me 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 i= t's own is quite good at talking about purely homotopical structure. This i= s an important point because many topological/manifoldy theorems are not ne= cesserily homotopical in nature. They may depend on extra structure that Ho= TT cannot really describe adequately yet. Take for example Riemann-Roch whi= ch 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 d= oesn'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 no= t 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 exicite= d about using and developing HoTT is that it gives a synthetic foundation t= o many "purely homotopical" ideas used in algebraic topology that have proo= fs and constructions relient on outside ideas or formalisms. This isn't nec= esserily a bad thing (look at cobordisms in stable homotopy) however some s= impler areas of the subject should be able to hold their own. (As I underst= and). > > Therefore it stands to reason that it is unlikely that HoTT will bring an= ything new to the table when it comes to the ideas you are talking about. H= oTT essentially provides a synthetic way to reason about homotopy types, bu= t 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 spectra= l sequences for cohomology have been developed in HoTT and formalised in th= e Spectral library for the Lean proof assistant. The agda formalisation of = HoTT also usually has a lot of the latest gadgets of snythetic homootpy the= ory. Which is a fascinating subject if I do say so myself, but it isn't alg= ebraic 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-Whit= ney, Chern, Pontryagin classes) for an arbitrary type in HoTT? >> >> 2) It is possible to construct singular cohomology for a type and the co= rresponding Steenrod operations? >> >> 3) It is possible to construct an Aityah-Singer index theorem for an arb= itrary type (a type fibered with other type). >> >> 4) It is possible to construct integrality theores for the characteristi= c numbers of an arbitrary fibered type? >> >> >> Many thanks. >> >> Juan Ospina >> Medell=C3=ADn, 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. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.