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-io1-xd3f.google.com (mail-io1-xd3f.google.com [IPv6:2607:f8b0:4864:20::d3f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 20a5fa7f for ; Fri, 8 Mar 2019 15:13:15 +0000 (UTC) Received: by mail-io1-xd3f.google.com with SMTP id e1sf15531779iod.23 for ; Fri, 08 Mar 2019 07:13:15 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1552057994; cv=pass; d=google.com; s=arc-20160816; b=BYXDkERWorQlRms557aAhDj7FWOgx85WyV4HQupPupdlLJzeViRmzjh/vQz0rILqta Ejg/NNK9p18VyK43XrEh3jsWH2sF7Fw5h5p5B8mLpgHc1nI87cer2OTyfumUZrKpyB6A BBwNBCgJXtR98rDXCrvp9V2o4D1+BRW5MOemWxKNfLvEXtXiGAkwuK4dzobaESzPrIwK P3G6cc8hX7WK6LTHcyMsfxAXBdSGdv1EvPWR+9bznEB6ZH6feVTFVf9dbpYZrxppRs1/ p36sjeOUob0jOI/keG1hjRPv8NDPNzbuZIaS/DSg2+iEs8klQHf6YU6SZR4pyerjEhby NdWw== 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=QuP+INfy+brVR9Bgje/TfjEBkDuomzGkLymMQ/9fY3o=; b=ePZSjQq0aSHTj6KmABsBvVAb7TWXr+78c0WTUAMfK1S6/mTpITSVow5TS58FzOWnhq i7p6p3m5pcTejeUt3aaXl3xC8Ob5XrFryxxSdslfH/J8J6aZaEFsLtHwwbGAN19Rf3yh uq2kNZ05QShyeZYLS4Iqji8srIJpmDYEiUGxj2As6pW/apXhbx5lvCaqcT4YxQB6iQsj wd8cYGW/IkU+I3/pPTsoUh93ew4nY/tKH5Ita5ejpqyxWN9Ll+bfW9XdtV8+sfgQsn31 Bulh5MI4KbtZZYvzUKjQkha24NzAOgwNZ48u1eWt57txc8Z9/ovkmxhWbcHezaLaKRzt nndQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector1 header.b=c1Q8FdSf; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.74.130 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=QuP+INfy+brVR9Bgje/TfjEBkDuomzGkLymMQ/9fY3o=; b=LX28gVSKZmpMJ0KSh7P+mUu8SKcJv9xs1SZ8vWnUa7v8ELtxv6/Qi7hqnMtEij02WF YG1Vqn173N9XnMl4adJIhO5NgDmgEhXNWl7Sci/DbdHgGoNsVSTMKWXDsoofKY7PMKT4 BjS0Lr0BIUPfxc3WzQPNjzi4fQUeOnHCG7LHfTya0SITuIy5G0aumBsbxgVirJWs+N/0 XHqxkHyz4lNiLQCnRMdU4hjHnWUc3C2Q2nxFMQMijhXUubqRSkmOhmPrx60bNH4r0QYa MRfhKP81Ispwj53j8qRQ2Oh45E2kyOELPVOLGHbDUxqZ57KwgrKPUngPhHL7PjV+0HhM 5OHQ== 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=QuP+INfy+brVR9Bgje/TfjEBkDuomzGkLymMQ/9fY3o=; b=B2p/Fxiek2ioRHImKkpSsRwa2YR7Lsg3krprB/ZWRkaUAaPelzlfrM8kXbBKWHeSSh XwU/ADWthCeoI0ZLDdNO3eGKLxRsKCVC0dwoEbwTCllBJdzcaDKUMOJjP2fFeTU7sZ/8 qlJ/7l1BVaHEwOo3BYrsYtUqTHkenBqK4LJvU4bUtE4+86UIpI9avdpLh7aBcNe3vwQE /iRumK+Z9jak/+LOiUq3R2V5f4ntRUyMwyCKsVy+APhqjiU9s56awiphC/GPyvZVXOv2 qLWvsuk/rbxKp7NsZ6JgXpzfzEzicJ5zxmw9zTObmxVh+wwYRwpay7fC/oXbQOtRCnOA ztIw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUiSEVKzNJ+GsztgwVbO79B8gNOrt++9kwXX69sQaC/cEbGN3HZ 4acfCCbDCG9lIFkkjstRZcM= X-Google-Smtp-Source: APXvYqwYgoCrRXwXs96bGCTZ/jB+LF7T6eGIMgTs+dm3QMLZt6+lJmgxddj7Z6+YngTCc0rr/OQy9w== X-Received: by 2002:a02:3b2b:: with SMTP id c43mr10875501jaa.91.1552057994081; Fri, 08 Mar 2019 07:13:14 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5e:8303:: with SMTP id x3ls3769490iom.3.gmail; Fri, 08 Mar 2019 07:13:13 -0800 (PST) X-Received: by 2002:a6b:8f01:: with SMTP id r1mr2380989iod.27.1552057993722; Fri, 08 Mar 2019 07:13:13 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1552057993; cv=none; d=google.com; s=arc-20160816; b=atZ9QwKu0kjBp1HZTlUCMB9bXqfNZ0/cJXh7HtMMToPI1ZIKstjPMux4mI0dHYQXcI SnDjYf9qipOUMtUP83knRzaykyT/nFGr/PMDWi1tH2VyZ5i2COpne0oc8ODyrGg61s+F 9Wz+Q7KOAB1fJGglvjdFo/fgw7Ed5Cxj/ulBIlPAUvEs3mQuGhatSlfZPQSHJP3pTc6F N1wI2yXGlkOwkm2KaLHH0AuFcmvMaqpwET1HoeS26/VTZDXQ44elhqw8Gb+rRY+EP3YC PGiSOuVFRQJfy5SGS+UUNPRzav/Mp0b0CAqlX4yqd2eJZgysIkrabOkVB9K5B+fHecrt kpCQ== 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=8v7ozuJud/ge/xAE6Ih1abvvRKs8DB0o3kqcRa+Lpj8=; b=HLdOk6Tfqkgk9yk6YkY+5z0MwOHUkrfRb19ckXYhmBKFI7Ni+L7qGHPvBbHy3V3JoV QmQInIAFq1l2lY9rjh2NY3v4Eyad4BTygat0PH747EIoC5ID1XGs/x91ZEJoTqPo8eiL x5UZf2+Lly6VOOLb2wSTm+cxq6YX5spfZMnVMamB+tZvAkK3ErqRLx1Qj6r2z1D5SWIp HDmxNsV9ZCXJsUk94ItUXiSk2SQGIJKatVxMv+1sy9p1MK3nq67IKMV4tY7Lt/c+t3Gg aG1D9GfewAxq3vF9l0jQB+L4jLHN4Usm3+BGzBUU/cizfhg95BaWx+8gxwHsjurjpvo9 y67w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector1 header.b=c1Q8FdSf; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.74.130 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu Received: from NAM01-BN3-obe.outbound.protection.outlook.com (mail-eopbgr740130.outbound.protection.outlook.com. [40.107.74.130]) by gmr-mx.google.com with ESMTPS id 77si592972ita.2.2019.03.08.07.13.13 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Fri, 08 Mar 2019 07:13:13 -0800 (PST) Received-SPF: pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.74.130 as permitted sender) client-ip=40.107.74.130; Received: from BN3PR04MB2195.namprd04.prod.outlook.com (10.167.4.13) by BN3PR04MB2145.namprd04.prod.outlook.com (10.166.75.20) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.1686.18; Fri, 8 Mar 2019 15:13:12 +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.1686.019; Fri, 8 Mar 2019 15:13:12 +0000 From: "Licata, Dan" To: Anders Mortberg CC: Homotopy Type Theory , =?utf-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Subject: Re: [HoTT] Propositional Truncation Thread-Topic: [HoTT] Propositional Truncation Thread-Index: AQHU06NFzBcK2A371Uil15CpceOYdKX9o6aAgAAFZ4CAAo7QgIAAIy+AgABdtwCAAA2zAIAAAs4AgAAC34CAAAYtgIABBYAAgAADzIA= Date: Fri, 8 Mar 2019 15:13:12 +0000 Message-ID: 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> <98CB1099-377A-4A5F-94F2-B33C36D577B0@wesleyan.edu> <50111384-09a4-4c30-8272-fa9e5997d3c3@googlegroups.com> <7a7c3e3f-df35-42ea-9d89-f0d20b855e9e@googlegroups.com> In-Reply-To: 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: 68759727-d959-4c2f-3dc8-08d6a3d894bc x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600127)(711020)(4605104)(2017052603328)(7153060)(7193020);SRVR:BN3PR04MB2145; x-ms-traffictypediagnostic: BN3PR04MB2145: x-ms-exchange-purlcount: 6 x-microsoft-exchange-diagnostics: =?utf-8?B?MTtCTjNQUjA0TUIyMTQ1OzIzOjFscWx3WnpRZGpYNFBoUzRiT2R5NTZkWk03?= =?utf-8?B?L0lsYnNGbkptN0xtS1loNXV4UlBOYjdLZHYwSnNCQktzSFJKTWhkWGo1NFho?= =?utf-8?B?Y0NzWk9nU01EaXdQcGx6ekFpeE5YdzZWd2h2M2UrdWZxMU1NN05EUlRmZzRz?= =?utf-8?B?QThXRWY5OStLTWU2WDdhOXZ5c1JXY0Z4ci9ZRDYyU1llVDdjd3ZjQ1lIQWhz?= =?utf-8?B?Y0lpYjhYTGpESWl2SG02QVFBY081NnNvS2QydXlSc0lKSXUzVWFublVuL1VR?= =?utf-8?B?Q2R1U1dVTGhSWnFrSklOcml4aHVseTZZelN6NHVYYXlZQ2hGWm1BeEdsUFRh?= =?utf-8?B?aE8wQ20vaXNzSGlVanRpdzQrK2VlUmdyaGdKUmhYbXBGbGpGYmQrMnR4NzVT?= =?utf-8?B?dkdJaGszOHJMNVBUdVVxdE9XQWJiODYvM1FobDd6dGVlZ3YyaVNFZXV0bDBF?= =?utf-8?B?VE55Y3h1L2V5UTlnNFFwZTFic0lvWXhlUGZGbEdvQktNdnJ1VTRyZUtUbktK?= =?utf-8?B?UkhqUGxnU3RHTHFHcjc5UkIwcnBmTUVid3U2NnZuSlR2MlVjVy9TQlBWT29x?= =?utf-8?B?ODF0MGtsSHdwZURNSDdnckFtbDJnTkZPRkg2Q2pvb3RqQ1lQZFp4TEowSVda?= =?utf-8?B?SlQ3VWxQVWU1ckovOW14RnFzMjJ0SzVTSTZVUDFENDBUc1Q3eGdDZzhmL1dH?= =?utf-8?B?bUV2WEFTejljWjBSc3o5NURacWFuNXFDNFNpWVVDRU1yMUhmMEUrZjhUSEdF?= =?utf-8?B?cUpMaVkzNGQ2RDZkWi9xUEFuVzFDQVVXME5vbDZQOGt6WDhOZVRSRlZEMmw4?= =?utf-8?B?aWZtalQ3MnFMaDVJUXNuLzJIK2dLc1B3Q3Ara0RzV0k3NmJpeFhuVzJUZjFY?= =?utf-8?B?eTNiOU5tdGZRVUFYa1hZVGhuQmlCUHczL2Q0STBaeGxaUEpzcFVFcTBsYmtP?= =?utf-8?B?eEpUZmRYNU9FVUEvVVJyOFBBUWpiZy8rSjV6N2VDK0puV0V6VGVzMm5MR2Iy?= =?utf-8?B?VkxDaUJDUlZXVDBtcE9uaHA3cnlhZC9yQi8rampBU3doTnpCLzI3Y3FYTlJ1?= =?utf-8?B?Q2twQVpYVnZkejVNdFhqeEoyRGxCTFBKYm9LM3BtenE0RU5ReVFSOFUyRVFZ?= =?utf-8?B?Q0gyN2FTVDlPdzlWc29LanZvY1BuZ0Fhb2hyOWF6R0pISzE4TWNVOExFODY0?= =?utf-8?B?V1AyQk55NzhDWExDcEVkbFpWTXo3S29QejcvK01Bc1JhNXNXY3plbHFycHpH?= =?utf-8?B?NmYzV2Ird1dTTk9NZXRxUGxPZWk0VHBtbGxVWURyTkhPNkU3Wm43QWJyZGhv?= =?utf-8?B?cGM3US9rTjJoNFRvUjIxeHJ3Y3F5SjJ0d2l0TEdPOVJ6NHNaT1dseWdxZkpR?= =?utf-8?B?UUdKZzlkSHEwZlNaY011VTNMNXdJb29yZFVtNjBzT3luK25OVjJNR3FhbC9j?= =?utf-8?B?KzB2OU02TVFIQ1YrUjdsSE52RUdZTFNXL0d0L2tTZzRUQ3Z0L2FhblN2UFIw?= =?utf-8?B?ejErNWN4alRKODRkTi9lM2syQmVwSUZ4T294Ykd1eVlXMkNFQzJUM2owZ1hX?= =?utf-8?B?NEtOcTl1Zm1NMEhyanhIMzB5amNIVWlLdVI3bW51QlVQZmZwOW5iWnVjSnJa?= =?utf-8?B?OUF1c2pDKzdtNjdHU1RiZDBPVW90K0JtRklBcU5GUnJtOGQ5RVpDdUpLb09o?= =?utf-8?B?WW1YaWg0UjU4TEsyK0tlcC9BV2NqaDJKTytCckw1OXJGc1J3R1BsbjhNSkxp?= =?utf-8?B?eEtCbzdFbzlreUtFb0hlNTc4clRPR2JxU3p3dWV1NUNBaFFscWRTT1BHWERJ?= =?utf-8?B?UGU2OTVYd1FBeFREOEEzbGpuWGRzL0VZZklUbTEwRmpLQXpoQzRpN1YwMFRj?= =?utf-8?B?d0lsZlQzYldUaThyRmV5bXBYMEFBVmJkcmJ5eVd3U09KZDZhbmdEVkJuZGpV?= =?utf-8?B?Tyt1Y0Z6UHpnPT0=?= x-microsoft-antispam-prvs: x-forefront-prvs: 0970508454 x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(366004)(136003)(346002)(376002)(396003)(39850400004)(199004)(189003)(786003)(26005)(14454004)(25786009)(229853002)(4326008)(6486002)(66066001)(6116002)(6916009)(68736007)(76176011)(75432002)(66574012)(6506007)(478600001)(7736002)(305945005)(486006)(6436002)(99286004)(14444005)(54906003)(3846002)(256004)(53936002)(53546011)(5660300002)(88552002)(2906002)(966005)(33656002)(71190400001)(2616005)(186003)(71200400001)(86362001)(81156014)(446003)(81166006)(1411001)(476003)(6306002)(8676002)(93886005)(11346002)(36756003)(83716004)(102836004)(105586002)(82746002)(6246003)(106356001)(316002)(6512007)(97736004)(8936002);DIR:OUT;SFP:1102;SCL:1;SRVR:BN3PR04MB2145;H:BN3PR04MB2195.namprd04.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX: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: ujFZ0P/odgLi4V4EWQd20f9DKpxUECVZG/jRCBDG+QZP5GuI1+kOwKh7Nl2FjeaALuCwnloRx+eop5vM0s5ccNe3ajZC4/GEaDle8csKQJ4SRN4BIsVe8Df39txCNzU4YZ8GqpUaygSIl5+Gc0VRudB67TueH3voemN/kbFfKXqs6YRpAQas0tYQH2Zq2j2IafZCQWwm6ZKPLtvUNsdEvFHSNSADkuENHAU8HYSFdjr3XGWp/+4aKXp+ldLcZU3rG7+KVVBaT+Ku2LJfao4HKBskWtVU35y8jeFMRUzthHwKzRHax+KnZDIhhMoLU2wKGQ0eiGxfWZUeBV3yo8bHdSUeVnfm7M800hHS8FVw9gZnD22YlQY7wonnk3ziZP0468BnDnOTczc8jtlG9WQ/QAHHwiUvsSq5WqaY5YiaPSo= Content-Type: text/plain; charset="UTF-8" Content-ID: <33FCEBF45899314693137C842D02776B@namprd04.prod.outlook.com> Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: wesleyan.edu X-MS-Exchange-CrossTenant-Network-Message-Id: 68759727-d959-4c2f-3dc8-08d6a3d894bc X-MS-Exchange-CrossTenant-originalarrivaltime: 08 Mar 2019 15:13:12.1040 (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: BN3PR04MB2145 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=c1Q8FdSf; spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.74.130 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: , nice! the negation trick is clever. Martin, I don=E2=80=99t understand why this situation is any different than= natural numbers, though. If I have a closed term of type nat, I can norma= lize it, but then I (externally) need to read through all of the successors= to figure out what number it is. (Or maybe I can only weak head normalize= it, in which case I need to interleave further weak head normalization aft= er every successor.) Is this an unbounded search? The parallel is to read= =E2=80=9Chcom []=E2=80=9D as successor and =E2=80=9C|x,a|=E2=80=9D as zero= . =20 -Dan > On Mar 8, 2019, at 9:59 AM, Anders Mortberg wr= ote: >=20 > In fact, in Cubical Agda you will not get these hcomp's with empty > systems. The reason is that because of the way hcomp works in Agda > there is a very nice trick to implement the "generalized hcomp" > operation of the paper that Dan linked to. I summarized the trick in: >=20 > https://github.com/agda/agda/issues/3415 >=20 > I added this to Agda some month ago and it should be possible to > update Simon's canonicity proof to get a stronger result saying that > the only elements of HITs in the empty context are point constructors > (like in the AFH paper). For this to work you also have to impose a > "validity" constraint (Def 12 in the ccctt paper Dan linked to) so > that empty systems cannot result from substitutions. This is currently > not done in Cubical Agda, but if you start with a term with only valid > systems then you should never get an empty system. >=20 > So the extraction of witnesses from existence statements should work > as Mart=C3=ADn said in Cubical Agda. >=20 > -- > Anders >=20 > On Thu, Mar 7, 2019 at 6:23 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 > wrote: >>=20 >> And this is a wildly speculative question. If we used Andrew Swan's iden= tity type derived from the cubical path type only, as in the abstract libra= ry file https://github.com/agda/cubical/blob/master/Cubical/Core/HoTT-UF.ag= da) would we still get this phenomenon? Maybe not? What I mean is that we u= se normal Agda, together with what is offered in that file and nothing else= (so that we are using HoTT book axiomatic type theory). Martin >>=20 >> On Thursday, 7 March 2019 23:01:33 UTC, Mart=C3=ADn H=C3=B6tzel Escard= =C3=B3 wrote: >>>=20 >>> Oh, this is annoying, because it seems to mean that we would need unbou= nded search (to drop all "hcom []"'s) until we can read the |x,a|, which is= against the spirit of, say, Martin-Loef type theories. Martin >>>=20 >>> On Thursday, 7 March 2019 22:51:20 UTC, dlicata wrote: >>>>=20 >>>> That would be true if the term you are normalizing is in the empty int= erval context, and the cubical type theory has =E2=80=9Cempty system regula= rity=E2=80=9D (like https://www.cs.cmu.edu/~cangiuli/papers/ccctt.pdf). >>>>=20 >>>> Otherwise, if you evaluate something in the empty interval context, yo= u might 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 constructor of the type, and though there are no interesting lines to co= mpose in the empty interval context, the uninteresting compositions don=E2= =80=99t 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 typ= e || Sigma (x:X), A x || we will get a term of the form |x,a| and so we wil= l see the x in normal form, where |-| is the map into the truncation, right= ? Martin. >>>>>=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 ca= n compute 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=B6t= zel Escard=C3=B3 wrote: >>>>> I got confused now. :-) >>>>>=20 >>>>> Seriously now, what you say seems related to the fact that from a pro= of |- t : || X || in the empty context, you get |- x : X in cubical type th= eory. This follows from Simon's canonicity result (at least for X=3Dnatural= numbers), and is like the so-called "existence property" in the internal l= anguage 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 th= at exists in the empty context behaves like Sigma. But only in the empty co= ntext, because otherwise it behaves like "local existence" as in Kripke-Joy= al semantics. >>>>>=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 mor= e beginner point than the ones Nicolai and Martin made, one possible stumbl= ing block here is that, if someone means =E2=80=9Cis inhabited=E2=80=9D in = an external 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 t= erm of type ||A|| evaluates to a value that has as a subterm a closed term = of type 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 ba= se 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 sens= e) doesn=E2=80=99t necessarily mean there is a map A -> B internally. >>>>>=20 >>>>> -Dan >>>>>=20 >>>>>> 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/ regardi= ng what 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 inv= ariant under equivalence.) >>>>>>=20 >>>>>> The above paper shows that unrestricted ||X||->X it gives excluded m= iddle. >>>>>>=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 an= y type X, the availability of ||X||->X is logically equivalent to the avail= ability 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. Se= e 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 constructo= rs: >>>>>>>=20 >>>>>>> 1) for any a : A, there is |a| : ||A|| >>>>>>> 2) for any x,y : ||A||, x =3D y. >>>>>>>=20 >>>>>>> I get that if A is inhabited, then ||A|| is inhabited by (1). But i= s 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, s= end an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>>>>>> For more options, visit https://groups.google.com/d/optout. >>>>>>=20 >>>>>>=20 >>>>>> -- >>>>>> You received this message because you are subscribed to the Google G= roups "Homotopy Type Theory" group. >>>>>> To unsubscribe from this group and stop receiving emails from it, se= nd an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >>>>>> For more options, visit https://groups.google.com/d/optout. >>>>>=20 >>>>>=20 >>>>> -- >>>>> You received this message because you are subscribed to the Google Gr= oups "Homotopy Type Theory" group. >>>>> To unsubscribe from this group and stop receiving emails from it, sen= d 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 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 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.