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=-0.9 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-oi1-x23e.google.com (mail-oi1-x23e.google.com [IPv6:2607:f8b0:4864:20::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8d7a610b for ; Fri, 30 Nov 2018 21:54:17 +0000 (UTC) Received: by mail-oi1-x23e.google.com with SMTP id r82sf3746726oie.14 for ; Fri, 30 Nov 2018 13:54:16 -0800 (PST) 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=rIJfcPSwUhL+z4ZSeRAYIiXIUwbhCuoImbgw/gFnfQg=; b=mXdEQSTUK7o9wgxUbdNDXRdJ5QqOHbpfG8DNWp+EPzNSqv7EeX4vEfaGIxP1BYXMxT GC2LbXSHqR/P0iCoz0pRdy2plrKdkz5RFTgx6AReNAiQp+ci6g/fMa1vWKioFLU6ZPLJ 98B7qsl6FUhW8EXVb/A+kD/A7dX5GGNC6dpTeXC6LaD/7l/kX+8HfhJ0vwb3cPz1bMBg lzrAfpUu/O2I/1PuGgJnr7QfgV+8xyo54jn8S/ox/8gUKqsz79Xg5CYcuBEX0SBGzEVY zUdEdnujxDopOMaAFAqSpvUyH01++A4mseRLF5zXXttg1wkmelY+pj8Q8buyu3GUn5mF mAmw== 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=rIJfcPSwUhL+z4ZSeRAYIiXIUwbhCuoImbgw/gFnfQg=; b=UbH9pe58edKkSBNDpyRNFCbe8/chtA9kopCZXRXHo4+HYdT1avqxs7KQ3vvXdPrJyL y12+2076wkXer6aEEZcWNv8lsOLlXmlyWZw5hUshZ/DYMo0dygq5K6WUXe9IDhB2Snfv nZSwWRAP0hKI3bahNPKqfYtJ9EUrz4S75q0JlPp0CRTGcjup/NyEFhqha7niqeBuNGXF NZYZhxQhZvrvZE7zmPMgCZjGwGRJYIbpAolnASGS44ZYHDsCzIIZvbzgdaNAzo5hxy1c MtSXJcftT/ePO+BWn/RzlPg9J8g7NwDHzeFRt0CxfhGdPa4tT5QHR/oeGWB+9uhM0yIO YG6w== 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=rIJfcPSwUhL+z4ZSeRAYIiXIUwbhCuoImbgw/gFnfQg=; b=NDEzdfyrUDvajt1TFK6tHOD8vCCVyPrBEroTKA9xq8vhaViPXhoxL5OuytKNUUcUSy +VL7FL5u9olGmnPrIMo4Qkafpj/+atoEoeOG95GqPBG3j4SCQ0c0GRYbscdFjscqxjem TcZWpl97zNHF/iEnz89EUdvyYTKpcrnESm4mtXSho7QBmSMaq75z0iukYj5bWHxXzJ7b aL6thkujb2RD1Mz647dOkvTEjD5V8tJUWB5PeHRZcMbYNOFRdYAWjazUUFviphb1za2+ thJyaP35gzAk8Symhj5pTNZScJE4llhkVWmZMv0lPZpA/f9ee8bwrZDIuAiwpgsWt3hN lX7A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AA+aEWbDZWVVT4z7wyLGspQnp3BznlQz5QtZ2/OluN/XU0clLxMwcQNy SLgxiiqPKK1fTiFEiMHaGNs= X-Google-Smtp-Source: AFSGD/VrB8pEbNN+tIy7Vep+P8UWLAH+6D/Bhvzrlx6vN1RBEo+5ej/+WGyvyRp0a3r61shrx4Yx6Q== X-Received: by 2002:a9d:ef3:: with SMTP id 106mr91513otj.6.1543614856034; Fri, 30 Nov 2018 13:54:16 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:ecc:: with SMTP id 70ls4092733otj.1.gmail; Fri, 30 Nov 2018 13:54:15 -0800 (PST) X-Received: by 2002:a9d:5403:: with SMTP id j3mr94276oth.2.1543614855345; Fri, 30 Nov 2018 13:54:15 -0800 (PST) Date: Fri, 30 Nov 2018 13:54:14 -0800 (PST) From: Felix Wellen To: Homotopy Type Theory Message-Id: <50d9074d-b7e4-4cfd-8eef-ab40efa3a2ca@googlegroups.com> In-Reply-To: References: Subject: [HoTT] Re: Does (co)homology detect inhabitation? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_3336_1401232872.1543614854772" X-Original-Sender: felix.wellen@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_3336_1401232872.1543614854772 Content-Type: multipart/alternative; boundary="----=_Part_3337_1018956920.1543614854772" ------=_Part_3337_1018956920.1543614854772 Content-Type: text/plain; charset="UTF-8" Thierry caught a mistake in my answer, so both my counterexamples actually don't work at least for the strong requirement that Z is factor. The problem is, that the cohomology classes/maps P->Z I use are not different over Q. Am Dienstag, 27. November 2018 17:22:30 UTC-5 schrieb Michael Shulman: > > 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. ------=_Part_3337_1018956920.1543614854772 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thierry caught a mistake in my answer, so both my cou= nterexamples actually
don't work at least for the strong= requirement that Z is factor.

The problem is, tha= t the cohomology classes/maps P->Z I use are not different over Q.
<= /div>

Am Dienstag, 27. November 2018 17:22:30 UTC-5 schrieb M= ichael Shulman:
Suppose I have = an (unpointed) type X such that (unreduced) H_n(X) or
H^n(X) is nonzero for some n. =C2=A0In 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. =C2=A0Can I conclude (without using excluded middle) th= at
||X||?

--
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_3337_1018956920.1543614854772-- ------=_Part_3336_1401232872.1543614854772--