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.2 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-wr1-x439.google.com (mail-wr1-x439.google.com [IPv6:2a00:1450:4864:20::439]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id bbd0f687 for ; Tue, 5 Mar 2019 22:47:55 +0000 (UTC) Received: by mail-wr1-x439.google.com with SMTP id o6sf6263858wrm.2 for ; Tue, 05 Mar 2019 14:47:55 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1551826074; cv=pass; d=google.com; s=arc-20160816; b=P+AWW00vDA8E0IosqJZLK30eJP7Uhfd6Gk03CT2VIUe3FyDiq0YHcQmH/qLBQ1rcLi 4BiAkSHxwqlV3HZcmJg7+RvNM0osXqj1CdJyb03kFonh2jGlm+T6EkxZuHfhjWO/+1j+ T3WgMxBpx3HI/qfyHSH5z1KhPkOwPFxy6ZBn1afxzbOPTvwdqQcKyCw4Rn0m4+m/GjJx EQ1Jm0UAAfA3ecXRt5xIkkfjHjLumgbFB67/soJuOqm4xYmuMs87E+LUVE+xV3c7Tlwi 98wjHau5ol6JUfYTgRGFweRV3hO/12MjwBdJjiMOgkBsEqTrZhObQRzAsdXqEPfgU7f6 dCNg== 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:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:to:subject:sender :dkim-signature:dkim-signature; bh=1M7hlLRMoKQvjJ4+LmCX7YcR6fnbCxZdaJrvhY5aaKM=; b=SDF3bmddsx0ugJBsgzJy82zpHex24HW+pkHR24a+4zTTx0rZJaRvBy/gn9F/XCZY+q SUKjFx9eYk0DgKw6Pol4B1uB2U4miNs8/x1MNgwbq9feWAUdZf7iRGqLgCHtSPTOcdhs xkR2cGVdSti0hzCCtA5TBIuqkgd0lPTXX3DmBwximn8xK7UvdWtoC8lVq4NnaIg0MKCT VchBiy60Ig0Mz4tyAu4X77FfOKrQMrSWAzTF5gM7l99flBn3H2PjBQ77+6bIeyxP9YFV RjkkM8cJgc2tA8JvejccDTL+ONAQlBGIodV1O+t2kCNCnpcatfTfCzKjlWXUqtawGZhb +qkQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=BjYLQzPA; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::32e as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:subject:to:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=1M7hlLRMoKQvjJ4+LmCX7YcR6fnbCxZdaJrvhY5aaKM=; b=Vtz+xPPidhBhGrgMhJuKJE+KLbso2urB0DQr3OnAN4x3GF/s8VNxtA++SE5QF57yqS v0KGa96Hs39lMkNhIKykzcaRRpIzKz6SQVPXSTGoW4HTliMr4hjVwWuttQrVL8YcqrIl 2/7m/Mhga2rNq/fJP8tnWuImofxN8Ncc72g0N2vWDUMdo750DgQxDmFjuMa5lC1Z9Oz2 vUEg8phDnxI0hAFIbVZBoqOh1q/XE+S718k7G+GfMNmloj2v1Qv94jEYcpfQY7VSrokE Tz0+zYjETOX637RfOm2Wsf+vEhmATtW5qYYxdsZ2fhrhebYzHraLt8eOlxtzv7FxV8fq BURQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:references:from:message-id:date:user-agent:mime-version :in-reply-to:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=1M7hlLRMoKQvjJ4+LmCX7YcR6fnbCxZdaJrvhY5aaKM=; b=ZfI04F4Hyg59OsYyPVKuMpdCVtpXogsztk1cygOEVcu4WHkEQqEdTS1j68iAfnBj38 Wtb+wfKx6zt/u4XDTijmIuyZvO/Yzrt5lBiuIFkvm44U88e9rfkJ7MODo7LHfPIghSgR srzOswnBRkQaGg+LOlWSF73r7FX1xJo2jLqRJMmayItFPIXYvsZ/IANcodKjDfUgxemP uBjxvJt2uX4K7kmfHYVpGu2iPXEhEGCvcKzXUzMCcmQnpSRm3794UvbXkdctqJaDJNEF vP5EILaOpR7HD8DR3hrIys7DIfCijlbEikJCqauiGAIFUe/tStjPqfU0tyvHYv6rZpkA hqpw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-language :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=1M7hlLRMoKQvjJ4+LmCX7YcR6fnbCxZdaJrvhY5aaKM=; b=cJNFntPgFtiOHOqoQnoY0sDtqbt1eRTGsWikqb93fE/QOG0RlctJGROGQE69nQ0hiX JYZSi+AoJwkEYsTVzQxgPpxAbBIoOV+7DBb1dQLmhRB5ehmkEdxuvfuAUIPHx+OnitXa 8LEYHUNVnGaCxWp3XJF5e0pPCvlf/hQPKyY1tLUY0WaJtdAYw+oVlRmoQBhjjvPKOGdj 8+iFDi29hp1w/1YiU6eDCA/98oDXnd6oIWq8GJLrFulY0aPJw9g5gB6UCRRKtWPLFOrW RyAt0cOL6sgcM2LMBmWhkW7DBHP0B5Ix2snyEyToAVj82HQKxReEQmjYMwPItE29RFR/ D1UA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXdOKmmnugxXoHxc4ULoGqAK6g4gmCn8o8qAmU2FkIGhdrGEKcd kX2kLQ/AzAW7yTmqhOEAOl4= X-Google-Smtp-Source: APXvYqw904lkCN4JQVJteWrepGcQFM8tdV1FP3FUbDW2sm/r7VXMzzMq4TZQvwp0CnNycSZP+6KA9Q== X-Received: by 2002:a5d:6a8e:: with SMTP id s14mr733031wru.31.1551826074670; Tue, 05 Mar 2019 14:47:54 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:b641:: with SMTP id g62ls516034wmf.11.canary-gmail; Tue, 05 Mar 2019 14:47:54 -0800 (PST) X-Received: by 2002:a1c:358a:: with SMTP id c132mr450799wma.23.1551826074067; Tue, 05 Mar 2019 14:47:54 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1551826074; cv=none; d=google.com; s=arc-20160816; b=WyDAFymdMDuoNvgeLEmYeRYRKeizf7v6jSX2fFcXcQ/Ew9d7eIKENBjstXihGKPSeQ ter0AiN0x5WeL7IpZzopIQcIgGgGlLLmNmPvZY945jgbbDKpUlhY9rW5gAM2B16rxDxE tzuVEK2s6+4qaS0R8JajRvF85fEQRjKSPZxC18Vx/XgZ0h9I+1Gik8Dt+Hu/xXPsAqv7 Mxl0hRYW3oVWU5tKTBF5N2UKl/ky5DkarZBnXweBZftEXzkE/cuoz0lwuANdjH1y+wrJ QRxJ7i5OUPjg7joRinDITKj0Ir/dLIp2pK9nNuIdUZg4lHTXh3Idt2BfFAHeiP9OOyLF Vl4Q== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:in-reply-to:mime-version:user-agent:date :message-id:from:references:to:subject:dkim-signature; bh=igPU6YKRSZCmbQnx6B38jzXTra0VEbo6Hn1km2+hPME=; b=aTQfB54Enf7pPrT3yVvdjeUBRGw7cHBlMjBOFBVF6mlMjLIG+WaZdNqFZwMTh2tBzc O9QFV53rMRxiBSCjzw941XqHYU4LXX9P2PInyrZ/ZN3gH9Q9DD1P2Q5oyo5au3lzV6MZ 68PzPU5VQuJz8L8K07ttYsXxpRgjkyo1esP8JpDFRdZuykug/gkd1EWd2nN/WYB88ThU lgtPMoL6TVcJ0tWhSfscG3Stc3JQgsj8eyvFqls5YyZqvL3k1/G3/3+ZYRUTf4wolc1d 1NXCVTVe/FfSBASip8O6PS1XiVE2b9MyZrueRAsBYB3yfbBmSFXuR9LqwYZoeRNwlj9I f8Mw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=BjYLQzPA; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::32e as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x32e.google.com (mail-wm1-x32e.google.com. [2a00:1450:4864:20::32e]) by gmr-mx.google.com with ESMTPS id g10si3665wmk.1.2019.03.05.14.47.54 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 05 Mar 2019 14:47:54 -0800 (PST) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::32e as permitted sender) client-ip=2a00:1450:4864:20::32e; Received: by mail-wm1-x32e.google.com with SMTP id o10so3125513wmc.1 for ; Tue, 05 Mar 2019 14:47:54 -0800 (PST) X-Received: by 2002:a1c:5f89:: with SMTP id t131mr502619wmb.46.1551826073239; Tue, 05 Mar 2019 14:47:53 -0800 (PST) Received: from [192.168.0.4] (cpc86229-nott20-2-0-cust356.12-2.cable.virginm.net. [82.7.65.101]) by smtp.gmail.com with ESMTPSA id z15sm16360991wrh.18.2019.03.05.14.47.52 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 05 Mar 2019 14:47:52 -0800 (PST) Subject: Re: [HoTT] Propositional Truncation To: Jean Joseph , Homotopy Type Theory References: <0f5b8d0e-9f1d-47a7-9d39-a9112afb77ea@googlegroups.com> From: Nicolai Kraus Message-ID: Date: Tue, 5 Mar 2019 22:47:51 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.7.0 MIME-Version: 1.0 In-Reply-To: <0f5b8d0e-9f1d-47a7-9d39-a9112afb77ea@googlegroups.com> Content-Type: multipart/alternative; boundary="------------29E36E3D45A04E91A284AAC3" Content-Language: en-US X-Original-Sender: nicolai.kraus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=BjYLQzPA; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::32e as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , This is a multi-part message in MIME format. --------------29E36E3D45A04E91A284AAC3 Content-Type: text/plain; charset="UTF-8"; format=flowed You can't have a function which, for all A, gives you ||A|| -> A. See the exercises 3.11 and 3.12! -- Nicolai On 05/03/19 22:31, Jean Joseph wrote: > Hi, > > From the HoTT book, the truncation of any type A has two constructors: > > 1) for any a : A, there is |a| : ||A|| > 2) for any x,y : ||A||, x = y. > > I get that if A is inhabited, then ||A|| is inhabited by (1). But is > it true that, if ||A|| is inhabited, then A is inhabited? > -- > 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. --------------29E36E3D45A04E91A284AAC3 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable You can't have a function which, for all A, gives you ||A|| -> A. See the exercises 3.11 and 3.12!
-- Nicolai

On 05/03/19 22:31, Jean Joseph wrote:
Hi,

From the HoTT book, the truncation of any type A has two constructors:

1) for any a : A, there is |a| : ||A||
2) for any x,y : ||A||, x =3D y.=C2=A0

I get that if A is inhabited, then ||A|| is inhabited by (1). But is it true that, if ||A|| is inhabited, then A is inhabited?=C2=A0
--
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@googlegroup= s.com.
For more options, visit https://groups.google.com/d/optout.

--
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.
--------------29E36E3D45A04E91A284AAC3--