From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDF4ZP7WUQGRBMVNWPOQKGQE5I4GACY@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.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ot1-x340.google.com (mail-ot1-x340.google.com [IPv6:2607:f8b0:4864:20::340]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6e4d498f for ; Thu, 27 Sep 2018 13:10:11 +0000 (UTC) Received: by mail-ot1-x340.google.com with SMTP id s69-v6sf2966514ota.13 for ; Thu, 27 Sep 2018 06:10:11 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=njjlGkxtK0U9mjENlKM1brdhZVrpxV7UOQqA1Jgyvko=; b=mEEVTEl8rkCMtrIsoRQZKgr02aWpClaYtLfFsNpgnTY6l/Zfv2qT2iFLUpfewzV+HJ J7q3t/cEkH3bOYBiG6VcXsFHXuGLvBswgomfShr8i1q0oxWCXmW2BYIIJ/SW9g5fRklE vCpA992wM7gxA28hZnBAyP52CcJDa7z/qXJfa7ONKOjanM904btxryyNOxoObLOPmeL9 kWs0VUV/pvSLRtKHG2a7QwDlTYH5UVwpFUfT9UTKjuL0bzijSA3IZoregDyBnQbbHXSA XoRKBOYaXteMRv4btvJ+rgc4wsAWtErh2a7pPqlxCp9+fSw9ixCGobkg1JV+szudbshn L+Jg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=njjlGkxtK0U9mjENlKM1brdhZVrpxV7UOQqA1Jgyvko=; b=Ctf1JIpe5Wz9HB58aeAyvf64Kx4XqLrVmzvlN5lb2gM2xnWSdjsi5Yn7Z+JlvtqME6 mhzqL+b5oIcx+BMNE842lp4NNEd7HahXgxRL4QDD7HX2Al/kp7VILd7y09lu06kFuuLH /bsSK6vuoW97ZToNs94ZhNGgRCa3qJwaTcK7Zp1dW6xuGOhDD7sVffsY009CZhWTL7fz cCiMSP1RSGRcd9Efaf9+fae4IQyIaag5KB8IX/AwJclWbQEYo8mtcItPMv99gSP0XoG2 3+eRVxtfLatRkQLDkqnUi9dY876Q4+oqnDiu2Dp1nbpB49qUk7BBW5rm3/DVPRJDbFnz UdeA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=njjlGkxtK0U9mjENlKM1brdhZVrpxV7UOQqA1Jgyvko=; b=ImlyulU3k26XetGFx6k/mDpR0oHJeXEYCIurC6KcLpTB0z8hEwOcB3mtEr+aQQRIPg ybc4lIHL/mnW5Kt4YQESlnOI3i83TD8DVvnd/0H4IsZsKuewYiyPr4GDCcZrYG3eZGkQ hU3pdf+84zxRrD1EY/T3iTkuxLPHEbmR1jrG/oZN3VisgciYNI1n+M/uaCJSBHEE1ECk F1TCLaDcNMwk6ROWNcA4Pqjx+uMPk0EtfzuSrPBzGrWzK8fohhjWotIYpQmOtmkRnHGl 91EtXH1Bohb3KQQ+oSKRbUnJGnJSrBN7FUWlCgND8+4TSmkfTzQHuVeCTk/EQsG38Ync rpHA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfogpvdmhJkvAYe7jxaFHjAe8G1kSU7DYqqRYALgJkgu168iHccPb 6unR3I+PI23cvC+JB0VG3Kk= X-Google-Smtp-Source: ACcGV63CP0z9V9dJxWJo3I+xmFXnFdKPCSw/Qt4MU5wQEScdh7d1VEyMBnKXFfD2P+EbLWflhXVmRw== X-Received: by 2002:a9d:798a:: with SMTP id h10-v6mr153865otm.4.1538053810328; Thu, 27 Sep 2018 06:10:10 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:b89:: with SMTP id 9-v6ls1059103oth.3.gmail; Thu, 27 Sep 2018 06:10:10 -0700 (PDT) X-Received: by 2002:a9d:798a:: with SMTP id h10-v6mr153863otm.4.1538053809995; Thu, 27 Sep 2018 06:10:09 -0700 (PDT) Date: Thu, 27 Sep 2018 06:10:09 -0700 (PDT) From: Juan Ospina To: Homotopy Type Theory Message-Id: <91b60f0a-e5e3-4216-a422-9b52bb8a4cc7@googlegroups.com> Subject: [HoTT] Characteristic Classes for Types MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_211_1982423809.1538053809518" X-Original-Sender: jospina65@gmail.com 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: , ------=_Part_211_1982423809.1538053809518 Content-Type: multipart/alternative; boundary="----=_Part_212_1390521974.1538053809518" ------=_Part_212_1390521974.1538053809518 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Recently, there was a post about the Euler characteristic of a type and=20 other post about Hodge structure of a type. Then my questions are: 1) It is possible to construct characteristic classes (Wu,=20 Stiefel-Whitney, Chern, Pontryagin classes) for an arbitrary type in=20 HoTT? 2) It is possible to construct singular cohomology for a type and the=20 corresponding Steenrod operations? 3) It is possible to construct an Aityah-Singer index theorem for an=20 arbitrary type (a type fibered with other type). 4) It is possible to construct integrality theores for the characteristic= =20 numbers of an arbitrary fibered type? Many thanks. Juan Ospina Medell=C3=ADn, Colombia --=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. ------=_Part_212_1390521974.1538053809518 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Recently, there was a post about the Euler characteri= stic of a type and other post about Hodge structure of a type.=C2=A0 Then m= y questions are:

1) It is possible to construct ch= aracteristic classes=C2=A0 (Wu, Stiefel-Whitney, Chern, Pontryagin classes)= =C2=A0=C2=A0 for an arbitrary type in HoTT?

2) It= is possible to construct singular cohomology for a type and the correspond= ing Steenrod operations?

3) It is possible to cons= truct an Aityah-Singer index theorem for an arbitrary type (a type fibered = with other type).

4) It is possible to construct i= ntegrality theores for the characteristic numbers of an arbitrary fibered t= ype?


Many thanks.

Juan Ospina
Medell=C3=ADn,=C2=A0 Colombia
<= br>

--
You received this message because you are subscribed to the Google Groups &= quot;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 http= s://groups.google.com/d/optout.
------=_Part_212_1390521974.1538053809518-- ------=_Part_211_1982423809.1538053809518--