From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) 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_AU,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 30118 invoked from network); 2 May 2023 08:49:04 -0000 Received: from mail-wr1-x43d.google.com (2a00:1450:4864:20::43d) by inbox.vuxu.org with ESMTPUTF8; 2 May 2023 08:49:04 -0000 Received: by mail-wr1-x43d.google.com with SMTP id ffacd0b85a97d-30633990a69sf340606f8f.3 for ; Tue, 02 May 2023 01:49:04 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1683017344; x=1685609344; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:reply-to :x-original-authentication-results:x-original-sender:mime-version :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:to:from:from:to:cc:subject :date:message-id:reply-to; bh=bf9b4DLwzA65wMxoWsSbL+A+jp/t/damEruQee+ofAE=; b=BkxNT4zVpubXOqtHUxc5+9Xv0UdplbnSRATYLLFsoQlI3TfJzjZHs7Y1xdGqEtAD2Z pMBCYpq3jHs6JsaCDfk6IfwJZ0m+FZzKdMMyYsftzZxuAYw4W9eTUFGSyBrJRQ1KMLni /F6I1pqtjZiKLG5nLK71BypySbUXDNxWGkROqzxYYkKrfTyoaCarANfBwII++NGcAObt /PetaQ55DKIUZXoMjLqM66e91ZbwgVz7icHx/ePiQtYt8iyHurtXyxRYYOmzvDzUvs/J V1wrjqxzUfuLYyvcsMzsYCH2QcvbFHR7gjy8DT6QLt2TdNqcT5B6+Slf2vY+ZQ+whjEC DSdg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1683017344; x=1685609344; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence:reply-to :x-original-authentication-results:x-original-sender:mime-version :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:to:from:x-beenthere :x-gm-message-state:from:to:cc:subject:date:message-id:reply-to; bh=bf9b4DLwzA65wMxoWsSbL+A+jp/t/damEruQee+ofAE=; b=RK+DkfsHgyW1JUitTz/4Mfk6eP7MF2RGCCXjOuvRdc5CFTgS+9UUGfEmux3aBUARGD 0Jnz/9NNqb1LVhD2VwxKM7wcwnE7A4JT4HVUGs9Pess0Yltsu2xrunWfq7vQcugJifI/ lFCT0rRJOmvOREbDJf0WbEWVbfI8fvfZJsER0NVEZUdcPblyfvqd9NfsvOzHFLgSYTsY 3xg3xr3CeEbPJY1fv1SFuFfFu7/y0XiKiXF6cPpgKjHogLByMw28wR2YsAHPxfU+/zM/ FMNJtI+ZrB7XEuGWYxH9lNimde8AIdcYdvo6SQFBa9X6ahnA1ImCaDlv9QEj8ZJakyc0 3ZTg== X-Gm-Message-State: AC+VfDx4ORbwPkRGmKhTcouWnPOVCe7I1EW5w0123GynscoO/t0JG9KM MUEg0DiZV6E/qwhLfdUsPlc= X-Google-Smtp-Source: ACHHUZ475wrtJsCKA1l7upacx4flf/lk75tCBYQ8gJJg0OsDGBiB6PP8c+r0xyoKfAvhhUgP3VZezA== X-Received: by 2002:a05:6000:47:b0:306:31a5:99aa with SMTP id k7-20020a056000004700b0030631a599aamr462057wrx.4.1683017343824; Tue, 02 May 2023 01:49:03 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:3115:b0:3f1:714d:c42c with SMTP id g21-20020a05600c311500b003f1714dc42cls6363716wmo.0.-pod-control-gmail; Tue, 02 May 2023 01:49:01 -0700 (PDT) X-Received: by 2002:a05:600c:2189:b0:3f1:6fca:d5a5 with SMTP id e9-20020a05600c218900b003f16fcad5a5mr10828641wme.17.1683017341424; Tue, 02 May 2023 01:49:01 -0700 (PDT) Received: from uidappmx02.nottingham.ac.uk (uidappmx02.nottingham.ac.uk. [128.243.43.125]) by gmr-mx.google.com with ESMTPS id h5-20020adf9cc5000000b002f41048491csi1641722wre.7.2023.05.02.01.49.01 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Tue, 02 May 2023 01:49:01 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) client-ip=128.243.43.125; Received: from uidappmx02.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 6EDA32EAB0A; Tue, 2 May 2023 08:49:00 +0000 (GMT) Received: from smtp3.nottingham.ac.uk (smtp3.nottingham.ac.uk [128.243.44.55]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx02.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id 6A96E44EDD5; Tue, 2 May 2023 08:48:59 +0000 (GMT) Received: from uiwexedg02.ad.nottingham.ac.uk ([10.159.172.14]) by smtp3.nottingham.ac.uk with esmtp (Exim 4.94.2) (envelope-from ) id 1ptlgy-00030m-2w; Tue, 02 May 2023 09:49:00 +0100 Received: from UiWexCHM04.ad.nottingham.ac.uk (10.159.186.8) by smtp.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2375.34; Tue, 2 May 2023 09:48:59 +0100 Received: from UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) by UiWexCHM04.ad.nottingham.ac.uk (10.159.186.8) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.2.986.42; Tue, 2 May 2023 09:48:59 +0100 Received: from UiWexEDG02.ad.nottingham.ac.uk (10.159.172.14) by UiWexCHM02.ad.nottingham.ac.uk (10.159.186.13) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2375.34 via Frontend Transport; Tue, 2 May 2023 09:48:59 +0100 Received: from EUR02-DB5-obe.outbound.protection.outlook.com (128.243.226.54) by smtp.nottingham.ac.uk (10.159.172.14) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_CBC_SHA256) id 15.1.2375.34; Tue, 2 May 2023 09:48:56 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=GNcdm7IECVIfCdzgOmJJKrYOO7TxajkUgxPrUeA1gkpawxEA61cfV65/S7sSTxs0Z/oE+Av7LtllQ9mEdgEDUFf6ppZMi3gSg3D3/Gn3bvKjAxu2FO4jdoNn7Imxkzo+P36sfVlKi177Iccegsgb7Ci3U99/Gga+TSKUEpZNQiaHx6bhI75rGHcI4MCFq2Afbn2xrtakrAQ3N8HH/ZC9xSCDRn9ZcHUsroBFOd2r4JfefcIFjJdmi6+uTu/cYxP7isso1vtgsRHraZajXFJVpsVeaEwW1MxojTNB+L5b54DYx54eLxA+FcmkIhE9xSxMC9g9DAqyPvRwnlM3TLAltQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=JhsmiW+lho5fycFY2QPHneZ9UoWCn52vl64W21YaJ+E=; b=jKjs7aWMthJrZK3FlVEL3aWVJDMJiLu+mDMEIr/ASKyCIm9CBwACO7qGYV06+DpJH/6badIxoDwjFKPowHktd/ZcSgW3Zjfm8xGvUs3drgQfI7HpqJ2cjcqwxeTJvDULZFj/qu9MUFN1MkdjtpVSMr8s+jAtDDcdAnarqf8wHyNAGEsdSzIkFq+tACDNVqSZHDL6qlcUstxjmYXZw04/UNR4Es+qgkUPUXS+4OWHHiju49qDwXt+vxhKOPh78VVPPSaNRX46aJa0Dze1AgzWQBGhWeLxIwb0lMglJcDjY9ieAzj4ACYNN9N5i9Ne6sFyEDSbjCoK49qwLQkzRXLqlA== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=exmail.nottingham.ac.uk; dmarc=pass action=none header.from=exmail.nottingham.ac.uk; dkim=pass header.d=exmail.nottingham.ac.uk; arc=none Received: from PAXPR06MB7869.eurprd06.prod.outlook.com (2603:10a6:102:1a0::20) by AM9PR06MB8083.eurprd06.prod.outlook.com (2603:10a6:20b:389::9) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6340.31; Tue, 2 May 2023 08:48:55 +0000 Received: from PAXPR06MB7869.eurprd06.prod.outlook.com ([fe80::44b7:bf4:25f9:14bc]) by PAXPR06MB7869.eurprd06.prod.outlook.com ([fe80::44b7:bf4:25f9:14bc%2]) with mapi id 15.20.6340.031; Tue, 2 May 2023 08:48:55 +0000 From: "'Thorsten Altenkirch' via Homotopy Type Theory" To: Jasper Hugunin , Homotopy Type Theory Subject: Re: [HoTT] Free higher groups Thread-Topic: [HoTT] Free higher groups Thread-Index: AQHZdDivU07vMO5vwU25kyIDAE1cha9CsxWAgAQFAO+AAAURdQ== Date: Tue, 2 May 2023 08:48:55 +0000 Message-ID: References: <87leigyeya.fsf@uwo.ca> <87zg6qy4gx.fsf@uwo.ca> <21ED9406-6C3A-4B26-A74B-34C2821C97B6@gmail.com> <87r0s2y0rp.fsf@uwo.ca> <73121272-421b-4dba-943f-b81f32854862n@googlegroups.com> In-Reply-To: Accept-Language: en-GB, en-US Content-Language: en-GB X-MS-Has-Attach: X-MS-TNEF-Correlator: x-ms-publictraffictype: Email x-ms-traffictypediagnostic: PAXPR06MB7869:EE_|AM9PR06MB8083:EE_ x-ms-office365-filtering-correlation-id: 77bc1735-5597-44d8-b91c-08db4aea0fd6 x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: 05POPrz82JequFzV32rKmI9peblR/sXdz1bdlKH9+RG+T0OPcWtm5UY+8rlWW9QZ1T+eXHmGhuREo7tA02xXyZ7R5y/WL3xxCfSHpHMCIfxV401VanQK8TudnpwO5pTNXA2rsJCkBo41EtilB4X1XJXx8/Pkk16Ero9I5fztBuXqOi1LozeB006sqC3EY4NON4SWJPQuvRp9AhltshfIbu6k3zDIc8LCbmyLmn4S4uQFeKCube11p4LbiBvoeExxhYRHEtZDfAqj+Xum1Fm312iljd8KksOgCHVIn25nH9izeRZMcjGC8oeKECsG21cPfbg6GSS3SksEkHuo8G1MJe2VGypsiGa56LjG7m0pGam70w8Xxn00OW3OnSeddOh6H/s4ZD3HFnehGNkwGg79QWLmIGPBLjzgqSpCwREwd0QcItE4aqKpnhN9F54etWlB6F1L3zYRt0bPiMxxGE5uLnFSGwcw1VLhMn37EzzoLziCtdtoP5yW1aLJPLD1Kc7T08qj/nyzRLtCBLQlP6hxf5INij9Xwk7r5QoBpwv5p7Ve0swCxPpuXFfpR3WdsyYDSI/TJk39iSOOAn8v/eFGdtBXBSnzpVeYxuqNoEdA+3U= x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:PAXPR06MB7869.eurprd06.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230028)(136003)(366004)(376002)(39860400002)(346002)(396003)(451199021)(122000001)(71200400001)(38100700002)(38070700005)(55016003)(166002)(2940100002)(26005)(66574015)(186003)(6506007)(52536014)(9686003)(83380400001)(33656002)(53546011)(2906002)(8676002)(8936002)(5660300002)(478600001)(41320700001)(19627235002)(45080400002)(316002)(110136005)(966005)(64756008)(786003)(66446008)(66476007)(66556008)(66946007)(86362001)(91956017)(76116006)(41300700001)(7696005)(66899021);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?utf-8?B?QkQ3VlNIU0JQeStUYUxTeHpkRGVyR1QyMjQrdXA1RFFtRnJFYXh0V0IwVWRh?= =?utf-8?B?MmJwNWlaZnhHenlIUmdFay9lSjZST0JFOTVFNVIvcSsyTlJQVDY3STZaVHhr?= =?utf-8?B?Wkp0WFZFT093TlFHeU1RNTJnTVVIRmZPaE5ObmwrWmZvcFNWaGJaVjhCWWhQ?= =?utf-8?B?TkQ4dTNvbVlYMi8yR3RwdkEzVFFYS0FrSzBTcFAzbXh6M0R2RmpQM1lLdlhh?= =?utf-8?B?MWNpbWVsV2N1MzFDNTA4WlpYNmdza0pTSFZIZE9WM1ltcDdLZzNzdTVsaDgw?= =?utf-8?B?UFltVVozZjJaYlA1UXRZVlB4VVhDM3N4QkFIdmNIN3hUYXljdzNpVVNySWJ2?= =?utf-8?B?OWFlbE1rTW1vVlZscStwTFR2UTZxa0JtaE1PeVh1NEhCSGg0WkFRY1RTUTVX?= =?utf-8?B?d0NPQTVFRnBDVlR5YUpub054dDZkQWlGQjJRbHVLVjBxa0I5RmJESlU2NlYy?= =?utf-8?B?S1N4MFdGZ0NpbVNZeVBRMWZLSWhwSndBV0hCYWpncEZRVnZqS2xNZ0Y5UGR2?= =?utf-8?B?S0lZa3pNMzhqdUt2VVlvTzc3UU1wV1FXQkdxZnZJZlJqUnU5NnpYQUExUmpn?= =?utf-8?B?eVNuK21nREI3aU50dlJjWlpDU1ZXaUJXQVorWmt5UnZwWThrY3FZbHF3TUUw?= =?utf-8?B?bmFkczlUTHlnZEtkekQ3STUxQ1FZaUpTYnRiOVQvSTYwQ0lSN1Y4eFlKbW50?= =?utf-8?B?NFd1TENESld4TzZ6RU9uYnl0QjRkbm9YUEFqeGZhNkZnR3dxNWRnMjVDU25x?= =?utf-8?B?LzZmWi9YRU1wakphS3daYlNCMDdCMFpxZ0NxRkZaQnIvUlc5T2FZcjJTVzk3?= =?utf-8?B?RXZ1TVNwVkNJTW45aitzOVZUNUhONU03Wkp6SElVeFdabndFaHpyN0FFOEpU?= =?utf-8?B?ZlpQbnptQVFOd251dmUzSk43TTFSSUFtK1p5a1BSaGczSjc3cE8vK1U0L1VJ?= =?utf-8?B?WlBidWM4Y25UT29lam5wR1FCRVpsc0wvcmI3aTdneDJyZ3NCeFMrcHp2QWNp?= =?utf-8?B?MkUvMndTZWphOG9QOHltQXJ1N3FnV3NoUTJnNk1BY3RKU1lra01mQ2QzQ3po?= =?utf-8?B?MFk1VGY5MmhDVEJZQk9RcDdCRDVuSTZqTEJVdmdsTFhLbGNENmVPLzkxUnNq?= =?utf-8?B?bTNDREI1aHc2R3lKV2RtdGNGcU1IMW15dDl0Q1M4NlhvVUZhTTNuSFQycHNF?= =?utf-8?B?QW9CNFVsRjdGWnBSWTRVK0RuejNldC9ocnF0YjhFR3ZLTE40TTBuczl0a3Z6?= =?utf-8?B?bXoweU9ISTQyVzN3UnJlajc3aGdMUWJ2akZ4dHkwNVloMnRPOWVXNlZBRER5?= =?utf-8?B?amRNNTR0TCt2SlNKenR3dDhZdTJuWFJGQnBubURubUY4cGpOcHVNR3pIaExH?= =?utf-8?B?aUxoU2s5bmJlWEpDaEwvZzZSRVhkU1hTWTlHL0ZYekhUTS83WUlkWEFReWlw?= =?utf-8?B?RmlHc0I3aHBwU0NZNDdVOEhxZjFUWlBiTXdaa1pXeFExdTNtdjlYNjNWbTMy?= =?utf-8?B?cC8wMjhkdFArMXVEd2xQTllTQjBzNVEzTkNzVEg2S2ZzL3J5Z3RCRXMrMEw1?= =?utf-8?B?SnI2dWlOQ1NsN3h1MzFqamZOcHMraE5jRmRINzBYRm5PbjJzamNWbCtlOHNT?= =?utf-8?B?Qk1mc1RXaDJGL1AyTnZncC9tRTZMOVUrY3M0SmM5Y3diZXpUcFlOaDZIZGlL?= =?utf-8?B?RkVpL3FzKzhaNXErZEgzRmNYWDk0eTFzRGJ3WHVCdTllckpvSktsRXFFSTFO?= =?utf-8?B?dGhPZVViYnBQTExBa01tcHJkaW03OEJHekIrbDB1S2sycUppcEhFOGh1WFU4?= =?utf-8?B?VGZLcmN0Wit1eDFpTzg1VldiRjVBYTA1bDdFbW80ZjUwK0JydzhhMlQzeFFN?= =?utf-8?B?dnBMRCswMjNRWkloWHRTamNLaGNSd3c1eVc0Y05xd0RyU2hFV2NvTGVqcFZv?= =?utf-8?B?c0l2L0I1enVMYUdzWXM3TkNLV3oraytITGZXOW9rSk5rVi8xMmhDdjlrc0RF?= =?utf-8?B?VW1ELzlhT0p4cmh2eTBNczIvQ0RHRGtxaDRMaFErNlg2SGNmNnBlWEdSWkNM?= =?utf-8?B?eW4zZjB1S1ppYldTVHF3VTlIRG9zNUhqRk9uaE9tYXUvZGgvYlZGTWN6akVp?= =?utf-8?B?WnRXS0ExUFlHZStDa0RNUHRZT1VwOWxjRkpWN2t1cGFoNzhQK3l6cW1RZFk2?= =?utf-8?Q?M4LKo59lHJZQCAndsgBckmZh+yPRGxswzkNWxQlR+aab?= Content-Type: multipart/alternative; boundary="_000_PAXPR06MB78695C1CF6057EC48042EC03CD6F9PAXPR06MB7869eurp_" MIME-Version: 1.0 X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-AuthSource: PAXPR06MB7869.eurprd06.prod.outlook.com X-MS-Exchange-CrossTenant-Network-Message-Id: 77bc1735-5597-44d8-b91c-08db4aea0fd6 X-MS-Exchange-CrossTenant-originalarrivaltime: 02 May 2023 08:48:55.1274 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: 67bda7ee-fd80-41ef-ac91-358418290a1e X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: vTMuTxhkcJeoO9L7njRlHJ4xIvTEGaQr/OU0TAtNihYcXRLr/ZVSLyv7fXjFjV0+pXJm1xDEaIescVykIu8DkHLvpscl8zCsJP97jjUIyfR8/iHJXOr5+hAPBV8M9arm X-MS-Exchange-Transport-CrossTenantHeadersStamped: AM9PR06MB8083 X-OriginatorOrg: exmail.nottingham.ac.uk X-SASI-RCODE: 200 X-Original-Sender: thorsten.altenkirch@nottingham.ac.uk X-Original-Authentication-Results: gmr-mx.google.com; arc=fail (body hash mismatch); spf=pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.125 as permitted sender) smtp.mailfrom=Thorsten.Altenkirch@nottingham.ac.uk; dmarc=pass (p=QUARANTINE sp=NONE dis=NONE) header.from=nottingham.ac.uk X-Original-From: Thorsten Altenkirch Reply-To: Thorsten Altenkirch 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: , List-Unsubscribe: , --_000_PAXPR06MB78695C1CF6057EC48042EC03CD6F9PAXPR06MB7869eurp_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Actually it is sufficient to construct a morphism to tge wild CWF of types. Sent from Outlook for iOS ________________________________ From: 'Thorsten Altenkirch' via Homotopy Type Theory Sent: Tuesday, May 2, 2023 9:35:55 AM To: Jasper Hugunin ; Homotopy Type Theory Subject: Re: [HoTT] Free higher groups One option would be the solution to the coherence problem for Categories wi= th Families (CWFs). Define a wild CWF as a CWF-algebra with no truncation. = The question is whether the usual set-truncated initial CWF is weakly initi= al for wild CWFs. By initial I mean given a set of generating types and ter= ms (otherwise everything is empty). We don=E2=80=99t yet have a constructio= n for this even using 2LTT but we think it should be possible using semi-si= mplicial types. On the other hand we should be able to encode semi-simplici= al types in the initial CWF (ok we may need some Pi-types) and hence the so= lution to the coherence pro0blem would imply the constructability of semi-s= implicial types. Thorsten From: homotopytypetheory@googlegroups.com on behalf of Jasper Hugunin Date: Saturday, 29 April 2023 at 20:08 To: Homotopy Type Theory Subject: Re: [HoTT] Free higher groups Another example constructible in HTS but maybe not in HoTT is the large typ= e of semi-simplicial types (On the Role of Semisimplicial Types - Nicolai K= raus). This one might be a bit tricky because I don't know how to internally expre= ss that a particular large type is the type of semi-simplicial types either= (what universal property it should have). On Saturday, April 29, 2023 at 11:57:36=E2=80=AFAM UTC-7 Dan Christensen wr= ote: Sets don't cover in a general oo-topos. (You have to be a bit careful about the internal notion vs the external notion, but both fail in general.) There's a good summary here: https://ncatlab.org/nlab/show/n-types+cover/ Dan On Apr 29, 2023, Steve Awodey wrote: > good one! > How about just covering a type by a 0-type? > > Steve > >> On Apr 29, 2023, at 1:37 PM, Dan Christensen wrote: >> >> Another set-level statement is whether there are enough injective >> abelian groups. It's true in Grothendieck oo-toposes, but presumably is >> not provable in HoTT. >> >> Dan >> >> On Apr 28, 2023, Michael Shulman wrote: >> >>> The existence of hypercompletion is a good suggestion. >>> >>> Also I realized there are set-level statements that are already known t= o be >>> true in all Grothendieck 1-toposes but not all elementary 1-toposes, su= ch as >>> WISC and Freyd's theorem that a small complete category is a preorder. = So >>> those will be true in any Grothendieck oo-topos too, and can be presume= d to >>> fail in HoTT. But it's nice to have one that involves higher types too. >>> >>> On Mon, Apr 24, 2023 at 5:37=E2=80=AFPM Dan Christensen w= rote: >>> >>> A not-so-interesting answer to Mike's question is the type of delooping= s >>> of S^3. The reason this isn't so interesting is that it's in the image >>> of the natural functor from Spaces to any oo-topos, so it's true just >>> because it is true for Spaces. Similarly, a statement asserting that >>> pi_42(S^17) =3D (insert what it is) is true in any oo-topos. Another >>> reason these aren't interesting is that I expect that they are provable >>> in HoTT with enough work. >>> >>> So, I'll second Mike's question, with the extra condition that it would >>> be good to have a type for which there is some reason to doubt that it >>> is provably inhabited in HoTT. >>> >>> Oh, what about whether the hypercomplete objects are the modal >>> objects >>> for a modality? I'm throwing this out there without much thought... >>> >>> Dan >>> >>> On Apr 24, 2023, Michael Shulman wrote: >>> >>>> This is fantastic, especially the simplicity of the construction. As >>>> Peter said, a wonderful way to commemorate the 10th anniversary of >>> the >>>> special year and the release of the HoTT Book. >>>> >>>> Relatedly to Nicolai's question, this question also has an easy proof >>>> in any Grothendieck infinity-topos. Now that we know it also has a >>>> proof in HoTT, do we know of any type in HoTT whose interpretation in >>>> any Grothendieck infinity-topos is known to be inhabited, but which >>>> isn't known to be inhabited in HoTT? >>>> >>>> On Fri, Apr 21, 2023 at 5:25=E2=80=AFPM Nicolai Kraus >>>> wrote: >>>> >>>> Hi David, >>>> >>>> Congratulations (again)! I find it very interesting that this >>>> question has a positive answer. I had suspected that it might >>>> separate HoTT from Voevodsky's HTS (aka 2LTT with a fibrancy >>>> assumption on strict Nat). Since this isn't the case, do we know >>>> of another type in HoTT that is inhabited in HTS, while we don't >>>> know whether we can construct an inhabitant in HoTT? >>>> >>>> Best, >>>> Nicolai >>>> >>>> On Fri, Apr 21, 2023 at 8:30=E2=80=AFPM Jon Sterling >>>> wrote: >>>> >>>> Dear David, >>>> >>>> Congratulations on your beautiful result; I'm looking forward >>>> to understanding the details. Recently I had been wondering if >>>> anyone had proved this, and I am delighted to see that it is >>>> now done. >>>> >>>> Best wishes, >>>> Jon >>>> >>>> On 21 Apr 2023, at 12:04, David W=C3=A4rn wrote: >>>> >>>>> Dear all, >>>>> >>>>> I'm happy to announce a solution to one of the oldest open >>>> problems in synthetic homotopy theory: the free higher group >>>> on a set is a set. >>>>> >>>>> The proof proceeds by describing path types of pushouts as >>>> sequential colimits of pushouts, much like the James >>>> construction. This description should be useful also in many >>>> other applications. For example it gives a straightforward >>>> proof of Blakers-Massey. >>>>> >>>>> Best wishes, >>>>> David >>>>> >>>>> -- >>>>> 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 >>>> HomotopyTypeThe...@googlegroups.com. >>>>> To view this discussion on the web visit >>>> >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/f2af459c-53a6-e7b9= -77db-5cbf56da17f3%40gmail.com. >>> >>>> >>>> -- >>>> 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 >>>> HomotopyTypeThe...@googlegroups.com. >>>> To view this discussion on the web visit >>>> >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9= -A70A-51CB84BE4B6F%40jonmsterling.com. >>> >>>> >>>> -- >>>> 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 >>> HomotopyTypeThe...@googlegroups.com. >>>> To view this discussion on the web visit >>>> >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9V= ZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com. >>> >>> -- >>> 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 HomotopyTypeThe...@googlegroups.com. >>> To view this discussion on the web visit >>> https://groups.google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40u= wo.ca. >> >> -- >> 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 HomotopyTypeThe...@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/87zg6qy4gx.fsf%40uw= o.ca. -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/73121272-421b-4dba-943f-b81f32854862n%40googlegroups.com= = . This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law. -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/PAXPR06MB78693F3A96A29DB127C274E9CD6F9%40PAXPR06MB7869.e= urprd06.prod.outlook.com. This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment.=20 Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored=20 where permitted by law. --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/PAXPR06MB78695C1CF6057EC48042EC03CD6F9%40PAXPR06MB7869.e= urprd06.prod.outlook.com. --_000_PAXPR06MB78695C1CF6057EC48042EC03CD6F9PAXPR06MB7869eurp_ Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Actually it is sufficient to construct a morphism to tge w= ild CWF of types.

