From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBBGOLUXOQKGQECGVTNII@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-x33a.google.com (mail-ot1-x33a.google.com [IPv6:2607:f8b0:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2e5455e4 for ; Mon, 24 Sep 2018 22:30:50 +0000 (UTC) Received: by mail-ot1-x33a.google.com with SMTP id q3-v6sf22452352otl.14 for ; Mon, 24 Sep 2018 15:30:50 -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=nIT3PKVohj7sTC+phR3RIpcyX7GK6GhqV0lm3Os/YIw=; b=px3nHoRzAUvvcNOjzhBJPZmVE79CI60jg5qBfP7LsGnw/Q/bAkJpBkP8E1YreFGNEC DvP0KtozaJdp/4E7YdEa7fLLc9JmsDHApdK56tySgP6DatpT5fZnrcfopoiWmYfHmCB1 hY9ZVEWfJL76j+lBKtJlK9BRdFddmB6D3cB6Ur9OEvGJqugZVwy4ig9dfbhL4k47eZFO lW3vhHE/FfbkfjIwSg76gr/V44YcgDIhkaYn6hadK1svQlNkCAFkXLauSb+3jMj5MeCx kN5wwnqXQcRb9sg2TkKwVVZkpx/csRBvdj6nJDAvLjCsq4k5vFYAypZKHHEiGr+T916C h/qg== 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=nIT3PKVohj7sTC+phR3RIpcyX7GK6GhqV0lm3Os/YIw=; b=eqc5yFeo4LyTA1EkrLny5jfx6/Co0FkoXNs84N//ZNMZ/UgWDCWduLfk0fgLC4AB3J C1AeDf/ql07UBsAQ2ZEGf7gCl1RiNAPmOhFac4V6pSvPBQcaOp8TCqqcnYrcH8edXXpH J+0KcXGvRRaVToKtwo5Ne5geiQKvXgpesYDCA6+2tqq5AWtCxyfg2nkoPsuDZixdNaeu wKHk64RDPQoF0ZnHQ+39PNjDTTmevQTAZZYHb+Gs7CB0oN2CdJbL9Z10XOi6dDC7x1pM Tm+ildsmYmI68Iq/bexKAmN0MUFJ/FXew6iGm8XdzFU2aLJNkVTS9mI9JV/AkgI6ho7M yAug== 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=nIT3PKVohj7sTC+phR3RIpcyX7GK6GhqV0lm3Os/YIw=; b=ruzrLzPryDo65Mz/wEnCUFAgrMwP5rFuva55zEDVfEV2ffOf06iJNU2ygGQv5188Fm hDYn2SofJ3k6jP1q/IQ4CBmjJBONpG8e+dRjQMXVAyEblXF6za5l5pYCbOTYpArWg685 C+I/dqRJEpH3Q66PG5lTxoyWfv0tOu1c3iZzfZ60sPSLFDAj0TJ4K2w+qPZ9FgVfPeiD 61EOmdRlVqLQZVNgwQEgjj633SxrAIeeXIorBKJ89M6liAUhW0inx0s5cms827mn8/yh iVWeH9s4W5+TatCF52HcqjA1gIyFuBhFJVH7fbcZpmEOZCQZ4Pxhh8qA/FLnBvcS/sOg r47A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfojxQhukia5QZbf+XujEoZuC0zZG5yEyiwI4EPeEU/uas25Nt9CK IEkFsssbQZ1n1sILNk0vtC0= X-Google-Smtp-Source: ACcGV63Y3ATaCCqv4CbbVbmv590+EeveLqpIn3WdNNX+mH/jwTvCnMLZvP1G9IBTjdTRzvc/oLKIHw== X-Received: by 2002:a9d:6515:: with SMTP id i21-v6mr6190otl.0.1537828249412; Mon, 24 Sep 2018 15:30:49 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:4d82:: with SMTP id u2-v6ls1130378otk.12.gmail; Mon, 24 Sep 2018 15:30:49 -0700 (PDT) X-Received: by 2002:a9d:7419:: with SMTP id n25-v6mr5957otk.1.1537828248873; Mon, 24 Sep 2018 15:30:48 -0700 (PDT) Date: Mon, 24 Sep 2018 15:30:48 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: <2d708865-8b2c-416d-9343-b550121e596a@googlegroups.com> In-Reply-To: References: Subject: Re: [HoTT] The Hodge structure of a type MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1827_2084890994.1537828248239" 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_1827_2084890994.1537828248239 Content-Type: multipart/alternative; boundary="----=_Part_1828_1867526965.1537828248240" ------=_Part_1828_1867526965.1537828248240 Content-Type: text/plain; charset="UTF-8" However I don't want to discourage you. One possible solution is (differential?) cohesive homotopy type theory (which is at the moment even more undeveloped). This may allow you to talk about manifolds and their structure "synthetically" which would allow for definitions of de Rham cohomology and possibly with care allow you to talk about hilbert schemes of some torus. Pessemistically I would add that it would be at least 10 years before any of this is considered. -- 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_1828_1867526965.1537828248240 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
However I don't want to discourage you. One possible s= olution is (differential?) cohesive homotopy type theory (which is at the m= oment even more undeveloped). This may allow you to talk about manifolds an= d their structure "synthetically" which would allow for definitio= ns of de Rham cohomology and possibly with care allow you to talk about hil= bert schemes of some torus. Pessemistically I would add that it would be at= least 10 years before any of this is considered.

--
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_1828_1867526965.1537828248240-- ------=_Part_1827_2084890994.1537828248239--