From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBBF7HQDOQKGQEG3FJNZI@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-x33c.google.com (mail-ot1-x33c.google.com [IPv6:2607:f8b0:4864:20::33c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b84441f6 for ; Mon, 17 Sep 2018 23:07:04 +0000 (UTC) Received: by mail-ot1-x33c.google.com with SMTP id k18-v6sf15834otl.16 for ; Mon, 17 Sep 2018 16:07:04 -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=pcmgNSU1iJ3Q0gPFPy/6AIRttnjtHaHXOnvrhK9hqrA=; b=SxAkRqWpEFXozn+hltI4w9oQaEzF97POsqBtOEpTrlyTpAA91Fp1TaIwTPpQEZlAOY Bd6Z71GaES8aXujq0+F9J1UXZ1EJO/FFfe0wsTFSnQ4g+vz3Lt5rsx9oaT9N9QiqeANl dQgqHFd5Vfz9XaPbno2yT0IsCjj0t02c7Wx5TAn56AhJY+FbFvkBUhTMDB8qEw9spO/Z OGt4zvSgyBUQ3/NxKzyI5x2NO0uJVcBVnpADb5sW3JKL3zuOVb8tC17qfa4VMrbPlAxi mFqCAPk/kWxBCJSeEu0RVeXQr777m/TunJCepnDQGcDjV600EdRmjA3BSzOQJzYFB2vG Qpxg== 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=pcmgNSU1iJ3Q0gPFPy/6AIRttnjtHaHXOnvrhK9hqrA=; b=c16nlws4CjzsgkmYJ9z/AIlPyHtxfooQKKXcy0+M2gBUxQe9xySndPK8TPgu/heBu8 l9ZW6WiZY4VHOeoExtefna/tAupWKWYk0ksriRBtMRGnbLpdKiE32tjARKyan9uqxKIm 98gyg8LKkX8zWSpAwucDjtZshmkK461HL30AJF/hGDdgtWTYjndG7ley4tRUXUBIg7C8 yKwbPxubPt3bDAeHjCPEyEg6oJGJ9+Qp1VdxqPT2gFKk/3k8eXko/oJUe5A8TNXfRII3 7YSaZQh6mkHL1/gPiPQnOvDe7uY13ulAfPCnwZqwFvSttsOxIbUEMTVzFuhCpvHzGzM0 5YjQ== 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=pcmgNSU1iJ3Q0gPFPy/6AIRttnjtHaHXOnvrhK9hqrA=; b=btAJ2ICoNIRWF9gopf9E9v77t7FO3gXArOw5J5sJ706nBqiT7ihZYVywQ99XJ50Tkw uEcwKeQzLlv38WwftW+TElIzFHRjI9XkxT7fZOgMEdGIxuzt4B4f2ZkEa7hCv/GZHCJZ fCz5Q9TFzCbi5XvscHV86Eq2XYAcSchUYIyhnLhUPi50Ij2qc72Zj4VAcSkL1gRIYvym dbbSr7WzpA9xKz6N8u3B49RrZZtHQEioyoLlQsduP03vNub3Dv4WuX+oNX7/sgTzY+zq pTYCOqJ588Ap9hmY6Wx7toQOuFv+EmMlFePLlBoeEsE4xxvLrnoJGPxdFyvTfGvhG2Ne m0iQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51CX+kJoJOEp2LUqlnYIFljTubM4w4/Th3cN7NtLy8hBXevL64tl CbrJxUWIovZXKp51Nibdx5g= X-Google-Smtp-Source: ANB0VdZ776FkUg8njh2TlTG4cFgHJHyLdzSNEiQiFwljM8TrjQSqeOi+MRfbtep8w1nO9zmM+t+oww== X-Received: by 2002:aca:de07:: with SMTP id v7-v6mr205139oig.5.1537225623532; Mon, 17 Sep 2018 16:07:03 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:1219:: with SMTP id 25-v6ls10736506ois.12.gmail; Mon, 17 Sep 2018 16:07:03 -0700 (PDT) X-Received: by 2002:aca:d551:: with SMTP id m78-v6mr210402oig.1.1537225623081; Mon, 17 Sep 2018 16:07:03 -0700 (PDT) Date: Mon, 17 Sep 2018 16:07:02 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: <811a924d-8ffa-4fa0-b0e1-b5bd379c8917@googlegroups.com> In-Reply-To: References: <02f4bad3-496e-443a-8607-9a6f37fa878e@googlegroups.com> Subject: Re: [HoTT] Euler characteristic of a type MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1894_1155139891.1537225622425" 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_1894_1155139891.1537225622425 Content-Type: multipart/alternative; boundary="----=_Part_1895_1926572713.1537225622426" ------=_Part_1895_1926572713.1537225622426 Content-Type: text/plain; charset="UTF-8" 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 > 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. > -- 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_1895_1926572713.1537225622426 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
This would be some subuniverse of "compact" spac= es 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 subunivers= e.=C2=A0
For example, we could define it on the subuniverse of types wi= th finitely generated homology groups. For the Euler characteristic we will= also need that the betti numbers are eventually 0. Other than that, I agre= e that these properties should hold in HoTT.

--
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_1895_1926572713.1537225622426-- ------=_Part_1894_1155139891.1537225622425--