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-ot1-x33a.google.com (mail-ot1-x33a.google.com [IPv6:2607:f8b0:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8415da1e for ; Thu, 7 Mar 2019 14:10:57 +0000 (UTC) Received: by mail-ot1-x33a.google.com with SMTP id e25sf7115460otp.0 for ; Thu, 07 Mar 2019 06:10:57 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1551967855; cv=pass; d=google.com; s=arc-20160816; b=xOWeJQIbXaYEAvoOwVWIiE1/e7GZ/c/uxaEmy2blzO2b64poHMVUPvt9o3faZcXowl JfZQiVkpRWlKcD/8gRUAdZqUhtXDQiR7qUug+GYWTW/w+EAwET6QmV+w8BYF30HlG/CB SW/pb266KSJQ6VmmSTBRvbPB4F+pmKuOh0tX14AkyGgS5bMuJMST5iwxdlW8mMs50sua AEs7TpQG5eqEU4oaSM1o4IVnz72oWZM1M4u3sO9XdBZBWmxa6Bf4NXOpt1Md++uewkzA QtqhKtrGNzUBbnhGhLLUP3LrBYGTEvIa4UQ5EscxRq60F+vHA1gfBoPmTTzGiJYcJfwY +6Ew== 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:mime-version:content-transfer-encoding :content-id:content-language:accept-language:in-reply-to:references :message-id:date:thread-index:thread-topic:subject:cc:to:from:sender :dkim-signature; bh=mBA/db1z5vO9jhFjvak+EhdqyTduJTt+wlUOw3T+dts=; b=vPdTgsTOtj/vdNjK3cWLir3jb9J8IUOT8KkNWnR37axn7xc2fLYc+hEnquSCIFvn/5 U6gZq6lPkpyjTMSCt2dttgxT/sI+0HMs9ouaKhEmqh8F+BZQJmafV0T7HhaUo7qzcxl/ Q07JQU0IzUvK5W1HzG0EJFBK1R3TUQxAvSOELSlgEtsYzLKb3jYUF4nGD+g6CVHnuRQr dHZjY+KmtHaf1RISmgNvrP2fV4GAALLVlR2ldaHA+ZciM96Hsen6kUzqYBoSDmRamDTg A4Nt10uiLyaDigkPm56mZIxwLXh1YY2ElxAIJWpsV6P36ApxXXkoO4bv/a2rbvnTn4bR PR0g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector1 header.b=U8vJuEnd; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.70.125 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:content-id :content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=mBA/db1z5vO9jhFjvak+EhdqyTduJTt+wlUOw3T+dts=; b=MGDB3O2DXLCiRTFxIg7A1yHaKcOOm/GErcc5Glwzb6nZzfBNgrcm/ccvLk7qD5uRaP HiTngh6JDv07JZ/rz7Co0z5d7Syu7kFC4Ik1WomAqa6Q0NQXQV7jNoIBVS1EAERQygP3 O963rsDCcCk8VBZQxpv2uJXJG8E3ATKGmzZ8A1strcAKpN8yewlbQIhP13WpJZLl+CaG HbV63cMrAsYarf3qL7VzQJANfhQce9y7HR7Ae1Br6f1nvD5P8bIyyosigq95Ala6spaa LF3bIOEliseDTmeUPI68uAyBzjpR9ia803Ff73upbxdGJVDUw2Y6PA76Pqvxv3og7iOu ggKg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:content-id:content-transfer-encoding:mime-version :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=mBA/db1z5vO9jhFjvak+EhdqyTduJTt+wlUOw3T+dts=; b=jBLn3FB6sJ2bo8XLKi40QUgbOnABWkjxYLBLRo7btQfTK/HF3Ey2tdH/jJGdZGE3Xb v74jyytnnYzTNtjjy3cJcrsxTz5zQJaQ8Jvj+qPSBvb1xlraTISH0iaomEPDLD6H58ms rxNm9nksEnHWg+DqiwTk8qab/1jJJC73LnJyOpaQowid7tcrjblz43mdnh9G8PXjcRr3 WgC28eYm/udmfIX8MjpOZbYTB69tQ2G09KXrWJ3kh/x/cTZA1pH9k24sVOUIyscbfRw7 0ENP4UNNyw8kUjs3ae+71fv0/cqQ7HzxmQ164bsbDTvQWHLrN6AvMYl+ARW6VXT4QUUr +ecw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWpk95XH23U0Q5S0xlBY7egi6zOrGi4h0/acagkKKQryDmprhCj vMKkZH5bNMMRX4iaHxZ4vxA= X-Google-Smtp-Source: APXvYqxoE4Lno3+H3eN0hM8RUCLeok/AhcjrRFmBEfo37CKwDY3m2uTeGYKvvhheJcIV+zrEp+VWdA== X-Received: by 2002:aca:3e8a:: with SMTP id l132mr5179253oia.107.1551967855710; Thu, 07 Mar 2019 06:10:55 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:2c04:: with SMTP id f4ls1940792otb.1.gmail; Thu, 07 Mar 2019 06:10:55 -0800 (PST) X-Received: by 2002:a9d:4913:: with SMTP id e19mr7208685otf.67.1551967855399; Thu, 07 Mar 2019 06:10:55 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1551967855; cv=none; d=google.com; s=arc-20160816; b=LHEFtu0+IOiHYkAaQgHjWxm5kozgy/fAZTaFhHGsI3w+bjWBdpJ1Fz1FyPaKDTMY2k t8v6+3HkXAI837VqWxOyv/EtCXqT+jbAJHO68XsUsT7Dw6nT/Abcw3Zzgb6zX/18lyoP i0nKAfI01B/Ix7fmrTNqGrd11qtOLGOOWHVt5JTdHWK634C72sI/i6grswtYp5495XGG t4cKejZkhFU7DGCMP5gQ6K7XMYic5vPyPfUXm7aEcMvE0/Bnv48/ulPk16U10eDKoxep z8WvokGbH+1HdMeUKSdlvK0nj/ainNWNaJDcgZdjmLndGrk+turZNpT/ZlpCRP0V20na whTg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:dkim-signature; bh=b+uAvWT2IeCZdgYxBriy/ZEN83xn8X3OfOYJFsKMEJE=; b=su1XuDPbQ43BmCkwQMQSGnPD89RPCKNUWTeagit386wFeHOIMYuL3uUGmZOaIWEjAg zBfRxnFjANK1xlXDctmSRIkjPGo0mcYtXangXKluWWtMzNSckM+OGvJ7xgZ9H6IOdmte zQFNsfjbUG2CNzuwS4sewESM+5SZ+6wQfBWgyrEK5+RStfWzoedhnQKVBzL4LDE4Oa22 DBUlnSe1umC7VfSEcZxCZ7Ll+zEbgyjoCTwNmQd1BdJNsW1YQ43sNrUI/4O5BzaFCeF+ JzVnF2g2VxSTwS4Qwzx4gDzT8lo6w4ULiE+69Gg+c2r3AH1bkdB1RaiKPqHvEc1mDKgZ FDTg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector1 header.b=U8vJuEnd; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.70.125 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu Received: from NAM04-SN1-obe.outbound.protection.outlook.com (mail-eopbgr700125.outbound.protection.outlook.com. [40.107.70.125]) by gmr-mx.google.com with ESMTPS id l26si290333otf.0.2019.03.07.06.10.55 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Thu, 07 Mar 2019 06:10:55 -0800 (PST) Received-SPF: pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.70.125 as permitted sender) client-ip=40.107.70.125; Received: from BN3PR04MB2195.namprd04.prod.outlook.com (10.167.4.13) by BN3PR04MB2289.namprd04.prod.outlook.com (10.167.2.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1686.18; Thu, 7 Mar 2019 14:10:53 +0000 Received: from BN3PR04MB2195.namprd04.prod.outlook.com ([fe80::1054:134d:6696:2d12]) by BN3PR04MB2195.namprd04.prod.outlook.com ([fe80::1054:134d:6696:2d12%3]) with mapi id 15.20.1665.020; Thu, 7 Mar 2019 14:10:53 +0000 From: "Licata, Dan" To: =?utf-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= CC: Homotopy Type Theory Subject: Re: [HoTT] Propositional Truncation Thread-Topic: [HoTT] Propositional Truncation Thread-Index: AQHU06NFzBcK2A371Uil15CpceOYdKX9o6aAgAAFZ4CAAo7QgA== Date: Thu, 7 Mar 2019 14:10:53 +0000 Message-ID: References: <0f5b8d0e-9f1d-47a7-9d39-a9112afb77ea@googlegroups.com> <12cd6b73-7ca6-481c-9503-250af28b8113@googlegroups.com> In-Reply-To: <12cd6b73-7ca6-481c-9503-250af28b8113@googlegroups.com> Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [24.60.108.192] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 26d8cd43-ec9a-46ce-4171-08d6a306b613 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600127)(711020)(4605104)(2017052603328)(7153060)(7193020);SRVR:BN3PR04MB2289; x-ms-traffictypediagnostic: BN3PR04MB2289: x-ms-exchange-purlcount: 2 x-microsoft-exchange-diagnostics: =?utf-8?B?MTtCTjNQUjA0TUIyMjg5OzIzOjZEblNDWkNnUER4TFppZUljQTRDQm5oU3Ey?= =?utf-8?B?dVh0UUFmMDBLOFVkOGFhdWQ3cThLUlhWUmpuSGtyQU5mNzRYYWdZS1NOR0R1?= =?utf-8?B?aDRvTXQ5NmNxSFkzbWhtWXUxa2hmN3RnSFJhcXdLdlVudTZnMG52RTg1YzI3?= =?utf-8?B?THdZc1NDenRaVkxuRWc4R3ZMQ1ZuY3A3ZWhkelo0R3F5NnFoUkZiV1hrTnJU?= =?utf-8?B?YlI0NEtOVWRPenpUWnRmRnlWN1JKMFNXU2E5b282T0dTTUNRbzdaSmwycEQy?= =?utf-8?B?ekl6UUxBbHNlM3hxYnlWU0hlNFU0NFo2NU1xQkprOTZlcmM3OXM1SUwzNDBS?= =?utf-8?B?WVRVQWZqeGVySnc3dzM4L1k2V3l4ZGt0ZWNaaE9oNnlWSXpQQWFmMndkdE40?= =?utf-8?B?T283VUpzTTVwQ0RyNTBFVE1mOGpGRm1xQzNGdHFhOGt3cEN4Y0o2cmowVkU3?= =?utf-8?B?bGtSdnBEMWNPUWIzRGlFZHhJWTQ2cDFxVk9JY0NIODlHMEZHOXBxcUIzQ3V3?= =?utf-8?B?NUQreXk0RUorU1BSd1g0a050bTBwWG82SWwrUUZjM0N6RGNxY1hlay9CRG9w?= =?utf-8?B?VU5GZWZBT01KeDU3Z0J3WGxPTE5CQ04xVWtucitkcTJOUUQ5ZDhVL01wNFcy?= =?utf-8?B?NmFlTWQyK0lDa2dTTVdKYnVQZlIxcHZSeE1tdGpUQ0hXR2ttUEFSbzhvQUt5?= =?utf-8?B?RHZFSFZ6SW5CbDQzQXU2YUE5a2lLMVVzRFgzcUExd2xsV0pyQjBiaitIZnRz?= =?utf-8?B?bmRDK3UzenExWXFWTGFUK1VqVXlBeWRtc2ZQK3A1am9pS0hiVVp0dFRrZXRt?= =?utf-8?B?MHUwM2tFYUFnbHNVbU8wZ1YwYm5SdmRrbVlUajBqN254Q2ZidHFMZnhuRE1Z?= =?utf-8?B?clBCZE52Yi9LcmlsWnI3elFrQzZMTSs2NHRHYU1JaWpVcnlrT3h6OER2NklU?= =?utf-8?B?cFNtNFpmZ3U2bEtyUkVBbEh2dEhQaEloRUIyaG1lMUE2TnVDTXBnQi9BemNr?= =?utf-8?B?a2ZvcndKWVdXdFpWSElGMTFBVWJxekpnanlFV1NqbkZaZ3Fvclo1aVNwMUZQ?= =?utf-8?B?bU84d1d6NHI5enJNc05qemM5T2pabUVra2JvUmxvZVl6c3ZNSm9KUERrTHlV?= =?utf-8?B?MW1LMjRsMmdZQm5lUGZvdmtiaXFJWEVSR2FCaVh4Q3BhdlMrQm1IbjA5aUw5?= =?utf-8?B?MUU0VDFDOEIvd09LTmQzRk0wb2h6MmNlT2FzTXJnek9jLzJzV29NWTV4d2Vo?= =?utf-8?B?ME5PMUo2MWZPaVhoNWZGaGY2V0o2Tm1pZHdjU29mU3JmK0ZNUGFmc1A3U2w4?= =?utf-8?B?SHpQYzN4eVdvUm9sYjQ3MWMreTdYa1YvMjhETUpxbEhFNFdxbnQ3dlZZUVdv?= =?utf-8?B?eXNKeGgzVWdiSW00WTZxZk10a1VHbXFNQVhaZUJCOVczNnZUOW1KNlhHSmFt?= =?utf-8?B?ODlKOGt2M1pNU1NoSzhVNzVtN0ZzMXVXR3pLREZ1NWhEdmxBOXZXMThQNUpr?= =?utf-8?B?c2EyazFKL0oyUmd0d2JyN0hWNXVrcEVrOWRIU2xubkN2UnR2eUQvT29XRHNC?= =?utf-8?B?VERqM1NpTWhsQ2VHRk5JSzhtLyt6ckR3WEs5UDN5bEFPbjUwMEg4Sll5ZWJU?= =?utf-8?B?NnVOdDBCVVpuMUFvMjF5UVNmaE41dTlnVUZUZXdPOG4zK0JUaDNraFhLVmpR?= =?utf-8?B?ZXJGMFNIWUYyYUdvc1ZzeEtXSmRiZ1l4VEluRUJjNTRhVm1jdDVoZmhwUTlF?= =?utf-8?B?cUYzeVRFRUliWlErR084NzhoYUcyS3NzQWdsYzFBRWpDYmxVcW03UHVBMXJT?= =?utf-8?B?bjU1RXZ2cmUwUzdhNHEvTHJ0d2NrSUFlcG40c01kb3BnY3c9PQ==?= x-microsoft-antispam-prvs: x-forefront-prvs: 096943F07A x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(376002)(136003)(396003)(39850400004)(346002)(189003)(199004)(5660300002)(6116002)(76176011)(8676002)(36756003)(53936002)(81156014)(305945005)(3846002)(81166006)(97736004)(966005)(102836004)(256004)(26005)(33656002)(186003)(6506007)(53546011)(8936002)(478600001)(4326008)(86362001)(2906002)(71190400001)(75432002)(66574012)(71200400001)(88552002)(68736007)(446003)(11346002)(99286004)(486006)(2616005)(83716004)(66066001)(106356001)(229853002)(105586002)(7736002)(6436002)(6306002)(786003)(316002)(6246003)(6512007)(82746002)(6916009)(14454004)(6486002)(25786009)(476003);DIR:OUT;SFP:1102;SCL:1;SRVR:BN3PR04MB2289;H:BN3PR04MB2195.namprd04.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;MX:1;A:1; received-spf: None (protection.outlook.com: wesleyan.edu does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: Wm/kLxc3rtaqx2KnfFthyNg8j2Mf9AgSZXsi4huC4ulIqkz42+36+tmUjVnNsGJ/wJs/6VZSf4bX2yoBtLo9zwVjokYkD7AZgc+Or3y7jovYb50QtqcEeBZqneIrK2GZciBb0462i08FvOKga1InH7KyKFFlRXH46rZy0B2EwDMsDGDTOb4oQ/Y6yacvIrDep07DjQS592Q49p/TYCWh7FhazjNQDpSYSyXPTkvrn0l4n7cAxsXPcnbztEao4y4XUuSMgd5uCyRiTzP16pMKVAqFnpFWhpGXJkGpmdUK1PGZ1QAKYvtTX+iHWRQJyo6JlvwntYIo2if5136XrfOiiqtnJ+Gm/NSxWRodsYXD4DTRNw6kLJ/M5neCEtftWeLQi+mhFQfN8M0JIrBrLxMlIO97wGv7tmAA5c0KoPFbhGs= Content-Type: text/plain; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: wesleyan.edu X-MS-Exchange-CrossTenant-Network-Message-Id: 26d8cd43-ec9a-46ce-4171-08d6a306b613 X-MS-Exchange-CrossTenant-originalarrivaltime: 07 Mar 2019 14:10:53.7128 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: a9fd6c79-6d71-49f3-9111-0c8e591dc3d1 X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-Transport-CrossTenantHeadersStamped: BN3PR04MB2289 X-Original-Sender: dlicata@wesleyan.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector1 header.b=U8vJuEnd; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.70.125 as permitted sender) smtp.mailfrom=dlicata@wesleyan.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: , Just in case anyone reading this thread later is confused about a more begi= nner point than the ones Nicolai and Martin made, one possible stumbling bl= ock here is that, if someone means =E2=80=9Cis inhabited=E2=80=9D in an ext= ernal sense (there is a closed term of that type), then the answer is yes (= at least in some models): if ||A|| is inhabited then A is inhabited. For e= xample, in cubical models with canonicity, it is true that a closed term of= type ||A|| evaluates to a value that has as a subterm a closed term of typ= e A (the other values of ||A|| are some =E2=80=9Cformal compositions=E2=80= =9D of values of ||A||, but there has to be an |a| in there at the base cas= e). This is consistent with what Martin and Nicolai said because =E2=80=9C= if A is inhabited then B is inhabited=E2=80=9D (in this external sense) doe= sn=E2=80=99t necessarily mean there is a map A -> B internally. =20 -Dan > On Mar 5, 2019, at 6:07 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: >=20 > Or you can read the paper https://lmcs.episciences.org/3217/ regarding wh= at Nicolai said. >=20 > 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 invarian= t under equivalence.) >=20 > The above paper shows that unrestricted ||X||->X it gives excluded middle= .=20 >=20 > 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 typ= e 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). >=20 > Martin >=20 > 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 >=20 > On 05/03/19 22:31, Jean Joseph wrote: >> Hi, >>=20 >> From the HoTT book, the truncation of any type A has two constructors: >>=20 >> 1) for any a : A, there is |a| : ||A|| >> 2) for any x,y : ||A||, x =3D y.=20 >>=20 >> 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?=20 >> --=20 >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >=20 >=20 > --=20 > 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. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.