From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBD6672PURMHRBD6ZQDOQKGQEEUEOWEA@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-pf1-x438.google.com (mail-pf1-x438.google.com [IPv6:2607:f8b0:4864:20::438]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 752dfe1d for ; Mon, 17 Sep 2018 22:37:04 +0000 (UTC) Received: by mail-pf1-x438.google.com with SMTP id w19-v6sf9090175pfa.14 for ; Mon, 17 Sep 2018 15:37:04 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1537223823; cv=pass; d=google.com; s=arc-20160816; b=MMi8DYe0YDCdT+BhQo3WQOqmRUSuoUQF6tM3isJfCXw2YgwkVaBVqAJL0s5CAFU62+ 4WZGcXSQsuwkJaXBdOjP6pWpaP7iE+cW9T8uWdx8CbT/TAzCYH3WZjo+FD3YsqyPlumS 46TFM3TLKUdAWKNXRTMqG508IamzwnMvBNMuKFT/koe2OIl3EjAnB4GFetShWk5voQnI Pgmv091iDHAx2UcUfsqIzKGmfBuXiJKxo0bLkwVVHPnDdv9iE9RlYcooEQUaz8FnoY+M DXfPQxRIxfDvSmwony7o1XPoKfVX+2VhyEQlo8TJ/bjW5oer5cneQ81DIfoXHUsoz3ST K+WA== 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 :dkim-signature; bh=PzodWaGaNJxb5lnavZH++kAGtJk5Xe/+fLdWJIv6xWg=; b=FcHROcBJMu8GM7NhZF/J7KT4JmU63BBeqhMW8lV5gl5z705xlXzziRr8ggCtFgTjeb ydkfBk+FoaZxATgqgkYT7MW5RIOULAsD7MpsYHNHmQk6T92YFMWZ/EzzwAkZ7dXcrMk7 vPpmyL0kxCKW6VF7lNcpby9dIMbQjnLdWaOtN64hGE1VVm41gcMh1Gl67tIL46F5ej2p 5yellby5oCPVEaRGJqhHdHOJvXbeHM3/MTkmFrp9JDheFB8UeeSSQEnWwYjm1yziQrvu ls79hkYfKTji+HLMyHdZG1+LMStxWRgWPWSi8BTFVSqDi4V2/1yIfBpWnteaOz9Xsmxu 1ufA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=u1+b7eB2; spf=pass (google.com: domain of fpvdoorn@gmail.com designates 2607:f8b0:4001:c0b::229 as permitted sender) smtp.mailfrom=fpvdoorn@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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=PzodWaGaNJxb5lnavZH++kAGtJk5Xe/+fLdWJIv6xWg=; b=s44J5XrI6o0M9SfW8vnXm5+xQbz9sK4v3BHAg9MeCC1v8but6dFN+/fhefcG6Dz5Aq 6EtcP7DwoByVZKi4jcV1+QhplyqbHkRc1xYHteTfVOmeqkqAGIoD/4XUttoXh9vDFtVF xPGUfX5zC4xrRM9xOjybRZDYjh6PhZXDaA1KB2AT58oFK3tUfqpQZORB0Fq3G+TUMV5y UWY8ngZ0LwBFgQ653IXJZwT3rg29CpYq748ZFn+02OBk7M8XPNtb6atrvyH6HAxIn/NE ZgkqfJJZ/3A1MRz/orgp5cD0t7ikijwakxOEVOVqx+PaW5Q9L9RNgwhNzuZc3VeafGmc b3sg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=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=PzodWaGaNJxb5lnavZH++kAGtJk5Xe/+fLdWJIv6xWg=; b=tMlrfAIgf8/LGgM5GrgWsVW4IvMTKblxt1SPuJK5xFn0RqAzkjnXKLPoZVJacI4vSq fpPrikJRHKPNcT8gHIHXB/3yeGeuHgJAcsG8YNRKw5J7BXKeL+UOwmw66+gTPouK6UUk ORsapjSh78hkU0aRokfGdqU1W9qS2fgUbM8HTMQpdkyJxx9T61zl8jv8EZmhvk8P851B qMlHfZ1VDEQ8q6899HjmQNEgj5iVjkCVUodxl8bsY2tQcguMJwKyusfSL0azcj8ffqX+ dY25cAZ/Rl1dbKi2LeSmNPl/r3nRPFS2euW27GddYe013/EtOwod5AbfkzRWO0M1ml4N lk9w== 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=PzodWaGaNJxb5lnavZH++kAGtJk5Xe/+fLdWJIv6xWg=; b=stAHA+HoZsNcX5Z6GQkEbyGF/iCZMYxPW/tUM3O91NJUfaOHEIeb5FdvFfxLcZooGT 1H/Pw7XRGuLfyplv1/8fcRwRR1J0CTZlGnVLmZftjIcu3F0ZeQj5Y5jZwgHubF9TudgN +F7qNzrz0aWRzZX0sXaQFMJdBaAI6vu2fFktLEdaji01cM8cvUWRMENQUM6hlrVZoUnM y92Q2bXaS7M+xYqkau/4DRGejKduT0LOx4ZgZ9uiyBpIpGxn5722QfmPsrJWmyYUDUf4 xjh1NBpbIzl7+uX9BR01K+TRMuGAxqXv34BEHbXjbbGFMYfqXvwyDXdQE/T+YY7YHW00 npEA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51C4BtF21726b005Un2xhnO2zkwQfoUDlkHI4GUGdryrqxE9Hxe0 bqQyeP79yOxS8EKqhUbVPz4= X-Google-Smtp-Source: ANB0VdaevL/QxGrJgabkwmOQoPfZNoKdt9RHhbfQs5yno7syvkRvu3YPZqpdiq+wwTo/vaC3lC6AUA== X-Received: by 2002:a17:902:a718:: with SMTP id w24-v6mr99980plq.2.1537223823113; Mon, 17 Sep 2018 15:37:03 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:88c6:: with SMTP id l189-v6ls3652344pgd.30.gmail; Mon, 17 Sep 2018 15:37:02 -0700 (PDT) X-Received: by 2002:a63:6949:: with SMTP id e70-v6mr1258156pgc.175.1537223822791; Mon, 17 Sep 2018 15:37:02 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1537223822; cv=none; d=google.com; s=arc-20160816; b=ocSXocRONYxwuD5um/xLk3LLa5DECy37MpW2EMFFug/1Sf452RfPhAEEZgj+97lfcO yhZKchBfnwbrcNlhn1oByZfIkjUpH36Qei4hZQOFqh3u8XiX3QcVeh4d/Fvg76xbCel4 wN2QW2CwuUyIBfo/skPFW8V6sPRyrDldaJM9azU74CunSLZ9UibvtyR46K+Gh0NjSjoh XhRGyIM4V1xoE1PwkLtNZAoBu4px1BTeEGbvRJpFBxgrXwLh8HGP3nlVkjjjLNcoKeRh vIDy/UrVwOBra0UMQ6DwI45ToOoOv0Anhatakl6QNmHua5qAKCvAXKltAJrjTCk3pVw1 ybVQ== 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=nSYdNmtDsB0XuhKwh5BeHBqUHvUZ15jDihXYF07yIV8=; b=LZphzgQc0ENHk557AvIsh8RI8t7N5UfpcysTdF39AYbouNOCp0HtPyEGVS0prHqiyf y4PzU/mhv1JanyLEubGxhJbbi/+0EvOoIfuk2BO8NZ8MzMi/F7xqWLWW24i3hJOJgUUu UOUSmuaZ3xxnhXgFHLs1a8q3CckUJpqeT2Ka6wQ2lcunAtgCBPKIetKd+1cNaJx2MX/7 cX4PBk3kE7G/t2TbNJQqw9LF5tV2P6czf1E2iZbXo1cfeVAst72gMCGdYSykHLo6SatL gyklKJirRsA8J8pkVyQwh4OMavV/zI1X7QhzFafttJqHiLZWNu29tV+DVGWOMcIPSEpu XTxg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=u1+b7eB2; spf=pass (google.com: domain of fpvdoorn@gmail.com designates 2607:f8b0:4001:c0b::229 as permitted sender) smtp.mailfrom=fpvdoorn@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it0-x229.google.com (mail-it0-x229.google.com. [2607:f8b0:4001:c0b::229]) by gmr-mx.google.com with ESMTPS id f4-v6si831219pgs.1.2018.09.17.15.37.02 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 17 Sep 2018 15:37:02 -0700 (PDT) Received-SPF: pass (google.com: domain of fpvdoorn@gmail.com designates 2607:f8b0:4001:c0b::229 as permitted sender) client-ip=2607:f8b0:4001:c0b::229; Received: by mail-it0-x229.google.com with SMTP id h20-v6so536428itf.2 for ; Mon, 17 Sep 2018 15:37:02 -0700 (PDT) X-Received: by 2002:a02:cd0:: with SMTP id 77-v6mr24496378jan.67.1537223822293; Mon, 17 Sep 2018 15:37:02 -0700 (PDT) MIME-Version: 1.0 References: <02f4bad3-496e-443a-8607-9a6f37fa878e@googlegroups.com> In-Reply-To: <02f4bad3-496e-443a-8607-9a6f37fa878e@googlegroups.com> From: Floris van Doorn Date: Tue, 18 Sep 2018 00:36:50 +0200 Message-ID: Subject: Re: [HoTT] Euler characteristic of a type To: Ali Caglayan Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000de3e59057618cf51" X-Original-Sender: fpvdoorn@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=u1+b7eB2; spf=pass (google.com: domain of fpvdoorn@gmail.com designates 2607:f8b0:4001:c0b::229 as permitted sender) smtp.mailfrom=fpvdoorn@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --000000000000de3e59057618cf51 Content-Type: text/plain; charset="UTF-8" Clearly we cannot define E on the whole universe, but only on a subuniverse. For example, we could define it on the subuniverse of types with finitely generated homology groups. For the Euler characteristic we will also need that the betti numbers are eventually 0. Other than that, I agree that these properties should hold in HoTT. On Mon, 17 Sep 2018 at 21:11, Ali Caglayan wrote: > We currently have enough machinary to (kind of) define Betti numbers (for > homology see Floris van Doorn's thesis > ). I am confident that > soon we can start compting Betti numbers of some types. This would allow us > to define the euler characterstic E : U --> N of a type. If classical > algebraic topology tells us anything this will satisfy a lot of neat > identities. > > In fact consider U as a semiring with + and * as the operations. E is a > semiring homomorphism to N (the initial semiring (is this relavent?)). In > other words we should have > > E(X + Y) = E(X) + E(Y) > E(X * Y) = E(X) E(Y) > > and even maybe, subject to some conditions, a given type family P : X --> > U would satisfy E( (x : X) * P(x) ) = E(X) * E(P(x_0)) > > This would be a cool invariant to have. Unfortunately as it stands, > homology is a bit unwieldy. Perhaps rationalising spaces would help? > > Any thoughts or suggestions? > > -- > 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. --000000000000de3e59057618cf51 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Clearly we cannot define E on the whole universe, but only= on a subuniverse.=C2=A0
For example, we could define it on the subuniv= erse of types with finitely generated homology groups. For the Euler charac= teristic we will also need that the betti numbers are eventually 0. Other t= han that, I agree that these properties should hold in HoTT.
On Mon, 17 Sep 2018 at 21:11, = Ali Caglayan <alizter@gmail.com= > wrote:
We cur= rently have enough machinary to (kind of) define Betti numbers (for homolog= y see=C2=A0Floris van Doorn's thesis). I am confident that soo= n we can start compting Betti numbers of some types. This would allow us to= define the euler characterstic E : U --> N of a type. If classical alge= braic topology tells us anything this will satisfy a lot of neat identities= .

In fact consider U as a semiring with + and * as the o= perations. E is a semiring homomorphism to N (the initial semiring (is this= relavent?)). In other words we should have

E(X + = Y) =3D E(X) + E(Y)
E(X * Y) =3D E(X)=C2=A0 E(Y)

and even maybe, subject to some conditions, a given type family P := X --> U would satisfy E( (x : X) * P(x) ) =3D E(X) * E(P(x_0))

This would be a cool invariant to have. Unfortunately as i= t stands, homology is a bit unwieldy. Perhaps rationalising spaces would he= lp?

Any thoughts or suggestions?

--
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 https://groups.google.com/d/optout.

--
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.
--000000000000de3e59057618cf51--