From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDWYNQEA54IRBXPUUXOQKGQELVBV6EQ@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.9 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, 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 6a1d300f for ; Mon, 24 Sep 2018 23:59:26 +0000 (UTC) Received: by mail-ot1-x33a.google.com with SMTP id f11-v6sf22594429otf.7 for ; Mon, 24 Sep 2018 16:59:25 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1537833565; cv=pass; d=google.com; s=arc-20160816; b=ug8dYj5L+iuWvXP5QZIF5ajUVGahUg1WHD12J0kU91uRZWcM2dPWmaXYTvXW57jEPo VV30WyGbtciTvoeC+uSZHtkJXH+fSstDD3LTiD4I8exNomnll2IIujZofgd53/97f6+j H3uGDsnKbIMEgdC/an929ON3vnze8Vc1W0uL1nYmgNOUgIl+koiL6zcsll/Yzi/hy+qf Vm5YiK4UvLrbF4ccErqdnOF4Va8hN8iqPYlQ8djU1gtYjq9MlZtXYsG1JcirNE6EwS9F w3o0jzK4CQxF53of2NcptrKLCpaz+sNZSKfaK+TVXuKg2sBpQssQS78Dk3cwBVzOmOed LOrg== 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:to:references:message-id :content-transfer-encoding:cc:date:in-reply-to:from:subject :mime-version:sender:dkim-signature; bh=OUTZPcC4FaV2ZlqNaORgveDpQNWPsb9esvLxs9wdl8Y=; b=AfLknV7muOirKQABhet24ri5d3wPETDzjuuSaGMeUdg/jXYr99Fh7IL8ThP0qPWpKR jbpc/AFB/Gx5+5VswWUy0cIb6yFW77XJmC9SyBoJ2nLHtnf/Bito8R5d6j1kfCeZCTJB wSIEGaULUA2BzodOe025JqtDpd6oii7wA+6WmwAfQ9vLv41SJLlTGDFfQYOWN/cpUV4E WCVSJl4GPtQvRQMiaF9itnhpPPHZIoPDNqskGhCywM2nM/yKM8+DBsm06tSEJeAqVxi2 hRV/PLFyudGfxzqjQFJI+Z0mNG+YtmKhI8IvE7XVMOXkYUZB7IR7xO9WxEJD5y0qg453 TRnw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=fOmToW8q; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::836 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:subject:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=OUTZPcC4FaV2ZlqNaORgveDpQNWPsb9esvLxs9wdl8Y=; b=HXuaQ4omBXo1sm1sj+GEXunI1/+Hob1cWPvZhWgrdhWuudC/YvANaW79TBV+N8xV3C 31LT87ZMfTtNdia8UYNGD1c6fHNfBz/q0yO4z4UJIzD6autnwFFJbJCzjA6hpjIkq7F8 sj687kpI3VfcsaSzl0ddE3d/QYhG9FAeD28n305rmmOu2yyl2OGfWthCfy7ZhwlMW3A1 re489GRn14DZwy5aVNVXfR89stWru9mdPmeNIXwsTYkAH3N/tUKglue3ltgmxTPUdUMq hQLs82gZ9G+Z2GOKBwOobt/TZyHKoIVghGKdN3jiK8T3DSCJ/7GkbDXG1wYrX0WCT8YP QVEw== 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:subject:from:in-reply-to :date:cc:content-transfer-encoding:message-id:references:to :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=OUTZPcC4FaV2ZlqNaORgveDpQNWPsb9esvLxs9wdl8Y=; b=B8Uznb49uDDuNpZNxlxnMRtwpWeOGra81a9hjzCL2lJViOZdzKd8uB2w3p85lkqjtd 1JBmeQ7uIqYvXr52q1nD/B42kJNSG0IqTKRsGbHR8DX8gBfLb7dRvX3zLdtjDuU54aC2 wN/6+9lv0T/S/yTrNQSKnN/QWYg/i9ozgCsbcJjLV06IRKPlWlILYxbHmmicGlQ62OYo +Glgp2rxJCjTfHGlUhaTBKaVBTIxDe/UtSTsLZj4bjl3JVYTz/ttWiZh8bUTXuc5RGKy ATWop3zKXHLIcutPwelR9L1YWV1IVoPJktXgXdQo9B4n0Z4U90HiDrfYXATWtTuvc5at dBSA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: ABuFfojd61NvDy29HPjSGpiZ02iJrQNY4wx/X4y1vz6Nwmj4EUTqZ6DD If1muam90pzP4I1KE+UBQKs= X-Google-Smtp-Source: ACcGV6160J+vdpXPtnW7PqA3dgU6prWdiOKLy9TQEK64R9a02jHY9ZN4Xxq9iSQo7SC2Zd6v3GdmQw== X-Received: by 2002:a9d:4049:: with SMTP id o9-v6mr7620oti.2.1537833565279; Mon, 24 Sep 2018 16:59:25 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:6554:: with SMTP id q20-v6ls3557522otl.8.gmail; Mon, 24 Sep 2018 16:59:24 -0700 (PDT) X-Received: by 2002:a9d:ba2:: with SMTP id 31-v6mr1590133oth.49.1537833564920; Mon, 24 Sep 2018 16:59:24 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1537833564; cv=none; d=google.com; s=arc-20160816; b=THdgYM9sgdRfXt7dmtJXZRMmo4a+gZHQvCIn+pI2XW5E7p3JYK6z+xRm01P5Jhhc+U NqTQhBthikG+bVzhVOw8VDjDLc4uIDXF74ERw2ksp9ISwU0HqmjHz8p8Svrv538YCY49 4XdpCe8XY0v1vSqM0B3ZVAcc3km+/PCerZ1B0oqautE7rM4emcogrh1JHi2G2pR60k9l ieoF9Oj8UX3xh30JvEt88Pq0HBMbIsuG8Ls91Qup+vS7e9WdLlM7uO5oEnvllQht31yk O4FtPX8KJnwoUCB1vQM83oGf5A5P/rb8JCaMkkbqgHcbs6c/ROlIMzXKFsLpmKoSd0Ga l4nA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:references:message-id:content-transfer-encoding:cc:date :in-reply-to:from:subject:mime-version:dkim-signature; bh=jNdM3nRfWebsy3HRzIQvt/VWDTW5wLClbQY57tDt+qQ=; b=BmlPrKUTvwip3xrjGOVZYScNN3U5jilKsOey2GWTjqH+VVPgPfd5LtWnUNaorUEHEQ kxQ4nYELWXwdhyqMjOmnWaQbhshaHnLk3uDoPznKP1ZSssDeMqRarY9X/CEhhDX52uNC 7cqZHC/4JTygZqymhVVH95SxQ43UqkxYe3Y9Bg9G/XkO4MKS0k/pwjUYcAGimFqe7xTu lMdJ+Wo09zTP16Ba9xeeaOwRVAFoTq/tUWTL0X19rDUKNw3YtDgljeG8kPWeZEhNe4rE ffUVpaj00ZqTR0U5rzrdbH4FRXTqBiafzEWNSB8g9zVKt43jaP3bAZjksJgzTy0bmo+O IvRA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=fOmToW8q; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::836 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu Received: from mail-qt1-x836.google.com (mail-qt1-x836.google.com. [2607:f8b0:4864:20::836]) by gmr-mx.google.com with ESMTPS id f68-v6si50411oig.2.2018.09.24.16.59.24 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 24 Sep 2018 16:59:24 -0700 (PDT) Received-SPF: pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::836 as permitted sender) client-ip=2607:f8b0:4864:20::836; Received: by mail-qt1-x836.google.com with SMTP id z14-v6so6518987qtn.2 for ; Mon, 24 Sep 2018 16:59:24 -0700 (PDT) X-Received: by 2002:aed:38c7:: with SMTP id k65-v6mr1024125qte.84.1537833564726; Mon, 24 Sep 2018 16:59:24 -0700 (PDT) Received: from steveawodeysair.fios-router.home (pool-74-98-211-223.pitbpa.fios.verizon.net. [74.98.211.223]) by smtp.gmail.com with ESMTPSA id z132-v6sm428900qkb.50.2018.09.24.16.59.23 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 24 Sep 2018 16:59:24 -0700 (PDT) Content-Type: text/plain; charset="UTF-8" Mime-Version: 1.0 (Mac OS X Mail 11.5 \(3445.9.1\)) Subject: Re: [HoTT] The Hodge structure of a type From: Steve Awodey In-Reply-To: <2d708865-8b2c-416d-9343-b550121e596a@googlegroups.com> Date: Mon, 24 Sep 2018 19:59:22 -0400 Cc: Homotopy Type Theory Content-Transfer-Encoding: quoted-printable Message-Id: <37A3D139-B011-4E22-8F56-799BACDB642E@cmu.edu> References: <2d708865-8b2c-416d-9343-b550121e596a@googlegroups.com> To: Ali Caglayan X-Mailer: Apple Mail (2.3445.9.1) X-Original-Sender: awodey@cmu.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@cmu-edu.20150623.gappssmtp.com header.s=20150623 header.b=fOmToW8q; spf=pass (google.com: domain of awodey@andrew.cmu.edu designates 2607:f8b0:4864:20::836 as permitted sender) smtp.mailfrom=awodey@andrew.cmu.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=cmu.edu 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: , > On Sep 24, 2018, at 6:30 PM, Ali Caglayan wrote: >=20 > However I don't want to discourage you. One possible solution is (differe= ntial?) cohesive homotopy type theory (which is at the moment even more und= eveloped). 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. P= essemistically I would add that it would be at least 10 years before any of= this is considered. just for perspective: - 10 years ago we had the (higher) homotopy group(oid)s, and not much more. - 5 years ago the HoTT book was just finished. - 1 year ago the Serre spectral sequence was finished. things are moving pretty fast - I would not be so pessimistic. Steve --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.