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-ot1-x33b.google.com (mail-ot1-x33b.google.com [IPv6:2607:f8b0:4864:20::33b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2464ec5c for ; Tue, 5 Mar 2019 22:31:59 +0000 (UTC) Received: by mail-ot1-x33b.google.com with SMTP id e25sf4214478otp.0 for ; Tue, 05 Mar 2019 14:31:59 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=l22UQZ4ImDWRKGiGEp4k3LrPqSH5weliD2QwWYs8kAU=; b=TSveWs2XDb7bfRCKy3zg9DhyaagpdHHhUnK5Rb8ucW2vTJ3m6Ve/o+M+nIxZA5hM56 n9A12qniveO/shtdwDrYZdW8KL6ntENXxArndmr4Seaelg7kkhfTiMy43MfRIs8EgaCN ydU2MJ4kFhLZUZVN1gJZJHlOlzdKeZ0ogPeODXbktq0WM+4U+xAH9pyfk2j0I3btvYXB qhuvnGhpVwcEtkivSqrw1BYmi+A1El30PKxwt9dlieCWzr8WcW3OyyvqzaIJ6Vz6a9+u oMHb+yZtn1+XmxmLCxP44AaBwCQ0dMQyBKgTAH9O13QKjtmX4eUaRxogbMx08N7K+PGJ DepA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=l22UQZ4ImDWRKGiGEp4k3LrPqSH5weliD2QwWYs8kAU=; b=VsrTztrYUTnco+tMTfLcyT4Oj4ro19u8DOp3DzJSsFCmZldgViBZ7H1yhrdpoehSMy GRHPykgCbhAsks6TFDRNK5xGw8MEUbhdFBhmGifN+9AP+HwIPiAL9+SGcMhCtMzuy6RQ Ojt7FVfX7r+OwQAgq16rKEMxkYdmeBHL8Qjg+1J+Au7E2AiuPfrRE+HY68TPaN3N4fxj sXolbKHa5vQYNOiz+Gz0FIz8Eg/xrh2fVRWFg+ZWU3Ok1BRwAA8BV4ckwhTOusYHme/F wYF7WWWaaurRVxW8Ez+vMbo2ucUoAPkHPptDBaWShDxxJCemGnWdFcYmhAaa7Q+ayOc3 EC8w== 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: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=l22UQZ4ImDWRKGiGEp4k3LrPqSH5weliD2QwWYs8kAU=; b=S4kWDpHvCGIqlSIYteb5mGQX8mekXcDhYBzXQAg4zRgi0zO2dEuNY/3b3gKzb4ixvd zlcUYE5n2LnMl5PXL6H0SHM1KW7XNB7sUkdNFrHZHCLxMqjAKjC9A6tUgzE8X2PlKQnY Nly6/ul3QpI3pHvPTgRB/Vle7Xk0yE2r/yqVy8HZueqbg3SkCfDDy2miwH52zgAK33mF y/5nJ8UU8nIMkgN5nSQQEUtWFKTSYm4kgumCsO5g7aLUk/kQkvKVA+g3PtG+V2uzuegS E0hktdbeULtbUy+rXbfYPxTVuEB9dYmCiJJawUfHNVEjsXbBN92z8S/qAMpwV4X3EcvD KmaA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVgzzDNpqxVPLsIBr6mmF3ddWaCQ6GkHvJwEgaxagLwselaYNOT n902RYRcHxsNuTTprRxvcXQ= X-Google-Smtp-Source: APXvYqwgiziSPyFPn9fiAHEGJyn2XuTnuRGGPsnZXp39+lCf3DfsSd+asWhgdIoyuVoRO7Y/kn98EQ== X-Received: by 2002:aca:355:: with SMTP id 82mr548031oid.30.1551825118058; Tue, 05 Mar 2019 14:31:58 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:5c05:: with SMTP id o5ls1194101otk.6.gmail; Tue, 05 Mar 2019 14:31:57 -0800 (PST) X-Received: by 2002:a05:6830:1317:: with SMTP id p23mr2526479otq.55.1551825117565; Tue, 05 Mar 2019 14:31:57 -0800 (PST) Date: Tue, 5 Mar 2019 14:31:56 -0800 (PST) From: Jean Joseph To: Homotopy Type Theory Message-Id: <0f5b8d0e-9f1d-47a7-9d39-a9112afb77ea@googlegroups.com> Subject: [HoTT] Propositional Truncation MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_10_701954295.1551825116924" X-Original-Sender: jsjean00@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_10_701954295.1551825116924 Content-Type: multipart/alternative; boundary="----=_Part_11_449209496.1551825116924" ------=_Part_11_449209496.1551825116924 Content-Type: text/plain; charset="UTF-8" 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. ------=_Part_11_449209496.1551825116924 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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 &= 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_11_449209496.1551825116924-- ------=_Part_10_701954295.1551825116924--