From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORBFMQQ7OQKGQE3445HQY@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,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-yw1-xc3d.google.com (mail-yw1-xc3d.google.com [IPv6:2607:f8b0:4864:20::c3d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ab054217 for ; Wed, 19 Sep 2018 03:52:55 +0000 (UTC) Received: by mail-yw1-xc3d.google.com with SMTP id d23-v6sf1958160ywb.2 for ; Tue, 18 Sep 2018 20:52:55 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1537329174; cv=pass; d=google.com; s=arc-20160816; b=NyhcH6e1yFptqCLK8tLicua1TLCcSlDVJ2PgAU2ZxFBjvKrdK6+7BINA2NDVfTCguP TRcw7aln19c8lL5haCdKfkxZCA6bltH7PArd9G7JENAR0WKAlVdn2Xj8kLbE0OHIXmGc F2lwHq9j3aJ9Fymx8Sa/IoAcek8JCACVBYp4eJb7maU/Dhhl/1+wVI2p5o9zHCLXKBPY K/DgCI1LM4eJoUFvxQsxeGudvTPdgwuxxEcdZ0YvuFDwD0/VJxPy8ovXoembGHhhX8Yk 8YfZkIn2akpUZL/AsIPaLYtmfR88iovQG1k/Nzel0c1G9Rw85GhUJZKKj8ImMI3leVDY F0NQ== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=s8gHeel6Xlg+cgJOSjapONWvzeap0Sz2kVfT6cR8234=; b=0YY1USJZQCSNCMz4OYhsatEN4s6flUKrH5Zp/AfTfmJwEeXsiUW2U7E5nV2kIwaGFr U/+t1GBOt1ysHuucJXAvC4lprseijbVTZ9TukhBQ7Ss1CBGtEp69rKMk2OQCwXRe4owf MyRoljVD5MiCA/uZ/ox64BrpeDLju7BmUqSOFzt4ZtjimzGhOtFhzlstum0WhNE4fi2q 66qkKK5a9gq9en0+xGOQNUvBLx0SAFu5maRSXI7p7AqqjNQtp9kIB46wg987oNlXhmJV Q9aQPl3boazFiOTJOcmgd+QurYS8Z9R9/eWJZ7b4giyjqU27jsuidSvfYRq/EsOb/CeT sdMg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Yg+UaEfU; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b33 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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=s8gHeel6Xlg+cgJOSjapONWvzeap0Sz2kVfT6cR8234=; b=XUBscUdWjF1Mv09lxIOTJXVp+Rt+n9qR61KzpHqxqo5mCJG8aUcXTgret+tkNmHOag pwXqe10WPQry1vhx9Cycxxej4zaWL1vgDFPRLC0Min3qo91u8spU8C3q7KNVrzH5o11v Hg0el0iu4qoVqeh+zD+9IIkRRRsz9iPe8cRhky3yNszxvRkF3dc9vb9XsPzbFVvGbFhg 4niKu3ocejTdN2N15Ap/8hYA8B73tfttp2WqVllNU9PxTDnDydA19WbeGMACGp6+etvE w2+Vf4r1RsnYEyeO1+YxeEJcx3lCyhfy7BDftOCUa1wgFni8obrywMmu1Eo0g3wiUD1M lNTQ== 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: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=s8gHeel6Xlg+cgJOSjapONWvzeap0Sz2kVfT6cR8234=; b=MGDNYh/CQ0pJ71qRpO2MTCIqFeNngjxT7+dNv6B5vVfKFpfVB969zWbksh7qytyY4N rtg5zPbv2KyXwRdFvNQZs2/NHtZwLe89h+pjhIl8DWg+32XOcVLtv0BB3q2PN1stwmI8 RWqjbC7Z7QVzN1+rkHSqbblBBlqKa2HyKlhYHu2YhjeZvKChgn4k/Nnw0fga7L+9rOnZ yhyKEyxokxVbce+Txctfc49Wr2+0Zl5a6JTpi/4RDeqRA9blEOfsjw56gz21h1b7cFW3 +U9r6QtYR4O6kdhijEPwzNy3p6VQWkDHbqmsb2qwMaGOjeVv2AB/rzvxXKFz3fIpRC4s 4H8g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51DrBuKSh57I0rDgWCd8uWfD3kLaDS5U69TZWqhEoPjUsBfdC7nC kI1GoppiSC9TwcnfBCvZkqg= X-Google-Smtp-Source: ANB0VdYVT/BVTGuhCzUqeH/UBXiAucWp2rB09CNLTuPGtGJI0/Z4kK4AC8VkI34+aOJTn1O2KiRj9A== X-Received: by 2002:a25:1c83:: with SMTP id c125-v6mr186064ybc.6.1537329173918; Tue, 18 Sep 2018 20:52:53 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:11d3:: with SMTP id 202-v6ls3069294ywr.9.gmail; Tue, 18 Sep 2018 20:52:53 -0700 (PDT) X-Received: by 2002:a81:a402:: with SMTP id b2-v6mr5194827ywh.100.1537329173627; Tue, 18 Sep 2018 20:52:53 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1537329173; cv=none; d=google.com; s=arc-20160816; b=TIoIM6Gg8qixKAhC5Its+Hj3Nm+OO/DebhczhOXDXyuBCQJxr5+lsoklSfjpNcDpY4 WDZkgOxuhh9FPeuzK05tfem+xPjSnStXtoAdxNQ2bbIjBvXekcH/bnB6DEgruh5SmkCB ex2y0DfDt4DxLoRuh5ml2MfmSQLBG3Pt70B+NgOlyRoppN7Y2Q1vq/9w5lOxnjyKBgo+ +JpQfhmtwTLkfHF4J3WjvVFweuuhWem9/d+RGoPuw6L0ZJ+LJSMJcri3O1XRabipSMcM 2/GkiNZxVXzxChxXERUB1T2agnYp2nyj+6Hxqa6ZYF2mowSnAkat8+RdT48lWMOymjvh KeOw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=Tg9eXpWstDjL5r50/rLzApF5lluLT4pmK7MMmuKhJkg=; b=c0i2zjJRVUvqzBLAsD+8k33KVaexH9SIaB45p5fapWy/vCyWXf2gsn9ICyL05PVZ6t USAiOGExqVn6u36Uvwm9ZjTgplrAnJILd+RLHSROPGcCM+/vCi9vrM2MaFvrhMUo8/aC RWvkq4J2i6SFGsmqNTeoT82SdMAr6WntNTjPljWF8AtgFwbl0v7WPbIKpOSOexCqZAu3 PpzslLBq7WnXB+opBL8I3y+kFsHsu5sBjSmjTztQOJdKG+YIxuJsNfq25bBKNjb073mu VloYMUCekvgeHGjBbifMtsjpOCbjqzyN3CBoXkc5YijEjgKVnvFNCWg7uNtAz+dlkjqT GRcA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Yg+UaEfU; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b33 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb33.google.com (mail-yb1-xb33.google.com. [2607:f8b0:4864:20::b33]) by gmr-mx.google.com with ESMTPS id h5-v6si895297ybj.3.2018.09.18.20.52.53 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 18 Sep 2018 20:52:53 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b33 as permitted sender) client-ip=2607:f8b0:4864:20::b33; Received: by mail-yb1-xb33.google.com with SMTP id 184-v6so1831140ybg.1 for ; Tue, 18 Sep 2018 20:52:53 -0700 (PDT) X-Received: by 2002:a25:b7d0:: with SMTP id u16-v6mr14537012ybj.52.1537329173134; Tue, 18 Sep 2018 20:52:53 -0700 (PDT) Received: from mail-yw1-f43.google.com (mail-yw1-f43.google.com. [209.85.161.43]) by smtp.gmail.com with ESMTPSA id v126-v6sm2334733ywe.45.2018.09.18.20.52.52 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 18 Sep 2018 20:52:52 -0700 (PDT) Received: by mail-yw1-f43.google.com with SMTP id x83-v6so1744161ywd.4 for ; Tue, 18 Sep 2018 20:52:52 -0700 (PDT) X-Received: by 2002:a81:4bc7:: with SMTP id y190-v6mr13891697ywa.190.1537329172239; Tue, 18 Sep 2018 20:52:52 -0700 (PDT) MIME-Version: 1.0 References: <02f4bad3-496e-443a-8607-9a6f37fa878e@googlegroups.com> <811a924d-8ffa-4fa0-b0e1-b5bd379c8917@googlegroups.com> <1ce7df52-a67e-4d52-9acd-962a869562d4@googlegroups.com> In-Reply-To: <1ce7df52-a67e-4d52-9acd-962a869562d4@googlegroups.com> From: Michael Shulman Date: Tue, 18 Sep 2018 20:52:39 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Euler characteristic of a type To: Ali Caglayan Cc: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" 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=Yg+UaEfU; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b33 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: , >From an abstract homotopical point of view, the "finite types", i.e. those that have Euler characteristics, are *by definition* those whose suspension spectrum is dualizable. The dual object is then just part of the definition of "dualizable". Formal arguments applicable to any symmetric monoidal stable homotopy theory (e.g. (oo,1)-category or derivator, but which would have to be formalized differently in HoTT) should imply that such dualizable objects are closed under finite colimits, hence include all "finite cell complexes" represented as HITs. The dual in such a case is constructed formally as a corresponding limit of duals (since dualization is a contravariant equivalence on the dualizable objects). The business of stable normal bundles and Thom spectra is how one shows that the oo-groupoid presented by a manifold has this formal dualizability property. Book HoTT has no known way to go from a point-set-topological object, like a manifold, to a type (i.e. synthetic oo-groupoid) that it presents. It may be possible in a two-level type theory to construct the "fundamental oo-groupoid" of a point-set-level space internally as a semisimplicial type and then take its "realization" to get a single type. Alternatively, Cohesive HoTT provides an abstract context in which to talk about point-set-level spaces "synthetically" in parallel to homotopy-level spaces, where this presentation operation is represented by the "shape" modality. In either of these contexts, one could attempt to prove, using some analogue of Thom spectra of normal bundles, that the "shape" of a manifold is a dualizable type. It may also be possible to study in Book HoTT something with the "homotopical content" of a vector bundle, e.g. a corresponding cohomology class regarded as a map into some classifying space, as in the work of Rijke and Buchholtz on projective spaces. I don't know whether this would be helpful for dualizability, however. On Tue, Sep 18, 2018 at 5:04 PM Ali Caglayan wrote: > > So I have been reading your exposition and it seems to me the following things will need to be done in order to define the euler characteristic: > > 1. Sort out the symmetric monoidal structure on the category of Spectra. > - The main obstacle is the cohereance of the smash product (for spectra this follows from spaces I believe?). > 2. Define the suspension spectrum of a space > - This should be simple to define as a prespectrum which can be spectrified. > 3. Define the "stable normal bundle" of a space > - Isn't this something usually done on a manifold? > 4. Define the Thom spectrum of a vector bundle > - I have no idea what this is but I hope it can be defined. I have no idea what a vector bundle in HoTT is however. > > > > On Tuesday, 18 September 2018 17:13:26 UTC+1, Michael Shulman wrote: >> >> Some introductions are: >> https://ncatlab.org/nlab/show/trace >> https://arxiv.org/abs/1107.6032 > > -- > 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.