From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBB45SQPOQKGQE2QQLRVA@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-oi0-x23a.google.com (mail-oi0-x23a.google.com [IPv6:2607:f8b0:4003:c06::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 09d4e9fb for ; Tue, 18 Sep 2018 10:54:45 +0000 (UTC) Received: by mail-oi0-x23a.google.com with SMTP id l191-v6sf1256793oig.23 for ; Tue, 18 Sep 2018 03:54:44 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=2Jitxca94dzGdgbujY+EoVbcgrDaHlOecy/hRkI+RMw=; b=GPKb7vy81n/GMkswCYirIr3rgWM5TtkoMRu00QfUF0K0Aesuv0Zg3ITOQOvApWlMdf e5+IqsxW7H2zjaCfybgcslZawrVCz3Zu/qc7EvRre0FRrlpetFaGb/mBTK8QJ6ugN8Ju kwVnIOoWgP8Ve+7z1Ov15gAFmf0YSTwe7bp2mojsEHV6rQxug9x75R6Z6Jt7byaQ93nm elMOVXwBYZysLMzR/u1gYWj0X4WHUacQMWmd1OvyIUhVfXnevOaa+4dyqBvaEeoDPaDl ilhRTDt7OtTG8wIMDLIhNXzs5yDhN5DvNT6kARA7GFV3aq8bKd/O2YcdagTwprn6NXwh cw5Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=2Jitxca94dzGdgbujY+EoVbcgrDaHlOecy/hRkI+RMw=; b=bpYWvUlC64lhDbIrqmp7ABtzDH5R42X2q3O34a+lQNLW2aXkD/RkuPwxBNDgL7159e bHF08YWXfazkJ2ukmYoUg7bJIu/nN8pGIUCXNdNZEP30gnuivjpGgK4y46aQ7yraXpQQ 273xB5Luu0dW5xVfJ37i63tXkm4GxJTz4kxeLD8/7l50n7u2vHeNPCQtHh+pDWBMqVBB ljAYzBrmT3iTI506arDo23qjsJbo4+WaPTjY/rvfZZ0mN14jKkINT41CX9t3Z4VoM18b T70a353XIZpX6EFV470kDDgqixwICqjahOQ65iDNMTVcY8ncMZNeGP7RS4mVxyn1nkGH ZvMw== 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:in-reply-to :references: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=2Jitxca94dzGdgbujY+EoVbcgrDaHlOecy/hRkI+RMw=; b=rR5RpUAngQJnH1XSb53Xo0r92JtmeAFJC1ZmC2PiMMAt7CRgN1b//vBzzZ4l0KypXl QHRoLrPimQK581W9eVjnLhUMJhTT6/uiBkamhCMIlTgwARAi89TtHXK42uUHsIIghURy CduB7g5nmzq/jyNPRfZQsZkGy7bf6QG786UpMB6/PjOBwGgXEkJPxOaqWn8Jy7lXVNcM jBnmu+/sVymvGjqXEWkSBfSxDqpZ9k/0QLFrsrfd8WGTqTfiKsJwqVKmiWTnj4zBaOwU Rg04orrWllf/rs1+etoOQCJQUqRzIA6ml7frGXz+Gu9Yqi//kjJNn3dn+mmidc5Z/aIY 4/nw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51D19tNBC9cpsYa8ZEu6MrIM/FnURN5Dot2Rztq8WTob4qV/zkBi e0MM5bhoM9Sy9S+HFyGqej8= X-Google-Smtp-Source: ANB0VdYlDGin6Qanb8xoBA3FTHFh/1RGU5xP3y00n+IeqvDL4N7VPxblD+5kCxlNXTC8PpOqHDb4Ng== X-Received: by 2002:aca:5557:: with SMTP id j84-v6mr37724oib.3.1537268083765; Tue, 18 Sep 2018 03:54:43 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:1702:: with SMTP id j2-v6ls11403828oii.8.gmail; Tue, 18 Sep 2018 03:54:43 -0700 (PDT) X-Received: by 2002:aca:de07:: with SMTP id v7-v6mr37306oig.5.1537268083245; Tue, 18 Sep 2018 03:54:43 -0700 (PDT) Date: Tue, 18 Sep 2018 03:54:42 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: In-Reply-To: References: <02f4bad3-496e-443a-8607-9a6f37fa878e@googlegroups.com> <811a924d-8ffa-4fa0-b0e1-b5bd379c8917@googlegroups.com> Subject: Re: [HoTT] Euler characteristic of a type MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2074_403159124.1537268082600" X-Original-Sender: alizter@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_2074_403159124.1537268082600 Content-Type: multipart/alternative; boundary="----=_Part_2075_587869864.1537268082600" ------=_Part_2075_587869864.1537268082600 Content-Type: text/plain; charset="UTF-8" This is a nice idea. If we could somehow overcome the lack of coherance of smashes how would we go about defining the trace of an object in a symmetric monoidal category? On Tuesday, 18 September 2018 07:26:04 UTC+1, Michael Shulman wrote: > > 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. > -- 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. ------=_Part_2075_587869864.1537268082600 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
This is a nice idea. If we could somehow overcome the lack= of coherance of smashes how would we go about defining the trace of an obj= ect in a symmetric monoidal category?=C2=A0

On Tuesday, 18 September= 2018 07:26:04 UTC+1, Michael Shulman wrote:
A more "homotopical" way to define the Euler chara= cteristic is as the
trace of an identity map of a suspension spectrum in the symmetric
monoidal category of spectra. =C2=A0It 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. =C2=A0I 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.

--
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_2075_587869864.1537268082600-- ------=_Part_2074_403159124.1537268082600--