From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORB7FUQLOQKGQEKYQHRFI@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-qk1-x73a.google.com (mail-qk1-x73a.google.com [IPv6:2607:f8b0:4864:20::73a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c1dd114a for ; Tue, 18 Sep 2018 06:26:06 +0000 (UTC) Received: by mail-qk1-x73a.google.com with SMTP id w126-v6sf595807qka.11 for ; Mon, 17 Sep 2018 23:26:05 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1537251964; cv=pass; d=google.com; s=arc-20160816; b=0iO/8Vn1i+MkzBqjOAECnQRwfLNbJ5YI5R6Ixthj6FTTM8qI1MNT6XXoli0+ctNuLg cmzAaL52CzssmJlitZKCI/1XyxZVTByjVPQLqwfqxjkQUP73UR9MJtP0WQyj+qQIjuzY Jydg3xKYgjTvnkfZLJV36hUQMLp1Poaqpt8HUOTTXUquKeWd2VPAz93Cf210AX3NqnBa KjQSN6A5FsCfGkO0qS5nip3Z909t7jRYQaty1/hPq84erU4g7VldVKAizjW6cSOE0K32 lsInllpDQIyRgXvIm3PbMRiVkcmDDsMbTqn0DVns0dLunFax6SPPnnjHB4FZ6JqFdxNO uA8g== 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=+AKu3MzqjYwnket5nnLal5NbTOeUQyxov6mwJU8VmRk=; b=xac2yA8z6NFE+08ng6dOcfqwevA1RTNTKyh7aiIf2ouqCfj5HhqTS4hshXI7kYHXnf hjr0pw2j2tKC5kVpcio0yNBQHFVRLWkl18/1qzRAPzOctr6pGNGInX58J3XtgVKDNrWw JsZcLhOdy0VhUhM259dEuoENWvkAW0cVn4cXCV4xJHU1gSMw5/ImcKqRdgFwOtvGJ7tH VKo3T79xyHcv6U+aHrQ7akVLOoO69iFV7LLTP0kU76NujADkX7e4fMmb0opVvx57mymB Q65yWMZXZfpiMUm+XgZen6SHbJEul2oYDcNKv/FfDY4Df1HOf5OgmZLOXB2X+do1w28X l+Rg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=IkvX6WOg; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2f 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=+AKu3MzqjYwnket5nnLal5NbTOeUQyxov6mwJU8VmRk=; b=SfuBn/Trjw/w5bHzELazJUYKWs7WCbLFES+s80rTAQMJUtEminoVGvyhozlOutNlqd Lx7U/MRzlFMDuqmkzJWBvV3MtnyS7QucRp6SaCO70kgq27i9Acw3ZDCtjtGEARLStgvm at6rRu/hN3Ahk/BvUWDJQZrmHIvS1AbPleGSMpfrzcQsZvMsRx75LV9cAUApZeMTaZH8 TCrrMQZseHsXnl5ZbgC7jIFHsmLXvP+Uc4bHEm4NyZBKULQDu8FGOkqnsUg38sPNZbgT Ruua1stTVvxnWr+c9Ygqf3rZ6lGhsIR6wp3/o8AIs+EFs096ITh/jqG/3oqM/nWCqQ3R PGBQ== 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=+AKu3MzqjYwnket5nnLal5NbTOeUQyxov6mwJU8VmRk=; b=ZcAOagD4KIO0QUoBg+lJJa2588CXdMf4ky3U8jkKU74liCCqL25pcbXkfQjR0KYgaf WK6nr8nu6EQPw7zpIz8QCvpxzpwEHLIFeSXlVR30Kls2JW73KhULL6fhpgRAJqKm2WWl dodmMyAq54yQ9Wf+l7ZErfjF8QTlVhygPkt5WaZDnMoLXvpSsID7GN90kKDtce9w9C3d BgC7NFKrfNRNy8Ik1mXF2hePe7zCnJW6rISNaqs7RdpzVXAo9c8++5aDlzMkoGaR1S6r m6FOFG2rWK5tvzdBmh0Dui2sAFOFMK3OculDv/VnIFKPmxMXnQ7pa6hHzfs1MNypNDZ2 cc/g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51CrC6fqqWBaCiXNg32fBSzJBhYckw96FMPxPkWZh0mjaXTsxOtz z7MW1088UxFy+Tb4YSDPnTE= X-Google-Smtp-Source: ANB0VdYPfu4x8xmgyDEa5opt6ocC4NSUvLZAYxtWIrzF7JSZ2ldt/Qhuzlwhq8DNoD7zxulNknZeEw== X-Received: by 2002:ac8:30d6:: with SMTP id w22-v6mr246440qta.3.1537251964563; Mon, 17 Sep 2018 23:26:04 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:b486:: with SMTP id c6-v6ls6447337qve.10.gmail; Mon, 17 Sep 2018 23:26:04 -0700 (PDT) X-Received: by 2002:a0c:d4ba:: with SMTP id u55-v6mr9495961qvh.5.1537251964318; Mon, 17 Sep 2018 23:26:04 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1537251964; cv=none; d=google.com; s=arc-20160816; b=CyjHC+sZiQcDykL6/Zfev2vQFp0gRRYmSyBkCn3CZcamjtFObjwYX9/RSjt5T8r+Qo zVQoOV2RfmkvA0UnK/rQLYUvF0eJ2ygVZPCEIAHaFku15MQQHkKlNKqFjE/+f+uszePT 19lwoLAPId1iNMebLcPYIVgSxe1h21hkxbZRTX9E8mDZs7BBLVkpM8lU2lO3HGYGQame TqwfaU5AnjeEG+UE1aLMsIbKKm9ku3xYyO92QN4GP1HDn7hVOFpjZFimwi8cZiAbLCmk +rGRIBCeXNZl440BT/3Sv4wHy5J34q8hkRy2F7jxOOz7TQe9SxNSyOBaIiEuzbudWe5X 7YhA== 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=OrZmsZj8pr+XR32TdCYRABDtG8j2V64JPbPqPTqG/pQ=; b=Pnj2ECLQeXEObMMpP3hIxivOPfRT/zOvdFXErbhAm1KjI3Nc7b5DpKK/awfBI8rUzu pW+aoyYsdhHWpjD7A0QKBG3ZATeE7niLgpptAfWxCCVM11CVxj8tuU4E8Z+LE9RcHTr+ 7Zsfg2WADot6ZPGzDqYZSXF1WODk+IrDWpFrrx63tZXUHw88/p/KdxNS6t1EtklMCxQ9 Pd2swdhghcbMu3uwuvwd0FO/L+H1A9LDwa+uGRS/6bYPE4LcjVM+6xdVMmc45W6OZM/r UpQ2uaznMkBHwYcPkrBvntEYXFYhRiMj2zFVsEiJtIGFlk+mn33PfpK5+SNTRCvgtLqM 2XtA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=IkvX6WOg; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2f as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc2f.google.com (mail-yw1-xc2f.google.com. [2607:f8b0:4864:20::c2f]) by gmr-mx.google.com with ESMTPS id l15-v6si859047qta.0.2018.09.17.23.26.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 17 Sep 2018 23:26:04 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2f as permitted sender) client-ip=2607:f8b0:4864:20::c2f; Received: by mail-yw1-xc2f.google.com with SMTP id q129-v6so331314ywg.8 for ; Mon, 17 Sep 2018 23:26:04 -0700 (PDT) X-Received: by 2002:a81:9851:: with SMTP id p78-v6mr11420429ywg.175.1537251963939; Mon, 17 Sep 2018 23:26:03 -0700 (PDT) Received: from mail-yw1-f44.google.com (mail-yw1-f44.google.com. [209.85.161.44]) by smtp.gmail.com with ESMTPSA id q127-v6sm706073ywq.83.2018.09.17.23.26.03 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 17 Sep 2018 23:26:03 -0700 (PDT) Received: by mail-yw1-f44.google.com with SMTP id z143-v6so335258ywa.7 for ; Mon, 17 Sep 2018 23:26:03 -0700 (PDT) X-Received: by 2002:a0d:e341:: with SMTP id m62-v6mr11331799ywe.421.1537251962886; Mon, 17 Sep 2018 23:26:02 -0700 (PDT) MIME-Version: 1.0 References: <02f4bad3-496e-443a-8607-9a6f37fa878e@googlegroups.com> <811a924d-8ffa-4fa0-b0e1-b5bd379c8917@googlegroups.com> In-Reply-To: <811a924d-8ffa-4fa0-b0e1-b5bd379c8917@googlegroups.com> From: Michael Shulman Date: Mon, 17 Sep 2018 23:25:51 -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" 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=IkvX6WOg; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2f 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: , A more "homotopical" way to define the Euler characteristic is as the trace of an identity map of a suspension spectrum in the symmetric monoidal category of spectra. It also generalizes to a definition of the Lefschetz number, and many of the formal properties of Euler characteristic follow formally from this definition and the properties of trace. I suspect this would also be a useful version of the definition in HoTT, although of course there are currently technical obstacles to working with such things as the symmetric monoidal smash product of spectra. On Mon, Sep 17, 2018 at 4:07 PM Ali Caglayan wrote: > > This would be some subuniverse of "compact" spaces I assume. > > On Monday, 17 September 2018 23:37:03 UTC+1, Floris van Doorn wrote: >> >> Clearly we cannot define E on the whole universe, but only on a subunive= rse. >> For example, we could define it on the subuniverse of types with finitel= y generated homology groups. For the Euler characteristic we will also need= that the betti numbers are eventually 0. Other than that, I agree that the= se properties should hold in HoTT. > > -- > 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.