From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBB4HY77OAKGQEFQTWGVY@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-x23b.google.com (mail-oi0-x23b.google.com [IPv6:2607:f8b0:4003:c06::23b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ff3b8e16 for ; Mon, 17 Sep 2018 19:11:46 +0000 (UTC) Received: by mail-oi0-x23b.google.com with SMTP id u74-v6sf19163950oie.16 for ; Mon, 17 Sep 2018 12:11:45 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=dLO8uwYlm+uT/2Ayy72pq5cVkHpOhemRflQJxUaoBAQ=; b=E9pm5PNWXgDgZZff7MK8pbyshFarhIuM1PV8uwkIzRl9ge42BYK+3cQxqhgmhN08Vk 5vAxaOVtFackQWV9SUkgGmmXkHraJuirsn2ofzP/zna/05mdOsQNGBI0Z0sehFaOezCa LLYUxIAQa6RoTFpliZ2ZOLlzn1OMW9d9pq+xfa5XygNPdnDEvr5I+rhs04LdcM8qB9aT nH/lRvKdy1etXgkqm/NMsgvG7CcHHl79S2zwBkylPezTRtEprYytefSTPPlPM8S7Ee0R d3HyHdGaKVZB/G03bGSq6x1kdsnSEmHJkMgkij5MLgIJYwdwRmu4KCiG3zjNnrJCw1ry NR4A== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=dLO8uwYlm+uT/2Ayy72pq5cVkHpOhemRflQJxUaoBAQ=; b=jIb+kkdRPCMsXKPKMMJRe9/35gvkVNZ0VqvkoTh2g+lkudL405jgk04eU1w69czDkN JbnOtl3Pssyl4WXI98BebXVYXrgsEmhghWzjbkN1YqYcCH056Fm810sHvmzeHeAOR2KU ZBF8m7zrgt6T+G4DWzaZYcdNzFHX5+XdVqScrbl1PoyUVqTIELwCXcNMV4ThbIHUwGuQ N/wJLDooIe064dhDSjUNVTU0MmDUqhTLMl9dv1z6twOmIw3mub1aAdnr0hFJNX2kKurg t6DgXHYRyqaNy7qW3D/YRWPxFfObj/a6JnME05GWU/pYsetQ6kFl2GKUvMFFPT+Lyzp7 P9kg== 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: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=dLO8uwYlm+uT/2Ayy72pq5cVkHpOhemRflQJxUaoBAQ=; b=jRB10CaQ3Fnky54giqC4o9w7COVRyq8dutYn8FT3je5YIrwTkAoSEjfG//NTHhVk1N 8VYx4X69TZMk+lW5pDiOzkGqsZAC9L2hmOGsjeBlxqHcG5brMpIW7w+OrnQnwcyiasIw pWHOXNx8LdB+oMZjI1DOZRplH0bj7L8KVnghnSsfsJcDQM1jS4hUxVPQoNA65sbR0wYA R4JQwAxAJOaDssRFsZdvYx24t8JdS853ZZ91ym+XPaxV74N57ZUIg9S39u0hxegdULJe HYsu76lqu1Eby8mMjJ8EcDEt+J8/fZTB6BHmyYYhp+Q/o1lZ/WxYzTN3Ye2c6hOwa5LQ SMHA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APzg51CsvECByI+l7pre0eby5YggteV3JtHMNgZYT+PduhFyN9yy2TQb I/yQfpNqMbskrKx4uffHvvA= X-Google-Smtp-Source: ANB0VdbVh6pHHvnuyJ8Qm2nG5L7fqbPh5R5bZWhIJaa51CR+FAK+mFVI2Nj8PwaKDdGFZBNppRLu7w== X-Received: by 2002:a9d:4c8d:: with SMTP id m13-v6mr200265otf.6.1537211504850; Mon, 17 Sep 2018 12:11:44 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:1702:: with SMTP id j2-v6ls10260975oii.8.gmail; Mon, 17 Sep 2018 12:11:44 -0700 (PDT) X-Received: by 2002:aca:d417:: with SMTP id l23-v6mr194587oig.7.1537211504287; Mon, 17 Sep 2018 12:11:44 -0700 (PDT) Date: Mon, 17 Sep 2018 12:11:43 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: <02f4bad3-496e-443a-8607-9a6f37fa878e@googlegroups.com> Subject: [HoTT] Euler characteristic of a type MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1802_674735717.1537211503802" 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_1802_674735717.1537211503802 Content-Type: multipart/alternative; boundary="----=_Part_1803_304970995.1537211503802" ------=_Part_1803_304970995.1537211503802 Content-Type: text/plain; charset="UTF-8" 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. ------=_Part_1803_304970995.1537211503802 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
We currently have enough machinary to (kind of) define Bet= ti numbers (for homology see=C2=A0Floris van Doorn's thesis). I am confident tha= t 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 ident= ities.

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) =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 famil= y 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 it stands, homology is a bit unwieldy. Perhaps rationalising spaces wou= ld help?

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 http= s://groups.google.com/d/optout.
------=_Part_1803_304970995.1537211503802-- ------=_Part_1802_674735717.1537211503802--