From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-2.6 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-pl1-x63c.google.com (mail-pl1-x63c.google.com [IPv6:2607:f8b0:4864:20::63c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 5b7c77c4 for ; Tue, 27 Nov 2018 22:22:32 +0000 (UTC) Received: by mail-pl1-x63c.google.com with SMTP id 12sf10284473plb.18 for ; Tue, 27 Nov 2018 14:22:31 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1543357350; cv=pass; d=google.com; s=arc-20160816; b=qZc1UmlEmsjOZyValZ/M3wk3iHLR3B8cMe41jC9gdaYhVQHBIKfjsuLR4aAuv466K4 KE1iAVOHDyrsVcdLZSQ2MLn0Y+tz/0wdbFm8BctXFpUbaO70a7eYNvA6BY3wXv5luASK uJQ3EnpOPZ62i6Z5Da/CMTlQtzvkSYluBg2v08KEUmKcoAGmmyDVdXZsCmphR2Gomb6P USRg7joo07Ku7Yt4Kja4cajjyDbtc4JCtbvJ5zC5iKhMqrTvrs6JoIiaFfvZ/m5AM1fb hA+RzRxEZ4C2PNNV83xtXApQizDMRPWSSiiSqqo3JrSpYVBvbpCGRs057POVIE4a+6CX XkVg== 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:subject:message-id:date:from :mime-version:sender:dkim-signature; bh=Ps7NSQ9ITVbQrXrs2aM9+xzPIe4F3itS/jPZ2YzE2q8=; b=MV9gyLFp8EGgjcwIq1g6E8YYEbMBPLor516Fav5P1NyLOtwbP1EXPSxKRicPaw3X/t JIpYI/SaVse1v+infmMheCneKa2lOaWcpM3V4AZoqc8hT8z79mLFLvEypcW+YDXgaXoo 9ugUdrkWvtZH60qKOLoNt7BzXLRtR9n87nWVFF8ixRQbugff6L+bhii3DvvuaZyR6MsI eC++E6BFsAyQ7DhfrsRReyrrzz6az3edm7QhaHMbAjMUqsIihOSuP45ErNMI7akUijFC iEM3kXb6bbCs9GiYI8/Fwdg+TqpQv0jhyYHyAzcwEHF6cU6rEhZHeoBDPp5Lc5uKvkKI eLOw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Epqy4ETN; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Ps7NSQ9ITVbQrXrs2aM9+xzPIe4F3itS/jPZ2YzE2q8=; b=fvmm5mh79UwwCxdxyjdfa1Qyj3Bp9niZd+SpsYLd8AAA0Adi/gcEckcM+uhWY6s0Bt cP5rI/3mOphQHu6JlfQ24ET8fvtn1GA5GnMogjtJku1xUpKnbnKk4JOHmkm8H3DiJZJR pG5HVwyP0SxuT9Sfgf1I9iP4DCVuivlguIOE+CWusfCh8DuTqojNxwDOUHJVv80mUn0D aqGAhVSlMcEbKWH/eFhBCJbpj4w2FBYsKHH7DjHPpoqu8YzjIqATcr8mWrVqjRyenA+F c/4YeeUY4rWh/I8bTEQr3pkEdRPv/JZopvNvm6DzggC+Wu7DL/mtr4zj/XSyr+iijF0j Ly7g== 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:from:date:message-id:subject :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=Ps7NSQ9ITVbQrXrs2aM9+xzPIe4F3itS/jPZ2YzE2q8=; b=Q63PM+bgO0IK1vzY/FU7vlN69QniaEEjK2yftSfYUzkrG5hXE9u69zofNGyHP79ai1 W+g2y8ubT/dbqEIcfvzQjhTKTxMvc/3/3kJQr0GTzMHJbc1tbc/9ecqWrnWCpC2ENFKd ierYVgiZlMPJQ4BjzfMc9UffeICn4xV3gfstEGA2jpPdPZnSiwucRDoQcHE8kanGUI5E U5Q/Hteil9m91IPF0CyFsWiCKX2JdBZe5kF2BJOiMkx35SRMJ9GQtO//ol0kKuSGAfpl PSMfpzl8RnHoGMM3uzLsE8BTiC48z4ICOcMn/Sbk9wTZ4IjGlkD2PNvGEfl5lWpeJF06 /8yg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AA+aEWb+02tgYV4LENdslZzh76XOaUNbUmjAFoQ7B/VxuYnYuhy/Kh1p vMB7ztBP2rudRFA625VrCPA= X-Google-Smtp-Source: AFSGD/WuunTOibvIPQqcKTZrClFvruCy4FiJQ6KSYDKrMYXX/EaF1s+qnTY5bJLXeyLHMCVf9/P20g== X-Received: by 2002:a62:45cc:: with SMTP id n73mr21430pfi.2.1543357350178; Tue, 27 Nov 2018 14:22:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:18c:: with SMTP id 134ls3893894pgb.4.gmail; Tue, 27 Nov 2018 14:22:29 -0800 (PST) X-Received: by 2002:aa7:800c:: with SMTP id j12mr1313425pfi.128.1543357349819; Tue, 27 Nov 2018 14:22:29 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1543357349; cv=none; d=google.com; s=arc-20160816; b=LJ4cDf+uO4UBFMbchvSF5j0z2qevL1WxgSaMuNmBcMjQTIgQQa4xLuvFPZzyFl1JD5 OyB+dhBnpospZwh2Mo1i3RDstQQB98kYZemSpeRPl/sUshWnHXVhti7/BZCjKkUQvl7B eHeTeBWl3Oze5MHPtzrlBz3sUGJBVEtIw485M5/KdDMB3yiWGqG5rm8eHFnh6BLIRkWv 2g69hDtrhEaqjBO7ks36e7Iz6S9J5vpD5l9+bl7YO2WHmiyy6UWRAw8FJS7djymLAMFY iFQ0uesaCbBKU2MR9nOyHBl5KIv49xtYQfV2MZ75Fvt5TfVlGKFXo1I6XhEQK87D08pz Lkjg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=9Koh9Enizes/PlQo0epVgtlE4d3Gkyz662oq4aOflZc=; b=H/TXIDLPv6Xqu224RwdKgMyUXHMEzbZt6iusmHiInTSFhfM3ihp3eQCNkvQ+d1DNbF Chuq93rJNhdh5KXaDpgidWwaEo6F7Oh1bRZ40rn/pkNHF7rAizJJuDs6zoa6D62YMMpC bTNe7sw0efi1cnrLlfabKp1RXIYu7pXEi9Gb8DYnPQI/ur7tBw0fHRv4D2PE7bumOUot bJnnRyVzB+bHCb349a2kpqlM1XU+fI/VrlYonhVbtml/tS0pQBkLZ+bLmvq0WSnw+9vC EViqwNKsDM0D87Ipbt8Qwoz1DXdry6YsjcNpr6lkP1eeRaLz9mHyWt565zOH/JMANPCE 0Y6A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Epqy4ETN; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb2a.google.com (mail-yb1-xb2a.google.com. [2607:f8b0:4864:20::b2a]) by gmr-mx.google.com with ESMTPS id r8si257130pgr.5.2018.11.27.14.22.29 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 27 Nov 2018 14:22:29 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) client-ip=2607:f8b0:4864:20::b2a; Received: by mail-yb1-xb2a.google.com with SMTP id t13-v6so9779344ybb.8 for ; Tue, 27 Nov 2018 14:22:29 -0800 (PST) X-Received: by 2002:a25:f626:: with SMTP id t38-v6mr36080141ybd.285.1543357349391; Tue, 27 Nov 2018 14:22:29 -0800 (PST) Received: from mail-yw1-f42.google.com (mail-yw1-f42.google.com. [209.85.161.42]) by smtp.gmail.com with ESMTPSA id o14sm2114245ywo.52.2018.11.27.14.22.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 27 Nov 2018 14:22:28 -0800 (PST) Received: by mail-yw1-f42.google.com with SMTP id j6so3591271ywj.6 for ; Tue, 27 Nov 2018 14:22:28 -0800 (PST) X-Received: by 2002:a0d:d755:: with SMTP id z82mr35670689ywd.190.1543357348602; Tue, 27 Nov 2018 14:22:28 -0800 (PST) MIME-Version: 1.0 From: Michael Shulman Date: Tue, 27 Nov 2018 14:22:17 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: [HoTT] Does (co)homology detect inhabitation? To: homotopytypetheory@googlegroups.com Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=Epqy4ETN; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b2a as permitted sender) smtp.mailfrom=shulman@sandiego.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: , Suppose I have an (unpointed) type X such that (unreduced) H_n(X) or H^n(X) is nonzero for some n. In the application I have in mind, this group is nonzero in a very strong sense, e.g. it has the integers as a direct summand. Can I conclude (without using excluded middle) that ||X||? -- 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.