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-x338.google.com (mail-ot1-x338.google.com [IPv6:2607:f8b0:4864:20::338]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 0f606a2f for ; Tue, 5 Mar 2019 23:07:14 +0000 (UTC) Received: by mail-ot1-x338.google.com with SMTP id s12sf4247088oth.14 for ; Tue, 05 Mar 2019 15:07:13 -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=WZ97+QN7KBIZwa+Yd/aopdBtCb+EhvVsk5A+9/IV2FU=; b=Jz86T51o/N9VY42U+QElw3RxjK4+W7ULYwoYcE9ijrSZEZiwYaL6BmFzUouMGhPjSJ EmXgCXoI6c7NdD1h/oSzDj03R2o/qTkpLU2dmwBaOb4cyq5AOTPKMqNl3ypovfZ9h08J jaMVeKgexsmAp7aD+S7xy4FuIza1uj9n/h7EHvacUYP30nNiwMeEuV93G7CJ6+68hEic Y7SLUmIki/RnEsb6jLGspBDEW3BAci1U8Q22CPvBQ8DF/bHktX16WR6cRIVu6nqgrZ5N AxKelXXOEG1giZrCfoyz+zV1fUd+K1/epPv4L0SFRqFJI0Gzi+1fBAFEFzMt1ivjeIWb 0hnA== 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=WZ97+QN7KBIZwa+Yd/aopdBtCb+EhvVsk5A+9/IV2FU=; b=Y4+aZxe1con1awkltaEezdz7tyI08Y8F0MHLXhsoN1BEjxTcEni49RnhfppdahSWgC JAjiLoFJoV53b4urJH6G+3676VEKZOyPhhL1+37udt8AflVyXA+2jp2xFOXO0czpUtFR 60qPrVNdI/2W43mrFyPGcEr1UAA3lahiq4hwz08XVE0lWCmRVc8Y9Gn4vnYDOSyklyIQ cPWr1m53QtLQN2IV5W9jnf7sVwL7KdY8ZIDoeosqj3U9TI7mnCxIhujdDJu+jOEy2zf5 lLAqmSmLxwZ0CEM/bsTBa9oo/XgZsMUoI/FlYr5+ZLoxas8Ht3ziLgHOfNVdFhgNFoAx TsNw== 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=WZ97+QN7KBIZwa+Yd/aopdBtCb+EhvVsk5A+9/IV2FU=; b=OCcqH8IKxaEt9ifqWh2VupIPSpt9u2O3rE84AZ0UCTO/jf214dHrGyr78ZjxFPsJmf BOJfmo+CMlBnmz/V3PqSKqywqS8wqOCuU//z0XQ5IVWYO/bL3LEy4wgO5oGcvqzAq0+j r1yVLax+5ESd4ioNARlEsWhvAsI28ppcYDrulhkF1Jr1DJAZ7HxezTQ9X/1iZ4dfRxt6 OYCtmasA2ppzngiW6SdXDNeokH5xfbTAjHXq9BrQq0NN3n16H0qoJJzK6Q/uRYZ/b7r5 t0+MFGSuxoT3iI/3BPO5Llco4btSinM9OmYFOYTjG8ibkfpillRg/Wppkr8mDP0LDJsg M8MA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUxqgdq7QXnst6TqzVa+gSl1X9AJKwmBtS2bKOAqaplWVLK7gaQ SqNlTOu7pa0uZqkEDV0pz4U= X-Google-Smtp-Source: APXvYqz259BcxkJW9WdpFYLPl8toLXg1/5d8qXCoUptYKRpyunilgIXutOwKysESTYSTLSjRzO1EFw== X-Received: by 2002:aca:3608:: with SMTP id d8mr569259oia.104.1551827232775; Tue, 05 Mar 2019 15:07:12 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:3bb6:: with SMTP id k51ls1125449otc.9.gmail; Tue, 05 Mar 2019 15:07:12 -0800 (PST) X-Received: by 2002:a05:6830:1547:: with SMTP id l7mr2457660otp.196.1551827231933; Tue, 05 Mar 2019 15:07:11 -0800 (PST) Date: Tue, 5 Mar 2019 15:07:11 -0800 (PST) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <12cd6b73-7ca6-481c-9503-250af28b8113@googlegroups.com> In-Reply-To: References: <0f5b8d0e-9f1d-47a7-9d39-a9112afb77ea@googlegroups.com> Subject: Re: [HoTT] Propositional Truncation MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_23_1510081630.1551827231405" X-Original-Sender: escardo.martin@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_23_1510081630.1551827231405 Content-Type: multipart/alternative; boundary="----=_Part_24_1849414601.1551827231405" ------=_Part_24_1849414601.1551827231405 Content-Type: text/plain; charset="UTF-8" Or you can read the paper https://lmcs.episciences.org/3217/ regarding what Nicolai said. Moreover, in the HoTT book, it is shown that if || X||->X holds for all X, then univalence can't hold. (It is global choice, which can't be invariant under equivalence.) The above paper shows that unrestricted ||X||->X it gives excluded middle. However, for a lot of kinds of types one can show that ||X||->X does hold. For example, if they have a constant endo-function. Moreover, for any type X, the availability of ||X||->X is logically equivalent to the availability of a constant map X->X (before we know whether X has a point or not, in which case the availability of a constant endo-map is trivial). Martin On Tuesday, 5 March 2019 22:47:55 UTC, Nicolai Kraus wrote: > > 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. ------=_Part_24_1849414601.1551827231405 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Or you can read the paper=C2=A0https://lmcs.episciences.or= g/3217/ regarding what Nicolai said.

Moreover, in the Ho= TT book, it is shown that if || X||->X holds for all X, then univalence = can't hold. (It is global choice, which can't be invariant under eq= uivalence.)

The above paper shows that unrestricte= d ||X||->X it gives excluded middle.=C2=A0

Howe= ver, for a lot of kinds of types one can show that ||X||->X does hold. F= or example, if they have a constant endo-function. Moreover, for any type X= , the availability of ||X||->X is logically equivalent to the availabili= ty of a constant map X->X (before we know whether X has a point or not, = in which case the availability of a constant endo-map is trivial).

Martin

On Tuesday, 5 March 2019 22:47:55 UTC, Nicol= ai Kraus wrote:
=20 =20 =20
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@googlegroups.com.=
For more options, visit https://groups.googl= e.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.
------=_Part_24_1849414601.1551827231405-- ------=_Part_23_1510081630.1551827231405--