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=-1.1 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-vs1-xe3a.google.com (mail-vs1-xe3a.google.com [IPv6:2607:f8b0:4864:20::e3a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c86adcb3 for ; Tue, 4 Dec 2018 23:15:43 +0000 (UTC) Received: by mail-vs1-xe3a.google.com with SMTP id b203sf9470018vsd.20 for ; Tue, 04 Dec 2018 15:15:42 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1543965342; cv=pass; d=google.com; s=arc-20160816; b=oUq3VmWU9tRtCvQ127XmUjnC4gtk44o9SWr1lFObFyxKKMPvkwskbyW8kGvVErvilS KO1pOFMzAKpbpA2RnJr0ysZ7tyjoKK1q/dWiFetU5YtRx+67BSOXZVpEp6zmgJrqm060 qwz1HYSIFx+8sti/w3Z7xQ7TNAugO5IG7G9d9DgyDOICAin8aAWLdSB4D5rb2mXn+S1Q VRNVbOTbU0DLngKEDPXuMsQ9z2rSvhiYx9NqFL+TSFxU/22DY4RGB6wUwij7Cj+BS1os NQ2FtnK3kA4A1f/5CzvMlIeYo+KKI1tvKtRMXUsf/TcJlci2/QbZn8M8JulAITVYQ9a9 WI0Q== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=E3lYl8a158gcu2Mpir6xuwly1bbweH0c+wFM3/tjyCc=; b=MZpl1W6ChjL7YxZldexHYlTNsFDknPm5uAd0ZeeBsLcjSr36mUEG1AgCW005vBof8O Gfu6s83SIyWWO2l5ZN0wdE5cb/wEeh1PnmIXYsnlU1d/otxAz4onuKKpBWBXWjDffOjV sQ0YHTNY7ZGgrzMbx5008JmgkaaXa2c7lNMljheToOzEoFt35iYfWUrKxiyTISMdokkq hUhxzzohpOE8VZ4X7qsOMMmnR/YxIr2WobqovmPP5evVG5/TcH6r6E8mcfC5BpBiLtZ9 6pWCVES3lqUhObnHJjJCGEydCyD8fvLLRph2xGMc6nc0uOksd0clmK3WRj2F3hwmje0F +Hwg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="r/OsCuVZ"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c30 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:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=E3lYl8a158gcu2Mpir6xuwly1bbweH0c+wFM3/tjyCc=; b=KoATPgqq++V83ycFUVbM6R5Om/HoEul372g/bhrB54fY5gLaFTfGhe5Rb72wJNpDDr 1ZTX7GkH9iLaO5xPBJPP9n8fKmANqV+u0qGllKcvXAGiePBKvy3TbcLDfirDmWPN9bjp h/ghbmfEcG4bTTftSFHP0SFUXQWOwT2z2g9CSUKbiEWCs2lnFfJGCHBy3YIXolVcs/Sd 9RTynvOL9ouXdq8h0X5JzJgW5rqVe1HchbqJaF5UTWGSdBoR+i0MYXNyaSS7DpTT6ce2 iQtNv1surw0DQ4tw3Kmz+PztEhlwV+7FS0UjGgiTritP6IGkS3bGrqiXIbViAjHryfLd sl6w== 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:references:in-reply-to:from :date:message-id:subject:to:cc: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=E3lYl8a158gcu2Mpir6xuwly1bbweH0c+wFM3/tjyCc=; b=bPtetPMUmaE0M1q4HQq1NYnNMyueAiJONJkpwGInzMH2yefrh4+Kksrh+hKd7hCBrU f69MtBPRYUWs6EkzH3+79VgYKYSeQDOwkX9xf5TYWxPPMET+/WXm4p1QGNy8X8B9bWj/ 6dos4ELz9/+yob4HWzlomtiBUrxzPaKr7YofYV1ySnQIHO1jrsgssiDeJeyosSQhHYLA VYAJ6TjMs84Ip6TRKfSq6GoPda/4Gf0vPtLeJTm+B9SMKCTMSNuk/kSeasCKKJlEjG5N 7LHM/0Mg2MJOg2TBx7PW1r138D3WJlr/GZG10w6Y9gAPAP1PumkJd/Aq02H97SWjS/mx gAmQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AA+aEWbDK2n7hxDDl1pKtJ0pcwuLfyBtZSilCC/z1ufqj007JN4HgAuS cGccfqwWGSuAAKl6NJSPt1M= X-Google-Smtp-Source: AFSGD/XcnMql6j37aLNccqFxcfaX6Q8yYDS5KFBGgtVkNe1kdIkLxGGj+2G8XpJRkfU+qlDJYlvF8w== X-Received: by 2002:a67:698d:: with SMTP id e135mr67551vsc.0.1543965342075; Tue, 04 Dec 2018 15:15:42 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:2c44:: with SMTP id s65ls2877104vks.0.gmail; Tue, 04 Dec 2018 15:15:41 -0800 (PST) X-Received: by 2002:a1f:4e45:: with SMTP id c66mr18675274vkb.25.1543965341755; Tue, 04 Dec 2018 15:15:41 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1543965341; cv=none; d=google.com; s=arc-20160816; b=bssYzNQSlsEmHIyfua37xxjj9Br0aETql6BuBlLTD6ymP1C+GE4uz4eQgkPORR85np 65eezSSLFAnt2Hpk2aBWFBteh7gJdV6983XShgRXwM/X4Sqk6gmeyL4vVJKMW40FLpV9 Hfl5oCHFgXX0UHel4D0HpXxl6XN2iFhv99sCR1fgZnVZCnJzw3dtjn1cSz1p5e34g0fZ Vdg3f/gCy2JXe+uIBGlR4JwUZ3VuCF/mIiz5bBgfXC60p20Q4q/feMEjCBbgH0N7xDPN /+L3g9wqACM2sQ0bE4j1JppdeWjbfkuL/Ah2BYI6LNfJRvWw+oh7wDkeLyxAJx4PwJzc gryA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=1vVxwpYg3ZQBv1Tm6m/32pAyTEqCwNywz98OqhC3Iho=; b=cl4f6h5PHx/gYT3gmV7+J6DBxqU5edV8MSI74j7qKzAGnsiavaSI2Uwm9wXdey48HQ eoc3iNV3LLFPcaumuOgL9yFosh5IfouLmTIxsq2vDx0GmYQ1yqZGjhtu5L1+dvh1QElc D1f+LQPJYOuGoqmAtZvluOFhFpKV4gP8UJ+Tu9WS1DH84SJL8MyEnO3tqpKjNYeXIckw pCrStE3qxQxv+k3b6vssLW8XjmMsafP/+fTt1oXqfgv+CvAYLyO9oWz57TzoreAzNvei YErRj0o5pzinpU1u8WscrPqrWzqU1NGJQwxdclaiG+En2qbCCBeTdUUpDtHrLJ6sMPdD SuWA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="r/OsCuVZ"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c30 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc30.google.com (mail-yw1-xc30.google.com. [2607:f8b0:4864:20::c30]) by gmr-mx.google.com with ESMTPS id l127si901024vkh.3.2018.12.04.15.15.41 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 04 Dec 2018 15:15:41 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c30 as permitted sender) client-ip=2607:f8b0:4864:20::c30; Received: by mail-yw1-xc30.google.com with SMTP id x2so7730647ywc.9 for ; Tue, 04 Dec 2018 15:15:41 -0800 (PST) X-Received: by 2002:a81:b615:: with SMTP id u21mr22370655ywh.174.1543965341199; Tue, 04 Dec 2018 15:15:41 -0800 (PST) Received: from mail-yb1-f180.google.com (mail-yb1-f180.google.com. [209.85.219.180]) by smtp.gmail.com with ESMTPSA id y1sm5865035ywe.86.2018.12.04.15.15.40 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 04 Dec 2018 15:15:40 -0800 (PST) Received: by mail-yb1-f180.google.com with SMTP id c15so4243570ybf.7 for ; Tue, 04 Dec 2018 15:15:40 -0800 (PST) X-Received: by 2002:a25:d7c4:: with SMTP id o187mr6000929ybg.357.1543965339826; Tue, 04 Dec 2018 15:15:39 -0800 (PST) MIME-Version: 1.0 References: <23d2a68e-3428-4ce0-bb9c-7fd921406022@googlegroups.com> In-Reply-To: <23d2a68e-3428-4ce0-bb9c-7fd921406022@googlegroups.com> From: Michael Shulman Date: Tue, 4 Dec 2018 15:15:27 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Does (co)homology detect inhabitation? To: Ali Caglayan Cc: 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="r/OsCuVZ"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c30 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: , Of course. WIth excluded middle, either ||X|| or not ||X||, and in the latter case X is empty too so its homology and cohomology are all 0. On Tue, Dec 4, 2018 at 2:33 PM Ali Caglayan wrote: > > Can it be done with excluded middle? > > On Tuesday, 27 November 2018 22:22:30 UTC, Michael Shulman wrote: >> >> 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. -- 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.