Sent from Outlook for iOS
From: 'Thorsten Altenkirch'= via Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Sent: Tuesday, May 2, 2023 9:35:55 AM
To: Jasper Hugunin <jasper@hugunin.net>; Homotopy Type Theory = <homotopytypetheory@googlegroups.com>
Subject: Re: [HoTT] Free higher groups
 

One option would be the solution = to the coherence problem for Categories with Families (CWFs). Define a wild= CWF as a CWF-algebra with no truncation. The question is whether the usual= set-truncated initial CWF is weakly initial for wild CWFs. By initial I mean given a set of generating types a= nd terms (otherwise everything is empty). We don=E2=80=99t yet have a const= ruction for this even using 2LTT but we think it should be possible using s= emi-simplicial types. On the other hand we should be able to encode semi-simplicial types in the initial CWF (ok w= e may need some Pi-types) and hence the solution to the coherence pro0blem = would imply the constructability of semi-simplicial types.

 

Thorsten

 

From: homotopytypetheory@googlegroups.com &l= t;homotopytypetheory@googlegroups.com> on behalf of Jasper Hugunin <j= asper@hugunin.net>
Date: Saturday, 29 April 2023 at 20:08
To: Homotopy Type Theory <homotopytypetheory@googlegroups.com>=
Subject: Re: [HoTT] Free higher groups

