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-yw1-xc3e.google.com (mail-yw1-xc3e.google.com [IPv6:2607:f8b0:4864:20::c3e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 7c916738 for ; Thu, 7 Mar 2019 22:51:20 +0000 (UTC) Received: by mail-yw1-xc3e.google.com with SMTP id c74sf25333789ywc.9 for ; Thu, 07 Mar 2019 14:51:20 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1551999079; cv=pass; d=google.com; s=arc-20160816; b=Ca3Ys/IwTeKMjukPzgTHT9rf8rt4Mf05qu3jds8srWBzBnPFzCAi7rp72ANRbjZ587 8m6GN9QloXzJsmW/F37I7kRdp1WIhDveAju92pv6FDm6f8xEB+NUIAp0LGYP6MWRszV4 o1O4dDiz3R+zef+xfQGIseDFxrX2z5ZVBMYZ8BcjeF3lBErxnjIbtje1931WEv/JudDo 6lhJttFAyIMd+2XBJ9X70ukIaV3q/QRrTT2A11WjJviBjtnphMhBbZsuXLF7FaQXZph6 gim9RbqMdMkEyYM+ESKbFpO5ajhaUu9WxCCjw0JS7BgukWLSLSNlxjL4CT3wFL9bt4p1 1ozA== 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=nrjprOC+zmTxG5Gs4fGHfq39M3BRbsX6hbL47f34ksY=; b=zt38K4eXiua8vFmQ70h6rh/Tvp2Sx9sWmmFena8ZLbG5+NYGAqiZKM82m0RkCT05Z0 fjwVn/I1xKfDFupasKBU6XRifFI/auKbpEsIWAayEKBtMkfVQL0lq1jPnDt44n3OEuqG mwxBAAHjva2QcqGT9H57ns33HrKOs/ubmtsDFfYwGB6Sts7Co2bR8ezuRV17fPbacJrY VDGy/Q73lw8jzQTLivkowNMMDWMcSE1TTcPqhaAU+DAzkZBtR9pUJgg/NTOoqFwizrHs vKC13NDmPl6M1cjQ7CPlfDsRkhUlWTNY5iFuRdjV/EoM6CzmQbmEVIlY/ctoPgi3RYXe Ox5g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector1 header.b=DNPy2DFZ; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.75.121 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=nrjprOC+zmTxG5Gs4fGHfq39M3BRbsX6hbL47f34ksY=; b=nO/VzZaWUok1WWIbl4vPZ5gF8J7/DixKONae6O/8QLIxLq4IGRkyCPrbmeYUqxiDY1 GGe7epdhQh9lfsFeXN6f45nx7/V2X04LZJ4Sn+Qd06tlIYthxSGF9VLewVv6qRZTQ57B pXH0N55vs3DkkQc5wMvzb73mLtj2DBp9+mNtiURu1t9+SZWWQayon+k/5RKifuGBnH9t zq7FGeM6xMEipoqjpZiBzbJh8uyySU2k1n2ElH7O31sYfoutI16RXYDNv5YunHRxaSW4 Lclr7EM2QtVsUpZv10pLhwIGjKU4lNuMvI3WcI+RreuHlQNjjCFPE0RtIG+gxsyxoqwE 2v1w== 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=nrjprOC+zmTxG5Gs4fGHfq39M3BRbsX6hbL47f34ksY=; b=Nfgr2HzDyvVjJXRN2065dIPvBSbcOJhB2YsK8jhuIPjLU4LeqoEQbpSki2AouDEbD0 NXVLVt72SZwILMLpa9a5UfVVovaPZltylR6U9lhaFDfZEmlumQ271TKYqRu+A0KmRRWS DTfGscWgSixgOp/wHMeySJp6qPSAPwM7TLXTe4jKBR+6NB2/C66JB3y9QmOaddXwup2N ccsq4RGJ6bi7ubkgwmatVphBN6JUj+EHymQPArKqKvrR78UJPmTqevPfdRmlBNJAqcXu gZHvuyt8Seu5Qs4RgfLcB29P6buUG8DsNdUp2yQj4+hfmolWLaQ/3aao7W8SUEZOz9VA T7Ag== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAX3EIgVh4e6Tl5Xv2Etfra7MVaTvXP9/JXiLH/HoDGVwaRs0nLM 33wQv+r35Vg0P413gKsRGdo= X-Google-Smtp-Source: APXvYqxdb4QCPfPZKQEM9wAbuoh8eF06tO2bHH+hG2y+qd/4PbLnwr7ROBocsOlBV/p3dTbQR4OLaA== X-Received: by 2002:a81:346:: with SMTP id 67mr12229406ywd.128.1551999079666; Thu, 07 Mar 2019 14:51:19 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:3888:: with SMTP id f130ls2491647yba.5.gmail; Thu, 07 Mar 2019 14:51:19 -0800 (PST) X-Received: by 2002:a25:ae96:: with SMTP id b22mr4483560ybj.94.1551999079329; Thu, 07 Mar 2019 14:51:19 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1551999079; cv=none; d=google.com; s=arc-20160816; b=NBIk6s5DGyZFcTK4oKyNMPHAbTN/ajj2Lb4tHLMRSpSoXQylwBwUR4e7pfxtuGdl7U YzjMGx8uPYzo2zk1O+oFf0vsKMhlb22nyDus1OKppZYv0xchIy10WcBhzGVUbINuUUEp 5JXsbfZ7rhVYbw7LTxIkDsW1QTQHXgjkdta9jHXPuuJ8r/B8dA1AqMrLX+XscyQCUuDu Fn9Au8cDrZBMhNYg+8O/ySZqp3IZUCGch19jVhqhmy9w6AyNlP801WK8uhN08Jj74F/N wdWL50PB7RDZikokHbcC2reaON+F1yL3KexRs1lO/e6ORgJix/DJhLxfRw510rlvj667 VSqA== 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=/TS4mpsfUUIGslVoFncFI3ZUGZ9AQ/vjujPiBKPLRc4=; b=oql3XIbnxONjbW8AXMUqT1EDusEn9zsuNJR5axjJyWxRUz0ftCEX4PzO6JftS5wjbR sxUvaIFCdii1ITy2CdExDVvKB/x5LjoU2aML+JZrMWr4AhckcYDWF1whZ1FmG3JHifA0 8hPOzCYT2ZHq7VPH5zfSbAWKkspD6QYbIrm+BVixiZK9iexpk5I8SAvNi+kc5xuZ8Qhw GE2rl6uMkJaJlD3tjcNvTMHjaMJlQ9yajBpky35j34efGcUvV02K5632ufoVo9FN0Jnb MBsFEi4gWkVVv35IUAf6ZRLdJRaLGMrqFVEnhK5/p8j3GSNumM7xn5XNXeet9H3SRXlf G0iQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector1 header.b=DNPy2DFZ; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.75.121 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu Received: from NAM02-BL2-obe.outbound.protection.outlook.com (mail-eopbgr750121.outbound.protection.outlook.com. [40.107.75.121]) by gmr-mx.google.com with ESMTPS id k62si311307ybb.4.2019.03.07.14.51.19 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Thu, 07 Mar 2019 14:51:19 -0800 (PST) Received-SPF: pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.75.121 as permitted sender) client-ip=40.107.75.121; Received: from BN3PR04MB2195.namprd04.prod.outlook.com (10.167.4.13) by BN3PR04MB2324.namprd04.prod.outlook.com (10.174.64.141) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1665.19; Thu, 7 Mar 2019 22:51:17 +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 22:51:17 +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: AQHU06NFzBcK2A371Uil15CpceOYdKX9o6aAgAAFZ4CAAo7QgIAAIy+AgABdtwCAAA2zAIAAAs4A Date: Thu, 7 Mar 2019 22:51:17 +0000 Message-ID: <98CB1099-377A-4A5F-94F2-B33C36D577B0@wesleyan.edu> References: <0f5b8d0e-9f1d-47a7-9d39-a9112afb77ea@googlegroups.com> <12cd6b73-7ca6-481c-9503-250af28b8113@googlegroups.com> <30ae0dc4-cef2-46ad-a280-bdf617a0db4e@googlegroups.com> <9fbd1c51-139e-4657-980a-2264a8f9ff92@googlegroups.com> <5f7932a1-417b-42be-9d63-300dddc83037@googlegroups.com> In-Reply-To: <5f7932a1-417b-42be-9d63-300dddc83037@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: 6c538615-13d2-4126-55a7-08d6a34f68ed x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600127)(711020)(4605104)(2017052603328)(7153060)(7193020);SRVR:BN3PR04MB2324; x-ms-traffictypediagnostic: BN3PR04MB2324: x-ms-exchange-purlcount: 4 x-microsoft-exchange-diagnostics: =?utf-8?B?MTtCTjNQUjA0TUIyMzI0OzIzOktxUVJNVUVqdzF5MThiZ3BJRUZlOXZpMEF5?= =?utf-8?B?NTlRRnhvMlhhU1psTEpQNmluMVJ5OFFLaEFzYW5KUHpOcE9rK1kzSEVpYmtV?= =?utf-8?B?OTlsTVF1cHBBUnBoeWhhU24zWE9lY0gwcmNqbTBHNXBOTFB0UVJvY3N2SkdX?= =?utf-8?B?S1cwcC9hcW0rSkhlWnppZzJGcjZPN2pJT0hSbk5sODFKei8wR0tMbk1weVln?= =?utf-8?B?aFoxZDlUTGsvYkRreTljdWJWMTFIMldpNndGdzErZUkxb3JINExlcGRMclZa?= =?utf-8?B?UzlnWG5CcWpuTUFpS3BIcExodUcxTmxuR0M0dDZZS1BveDlUN0xKbjBDT2I0?= =?utf-8?B?TU5icTlPTVlFN1BVdnRuYUpxM2dXcXpSNFFNcjFOY015V010TUpSUjh5aFM4?= =?utf-8?B?ODJRVGdjWFNlaU1xNEpJcjd3aDZ0Ymk4NkJzRU9XWlFhREk2a1Aza0RSWmNR?= =?utf-8?B?Tit0MzYzS3QrenRGMkZqK29IUGVDTHpWL3Q0UkczOVRqRTQ2Q3c5VkFZaVN0?= =?utf-8?B?SEhPQWhSVVUvcW9scjNuWTNmRzl1RTdRMEhLMWpoMjZrbjVpeUJGRFdqTG5Y?= =?utf-8?B?K013TXFwL2haVFpkQjZFV2gyRlRUSGovRDJWbXBWNHNtOFBDbGNtMnhQMUxR?= =?utf-8?B?SlJVREsxejhieW1NRjZ2WkwrblBuNjltREVyVnNYWDNkMUgxMDE3Q21ycjlp?= =?utf-8?B?N0wyLzQyRmVuWlNJcTg3bEFqdGtRc1M0eDNhTncrRS9MZ01uWUZiUmc2YlFw?= =?utf-8?B?cEEwSFR0N1NDME5WYkV3R0NXRGF4a1lrM0ZmNzd5NzFpM2FtSjBYN0t4WjFQ?= =?utf-8?B?WVIwNC9FZXA1WjE2RkJhSE8rcXVyV0F5bzM5ZHVaK0VvZEFnQVZ5STNxUEZk?= =?utf-8?B?Tk1vWWpTOWhTTDhrMlhhUk96dGdkZ0xsZlRPaU1peHFkZUo5R2RqY2piQ2hX?= =?utf-8?B?OHYrTlJxajgwZmtKU05CV0ZzbGdyRXZlK1BaU2QxWXQ0bHpTNjBUMkVOcnFs?= =?utf-8?B?QnI2SzRFNmdoSExjZU5zeVp6RzRQaDM0V2FTUERtdmdVU0llWjhTT1I5OVlZ?= =?utf-8?B?Tk1XVVRRNElDQk9zZ0xVeEtDUTMxa1REQThJVU1hVWdBY0tsenhRSHpIVEt1?= =?utf-8?B?d0Z0ZktORC9ETEVHT0FnYVN0SGJ2QWJHUDd2RkVVNDBId3NJZkNBc3pQL29j?= =?utf-8?B?Zng1UDIzVUhXblhXcnpCcWQwZmd6dmUzc3NaUWJ6QTNjQ3owanJwUkxNQnpH?= =?utf-8?B?VnMrN0hYVVdMVjQ1NXZEdGR5NGZxQkRjemMxZEZ6QTN0eUxPNWxMQW8vbHhs?= =?utf-8?B?em84eE9IV3VGUGpKakFXL05QYkt6OXA4RFBKcFduR21qd2VxQkpxT1ZROU9J?= =?utf-8?B?Ui9wOEYvdndtUTZHbmxhV2ZHYUFMd3pqMFBNMTV3Uk1YMDRmOGh0T2Y3ZDZ3?= =?utf-8?B?bXRneE1mMExVWFJoZVZaY0Y0ck1uTUVabUUwUWtuV3lYdVU1S2UwckdrdUsz?= =?utf-8?B?dkdjNjBEcW5vb1YzbHF4dWFmZE5EakdtUVBYTnV4djlkaTE5Z21QeGFVaE9a?= =?utf-8?B?TW9TNEoxbDVxT1V3WWRib0Z6MVZxL2hyNE56dDNpcWNZL2hmYkNmL3dzbisy?= =?utf-8?B?bFlDZG9uOFRHVXNnQkNOeXJ2Y3ZGUlQvQzF5cm5jSlRTckx3SFV0Nnlja21s?= =?utf-8?B?SDNOV1hDRmg3c2dnN1BMSXZhcnVaeTRyVTZXWU9PdTRMd053RE51S2NuNytV?= =?utf-8?B?UTVZN2lEZzc1NXRVMkliNXRxNExORy90R1BxQ0RRTnhqbEt2Y0ZrY29YaTdx?= =?utf-8?B?T1FXRFlWanlNc3h2OVdMMkpyWTg3SEoyY25yanU1dG5tOWw0OHBzSkozeE93?= =?utf-8?Q?uy4UJf1bbwY=3D?= x-microsoft-antispam-prvs: x-forefront-prvs: 096943F07A x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(396003)(376002)(39850400004)(366004)(346002)(136003)(189003)(199004)(5660300002)(446003)(11346002)(2906002)(6246003)(486006)(8936002)(6306002)(2616005)(256004)(6916009)(99286004)(81156014)(786003)(81166006)(316002)(83716004)(93886005)(36756003)(476003)(71200400001)(71190400001)(82746002)(105586002)(97736004)(6436002)(53936002)(68736007)(102836004)(8676002)(66574012)(6486002)(66066001)(6506007)(3846002)(6116002)(106356001)(478600001)(7736002)(4326008)(88552002)(75432002)(186003)(25786009)(53546011)(26005)(966005)(14454004)(305945005)(76176011)(229853002)(33656002)(6512007)(86362001);DIR:OUT;SFP:1102;SCL:1;SRVR:BN3PR04MB2324;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: qsWNioLxXl4fl8gYZpdMSFcLt58dJzdb0xsT/+/szUPlT92rLoG4PU+ZWQjW75QjFiV0dAlTRvMkK5p2bri44gE3gQk/GWp2BdYy9asHOtwvsZ9eHfXB3YPRQM2r4Dd5eziT1qBInrx8QQNqXzBXbTv02B3sciYzL4UuNk85jE8/5se+tLc5nfvUnoHYtogpH3vTB2l96t9RLkGgYAjXJTTlBh19bexmDdYM9YgSjLT1Cm3uHtSMUOM0MBxR9XD/SvPqREKSrhQR7e5eyD2CpZVp8U/0Dk3qlv27IeP17387Y01j3BPa9wwHv3sm5zx++rJ7VW1glSlz3ZxzZLIuj5qV5mwamIcz/DsIEG8mucx4SC3mKkxegFqLS+xQw2JDUq5QqQdrcJ3OiseHTNLfv8A6HV+ekvZ4GEWwtk5diy8= Content-Type: text/plain; charset="UTF-8" Content-ID: <96EFB765BDA59C458724B267D2C5E5F9@namprd04.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: wesleyan.edu X-MS-Exchange-CrossTenant-Network-Message-Id: 6c538615-13d2-4126-55a7-08d6a34f68ed X-MS-Exchange-CrossTenant-originalarrivaltime: 07 Mar 2019 22:51:17.5720 (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: BN3PR04MB2324 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=DNPy2DFZ; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.75.121 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: , That would be true if the term you are normalizing is in the empty interval= context, and the cubical type theory has =E2=80=9Cempty system regularity= =E2=80=9D (like https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf). =20 Otherwise, if you evaluate something in the empty interval context, you mig= ht see something like hcom [] (hcom [] (hcom [] (hcom [] (=E2=80=A6 |x,a| =E2=80=A6 )))) with |x,a| in there somewhere. In HITs, Kan composition is treated as a co= nstructor of the type, and though there are no interesting lines to compose= in the empty interval context, the uninteresting compositions don=E2=80=99= t vanish in all flavors of cubical type theory. =20 > On Mar 7, 2019, at 5:41 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote: >=20 > So I presume that when we ask cubical Agda to normalize a term of type ||= Sigma (x:X), A x || we will get a term of the form |x,a| and so we will se= e the x in normal form, where |-| is the map into the truncation, right? Ma= rtin. >=20 > On Thursday, 7 March 2019 21:52:12 UTC, Anders M=C3=B6rtberg wrote: > The existence property is proved for CCHM cubicaltt by Simon in: >=20 > https://arxiv.org/abs/1607.04156 >=20 > See corollary 5.2. This works a bit more generally than what Mart=C3=ADn = said, in particular in any context with only dimension variables we can com= pute a witness to an existence. So if in context G =3D i_1 : II, ..., i_n := II (possibly empty) we have: >=20 > G |- t : exists (x : X), A(x) >=20 > then we can compute G |- u : X so that G |- B(u). >=20 > -- > Anders >=20 > On Thursday, March 7, 2019 at 11:16:48 AM UTC-5, Mart=C3=ADn H=C3=B6tzel = Escard=C3=B3 wrote: > I got confused now. :-) >=20 > Seriously now, what you say seems related to the fact that from a proof |= - t : || X || in the empty context, you get |- x : X in cubical type theory= . This follows from Simon's canonicity result (at least for X=3Dnatural num= bers), and is like the so-called "existence property" in the internal langu= age of the free elementary topos. This says that from a proof |- exists (x:= X), A x in the empty context, you get |- x : X and |- A x. This says that e= xists in the empty context behaves like Sigma. But only in the empty contex= t, because otherwise it behaves like "local existence" as in Kripke-Joyal s= emantics.=20 >=20 > Martin >=20 > On Thursday, 7 March 2019 14:10:56 UTC, dlicata wrote: > Just in case anyone reading this thread later is confused about a more be= ginner point than the ones Nicolai and Martin made, one possible stumbling = block here is that, if someone means =E2=80=9Cis inhabited=E2=80=9D in an e= xternal 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= example, 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 t= ype 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 = case). This is consistent with what Martin and Nicolai said because =E2=80= =9Cif A is inhabited then B is inhabited=E2=80=9D (in this external sense) = doesn=E2=80=99t necessarily mean there is a map A -> B internally. =20 >=20 > -Dan=20 >=20 > > On Mar 5, 2019, at 6:07 PM, Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 wrote:=20 > >=20 > > Or you can read the paper https://lmcs.episciences.org/3217/ regarding = what Nicolai said.=20 > >=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 invari= ant under equivalence.)=20 > >=20 > > The above paper shows that unrestricted ||X||->X it gives excluded midd= le.=20 > >=20 > > However, for a lot of kinds of types one can show that ||X||->X does ho= ld. For example, if they have a constant endo-function. Moreover, for any t= ype X, the availability of ||X||->X is logically equivalent to the availabi= lity of a constant map X->X (before we know whether X has a point or not, i= n which case the availability of a constant endo-map is trivial).=20 > >=20 > > Martin=20 > >=20 > > On Tuesday, 5 March 2019 22:47:55 UTC, Nicolai Kraus wrote:=20 > > You can't have a function which, for all A, gives you ||A|| -> A. See t= he exercises 3.11 and 3.12!=20 > > -- Nicolai=20 > >=20 > > On 05/03/19 22:31, Jean Joseph wrote:=20 > >> Hi,=20 > >>=20 > >> From the HoTT book, the truncation of any type A has two constructors:= =20 > >>=20 > >> 1) for any a : A, there is |a| : ||A||=20 > >> 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 i= t true that, if ||A|| is inhabited, then A is inhabited?=20 > >> --=20 > >> You received this message because you are subscribed to the Google Gro= ups "Homotopy Type Theory" group.=20 > >> To unsubscribe from this group and stop receiving emails from it, send= an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.=20 > >> For more options, visit https://groups.google.com/d/optout.=20 > >=20 > >=20 > > --=20 > > You received this message because you are subscribed to the Google Grou= ps "Homotopy Type Theory" group.=20 > > To unsubscribe from this group and stop receiving emails from it, send = an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.=20 > > For more options, visit https://groups.google.com/d/optout.=20 >=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.