Anothe= r example constructible in HTS but maybe not in HoTT is the large type of s= emi-simplicial types (On the Role of Semisimplicial Types - Nicolai Kraus= ).

 =

This o= ne might be a bit tricky because I don't know how to internally express tha= t a particular large type is the type of semi-simplicial types either (what universal property it should have).

 

On Saturday, April 29= , 2023 at 11:57:36=E2=80=AFAM UTC-7 Dan Christensen wrote:

Sets don't cover in a= general oo-topos. (You have to be a bit
careful about the internal notion vs the external notion, but
both fail in general.) There's a good summary here:

= https://ncatlab.org/nlab/show/n-types+cover/

Dan

On Apr 29, 2023, Steve Awodey <steve...@g= mail.com> wrote:

> good one!
> How about just covering a type by a 0-type?
>
> Steve
>
>> On Apr 29, 2023, at 1:37 PM, Dan Christensen <j...@uwo.ca> wrote:
>>
>> Another set-level statement is whether there are enough injective =
>> abelian groups. It's true in Grothendieck oo-toposes, but presumab= ly is
>> not provable in HoTT.
>>
>> Dan
>>
>> On Apr 28, 2023, Michael Shulman <shu...@sandiego.edu> wrote:
>>
>>> The existence of hypercompletion is a good suggestion.
>>>
>>> Also I realized there are set-level statements that are alread= y known to be
>>> true in all Grothendieck 1-toposes but not all elementary 1-to= poses, such as
>>> WISC and Freyd's theorem that a small complete category is a p= reorder. So
>>> those will be true in any Grothendieck oo-topos too, and can b= e presumed to
>>> fail in HoTT. But it's nice to have one that involves higher t= ypes too.
>>>
>>> On Mon, Apr 24, 2023 at 5:37=E2=80=AFPM Dan Christensen <j...@uwo.ca> wrote:
>>>
>>> A not-so-interesting answer to Mike's question is the type of = deloopings
>>> of S^3. The reason this isn't so interesting is that it's in t= he image
>>> of the natural functor from Spaces to any oo-topos, so it's tr= ue just
>>> because it is true for Spaces. Similarly, a statement assertin= g that
>>> pi_42(S^17) =3D (insert what it is) is true in any oo-topos. A= nother
>>> reason these aren't interesting is that I expect that they are= provable
>>> in HoTT with enough work.
>>>
>>> So, I'll second Mike's question, with the extra condition that= it would
>>> be good to have a type for which there is some reason to doubt= that it
>>> is provably inhabited in HoTT.
>>>
>>> Oh, what about whether the hypercomplete objects are the modal=
>>> objects
>>> for a modality? I'm throwing this out there without much thoug= ht...
>>>
>>> Dan
>>>
>>> On Apr 24, 2023, Michael Shulman <shu...@sandiego.edu> wrote:
>>>
>>>> This is fantastic, especially the simplicity of the constr= uction. As
>>>> Peter said, a wonderful way to commemorate the 10th annive= rsary of
>>> the
>>>> special year and the release of the HoTT Book.
>>>>
>>>> Relatedly to Nicolai's question, this question also has an= easy proof
>>>> in any Grothendieck infinity-topos. Now that we know it al= so has a
>>>> proof in HoTT, do we know of any type in HoTT whose interp= retation in
>>>> any Grothendieck infinity-topos is known to be inhabited, = but which
>>>> isn't known to be inhabited in HoTT?
>>>>
>>>> On Fri, Apr 21, 2023 at 5:25=E2=80=AFPM Nicolai Kraus
>>>> <nicola...@gmail.com> wrote:
>>>>
>>>> Hi David,
>>>>
>>>> Congratulations (again)! I find it very interesting that t= his
>>>> question has a positive answer. I had suspected that it mi= ght
>>>> separate HoTT from Voevodsky's HTS (aka 2LTT with a fibran= cy
>>>> assumption on strict Nat). Since this isn't the case, do w= e know
>>>> of another type in HoTT that is inhabited in HTS, while we= don't
>>>> know whether we can construct an inhabitant in HoTT?
>>>>
>>>> Best,
>>>> Nicolai
>>>>
>>>> On Fri, Apr 21, 2023 at 8:30=E2=80=AFPM Jon Sterling
>>>> <j...@jonmsterling.com> wrote:
>>>>
>>>> Dear David,
>>>>
>>>> Congratulations on your beautiful result; I'm looking forw= ard
>>>> to understanding the details. Recently I had been wonderin= g if
>>>> anyone had proved this, and I am delighted to see that it = is
>>>> now done.
>>>>
>>>> Best wishes,
>>>> Jon
>>>>
>>>> On 21 Apr 2023, at 12:04, David W=C3=A4rn wrote:
>>>>
>>>>> Dear all,
>>>>>
>>>>> I'm happy to announce a solution to one of the oldest = open
>>>> problems in synthetic homotopy theory: the free higher gro= up
>>>> on a set is a set.
>>>>>
>>>>> The proof proceeds by describing path types of pushout= s as
>>>> sequential colimits of pushouts, much like the James
>>>> construction. This description should be useful also in ma= ny
>>>> other applications. For example it gives a straightforward=
>>>> proof of Blakers-Massey.
>>>>>
>>>>> Best wishes,
>>>>> David
>>>>>
>>>>> --
>>>>> You received this message because you are subscribed t= o the
>>>> Google Groups "Homotopy Type Theory" group.
>>>>> To unsubscribe from this group and stop receiving emai= ls
>>>> from it, send an email to
>>>> HomotopyTypeThe...@googlegr= oups.com.
>>>>> To view this discussion on the web visit
>>>>
>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/f2af459c-53a6-e7b9-77d= b-5cbf56da17f3%40gmail.com.
>>>
>>>>
>>>> --
>>>> You received this message because you are subscribed to th= e
>>>> Google Groups "Homotopy Type Theory" group.
>>>> To unsubscribe from this group and stop receiving emails f= rom
>>>> it, send an email to
>>>> HomotopyTypeThe...@googlegr= oups.com.
>>>> To view this discussion on the web visit
>>>>
>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-46B9-A70= A-51CB84BE4B6F%40jonmsterling.com.
>>>
>>>>
>>>> --
>>>> You received this message because you are subscribed to th= e
>>> Google
>>>> Groups "Homotopy Type Theory" group.
>>>> To unsubscribe from this group and stop receiving emails f= rom it,
>>>> send an email to
>>> HomotopyTypeThe...@googlegroups= .com.
>>>> To view this discussion on the web visit
>>>>
>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZV0f= gJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com.
>>>
>>> --
>>> You received this message because you are subscribed to the Go= ogle
>>> Groups "Homotopy Type Theory" group.
>>> To unsubscribe from this group and stop receiving emails from = it, send
>>> an email to HomotopyTypeThe...@= googlegroups.com.
>>> To view this discussion on the web visit
>>> https://groups.google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uwo.c= a.
>>
>> --
>> 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 HomotopyTypeThe...= @googlegroups.com.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/HomotopyTypeTheory/87zg6qy4gx.fsf%40uwo.c= a.

--
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 Homotopy= TypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/73121272-421b-4dba-943= f-b81f32854862n%40googlegroups.com.


This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.=20

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored=20
where permitted by law.

--
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 Homotopy= TypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB78693F3A96A29= DB127C274E9CD6F9%40PAXPR06MB7869.eurprd06.prod.outlook.com.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.=20

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored=20
where permitted by law.

--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB78695C1CF605= 7EC48042EC03CD6F9%40PAXPR06MB7869.eurprd06.prod.outlook.com.
--_000_PAXPR06MB78695C1CF6057EC48042EC03CD6F9PAXPR06MB7869eurp_--