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, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 29791 invoked from network); 2 May 2023 08:36:10 -0000 Received: from mail-lj1-x23d.google.com (2a00:1450:4864:20::23d) by inbox.vuxu.org with ESMTPUTF8; 2 May 2023 08:36:10 -0000 Received: by mail-lj1-x23d.google.com with SMTP id 38308e7fff4ca-2a7add46109sf15702571fa.1 for ; Tue, 02 May 2023 01:36:10 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1683016569; x=1685608569; 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=4xb6paxd1bU7Z5A4RPWIVCz5k8Ja2ItmQ0H+AKqkjT8=; b=q7m+3zWrpsaXIXSBdTLYRqXfmF+P9RjzPrVevugNAqB/Ge5Kx3r2EqhWfqYI67HGkg XgZe5Dlbas1XknXl6gl3Qy5y9lWDQtGOCTenZZBOVQMSoU9JfWMJDhILkNNprEfLrvye pAwMVkjelDsBb+9M1YNrdd8R/3CsDB+LKSSK7aDOTj85ezCFktvwpQuf7pgNSQzhAs4R IwZ1uQ5SHh3duT9LQQYJ+exWMLWJlEi522dmzbU7IHv4LqefsfeT/n8L0/7gmf2CBibw IMWAOD8Sv50YD0PDNw4lsm1YjpkrKqE04wZjLehGKWJR74mE0SmCX0b6icjSVqK0xP8m +Zfw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1683016569; x=1685608569; 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=4xb6paxd1bU7Z5A4RPWIVCz5k8Ja2ItmQ0H+AKqkjT8=; b=CElEqBqSInZdNfM1NDcvv+N5BEvfVqMWvyHtBaCjCELNgV1VbcdaN+/DtJ7BX0FDBd 24a8ptblxZAuGlSOM+b0F/KaHHT3bArGPjT+rGOC0oMfbyRcxsklmwHam+EZyNoQPsB6 zbCd6BLcTr3K0IYXXlb6gePwxrK17SL/tbyoVOEFPsLvM0hUmXTVNoxvGqQ77+yFp59i Nrc+gGGgFlBt3vWP5mTXIL85mR2BgIW70OWJurrmCRYv5EMDDwijhpRqRVtB08Ltj8VZ 9gn7XRbsepbPwUJ1VaVaSwQRN5KUehlZryJxa0kID565U7aJWTucUJmzBNdKwcdKYrBq jdSQ== X-Gm-Message-State: AC+VfDy3j13BAtq+hiq1vbkyXuYnoVgxNomgtrvjSWTERt4eDTLoxtgr SROg709NR48XnMD39P+xhAs= X-Google-Smtp-Source: ACHHUZ67GD5lKIMyfdowofpiY6YT9LEiqS69LGgo/l9zSq8S+sgJJ7F/LtSBfHU3w+9tXGxy2R0T0A== X-Received: by 2002:a2e:6a1a:0:b0:2a1:d819:f0ae with SMTP id f26-20020a2e6a1a000000b002a1d819f0aemr3804236ljc.9.1683016569608; Tue, 02 May 2023 01:36:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6512:39c2:b0:4ed:c108:7214 with SMTP id k2-20020a05651239c200b004edc1087214ls339163lfu.3.-pod-prod-gmail; Tue, 02 May 2023 01:36:06 -0700 (PDT) X-Received: by 2002:a19:f503:0:b0:4f0:7d5:1723 with SMTP id j3-20020a19f503000000b004f007d51723mr4969449lfb.42.1683016566251; Tue, 02 May 2023 01:36:06 -0700 (PDT) Received: from uidappmx06.nottingham.ac.uk (uidappmx06.nottingham.ac.uk. [128.243.43.129]) by gmr-mx.google.com with ESMTPS id p2-20020a056512234200b004dbafe55d43si1888407lfu.13.2023.05.02.01.36.05 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Tue, 02 May 2023 01:36:05 -0700 (PDT) Received-SPF: pass (google.com: domain of thorsten.altenkirch@nottingham.ac.uk designates 128.243.43.129 as permitted sender) client-ip=128.243.43.129; Received: from uidappmx06.nottingham.ac.uk (localhost.localdomain [127.0.0.1]) by localhost (Email Security Appliance) with SMTP id 296B22B7C67; Tue, 2 May 2023 08:36:05 +0000 (GMT) Received: from smtp4.nottingham.ac.uk (smtp4.nottingham.ac.uk [128.243.220.65]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by uidappmx06.nottingham.ac.uk (Sophos Email Appliance) with ESMTPS id 03CD6419838; Tue, 2 May 2023 08:36:04 +0000 (GMT) Received: from uiwexedg01.ad.nottingham.ac.uk ([10.159.172.13]) by smtp4.nottingham.ac.uk with esmtp (Exim 4.94.2) (envelope-from ) id 1ptlUR-0002Np-TS; Tue, 02 May 2023 09:36:03 +0100 Received: from UiWexCHM04.ad.nottingham.ac.uk (10.159.186.8) by smtp.nottingham.ac.uk (10.159.172.13) 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:36:03 +0100 Received: from UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) 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:36:03 +0100 Received: from UiWexEDG01.ad.nottingham.ac.uk (10.159.172.13) by UiWexCHM01.ad.nottingham.ac.uk (10.159.186.12) 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:36:03 +0100 Received: from EUR04-DB3-obe.outbound.protection.outlook.com (128.243.226.54) by smtp.nottingham.ac.uk (10.159.172.13) 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:35:57 +0100 ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=keQ3ZU3wmpzCsCOV5FMMLPW6T8sAyZSVBumszp2nNp/iGyTh9PQTLlJkxUC+04ysdAcq1UNiV/AI+FDOzaBSFl1KMd+8mD6SDD88sHuI9CvVjNq9ExLiXZvkBHJnVkZtoR5FOpGDCrtT6q8Rr5LjyNTYPcUbS0g+3Eg+B274JogFHlUoefDrlMbZe4NEk6D++ZsxW0s5s0GVF9x+hDlhLeZJnbv4IFs8B0rcj0wvBDQxjeiFH9nO8nb4EcvJV8FFlAZpTf7+cc2dJFfalRV4Kxg4EG3lATMBaVSnDiBUGFTyr8DOH6ndtPkmjiwccwoWEiAgKyrCQQ9Zuwh62U2e1Q== 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=Hn6/LAFU2AqNALIGES14oozj3lQVpwCWjr4nkHT22vQ=; b=AmZqpQ9spmO0WrZ2ZIErFYuSC/nVl0+7jUAIUtqGKQve7JCHbqP6dNDIDB6Pu3qFjkN7dA1OLKmbAncnKXEfGj28CFlEcjRBggTIKIycTbtxGeeZPUdErWEfX9hRTPYsYQdDbV5dhCltDMHcphixAXCaKj/l6MyirBlnr2741oG8pUfGYSSyHJoWgjf833KvjDBxPkK/x14nSmnsz5WEYgHoIVmqmB7r/o5pQO/h7Tydb0s9wRC33Jrdmk5GAqE9wdcZgPPPQp6c60DHfLbBW6e21+S8bEMWw3wBxHKA0OZ6U3coJhD+YCeDr0+F/f82o7e6NIINELFit7bHmC9/Ig== 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 DB7PR06MB6072.eurprd06.prod.outlook.com (2603:10a6:10:5c::25) 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:35: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:35: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: AQHZdDivU07vMO5vwU25kyIDAE1cha9CsxWAgAQFAO8= Date: Tue, 2 May 2023 08:35: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: <73121272-421b-4dba-943f-b81f32854862n@googlegroups.com> 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_|DB7PR06MB6072:EE_ x-ms-office365-filtering-correlation-id: 0b6e6f35-1683-45ec-04e0-08db4ae83f02 x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: Kycp9SlsB4zIS8ydkZU64oY6SAThKehK4HO8j/hKMu8t6U0+m+Maan2nrr3RjydZkDCLqrfDIf/AOofVknXklZSQI+e6J6zAsKVRb72ZFROZ8EwwQ25cu0k8z0IJwRiaRr5t5Z9y6z+BYHDV/6jEiP1ls3lftsKVrXosqCHraSnlYXq//wCjGF9OyGvMpqK2c0W+JTvq7YvltX87qvphPZTWiwRAYcvnvQyZAsbZYd2X1tP8PcTau42JWOXcoNKyoPlyrh3n4xVk4yJ1r0q90SmDbfB3cxgEsuqcvte0h97LTdKRVQr/qhp8rx3so/4NeitoaopRcN416uYO35ZO+TO1dKHri+kzRgFFbglFVbJkzpqTO94Qr27LrWUMn+XwkjWA6F7DtujrHEIC55pd4eZYeq2pjhCGEGrYgpsV//g/u8m0JwSD65JKmLDm+QMwAbakQVUb0kdySMNImJ2L6jcPcEWN9UylRPqQ4AFgk15cYwkMdtoxGis3LeNjYFBd7o9m5Mo2aJ1MoVT32NZKRrvzJ3BfHTBvHxxeYYLiKdpJoU3YmoD40LimPYx55jRerU2AZuMHIw8ns53SLTLqF1XS6f5/ZXTWch+rbcNDHp8= 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)(376002)(396003)(366004)(136003)(346002)(39860400002)(451199021)(186003)(2906002)(26005)(53546011)(6506007)(9686003)(86362001)(38070700005)(166002)(122000001)(41320700001)(38100700002)(33656002)(66574015)(55016003)(83380400001)(478600001)(786003)(316002)(71200400001)(7696005)(41300700001)(966005)(64756008)(76116006)(91956017)(66446008)(66946007)(66476007)(66556008)(8936002)(8676002)(5660300002)(66899021)(110136005)(52536014);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?utf-8?B?RVNvMytvMEFNWFBLaGdZblI2SEdNckZCUm5kZjJQeHUySHdxWWJ1VTg5UzU5?= =?utf-8?B?VUo1bHB5eW1NRzBPT2Z0ekF0b1lEYXQvYVgvZHdaNllMN2hUbDNxckZJcEM0?= =?utf-8?B?b1FwZkw0a05MVUR5U2g3WmI2RnNMYTd6V1hiREoxM0VZeEExWXk5a0dkbWk2?= =?utf-8?B?eTI4cDBCOHp5Q0tkdi9BN1ZVdDRvM215ODg3K3llcW9BZ2xFZDNxdE4vb3ZC?= =?utf-8?B?dFJnYU12VmNObFZTbW92RWREZ016OGoxYWNVdGFnMnhKUXNrR2FEdkxDLzhy?= =?utf-8?B?V0JNNWdDQVNLUnExam5yUEdkZHpsZHlzYXRsTmpESS9oRndTbEFtV2R4YkhN?= =?utf-8?B?eGJKaWE2bnFHRnZhNzAvdkI4TncyWVhxNjJ6eDY3dmd1V1hidCtpU21iU1ly?= =?utf-8?B?RVhFZDZYVWRheStDNG40azEvL0MwaVRWb1hUYjMxbC8ycHpxWnpqVFR3RWJu?= =?utf-8?B?UzVQL0cwQVJBNnphOTE0MlB3M2JLUENsR0k0TEVnSS9WS2s2cWdqTVhXa2cy?= =?utf-8?B?MGxLLzlDemRvaEtmRG1nclRqRHdBSWZJcVd3ais3a3JFWlRIQjVTRGdqekRm?= =?utf-8?B?b1NSd3RhaVQzWjMzZUdBenBBSytzTUVMRzhScTZuRGNHdXplM3RFNGduOFpx?= =?utf-8?B?bU1wdDhMRitvZVduUlBUbEJrbElUZy9iZWRJSXRBbTM4aEF3UFd1Vm92d09L?= =?utf-8?B?THVQM1BRN1VIMTdUemprUTRFSHFYMlJ3VWtiZTkySVRjSjdtWG9KMFh2aU1H?= =?utf-8?B?eDUzRnBEZFNreVBaUDVGeDVlMnhBQ0dKNFhvSVE1dEFEK2pVSnkvYk1GSVB3?= =?utf-8?B?MkE5cUM0VlQzK1d0WnlDVUVJMVlpOHBzRFVwYTJVWnd0Wjg0RDBPeHQ1bXls?= =?utf-8?B?cHBDUmpCYTVpT2pBSWxQVVJ4UVpKRzl2bmxQMkUyS2dYVklxVStrVndKVy9X?= =?utf-8?B?RW9kZzM1OXNHU1Q4VHJuOUtwQ0N4RlczY2prdW1FVHkwOTFaYjRtN2M4ZnUx?= =?utf-8?B?SkdyaXA2WUdkWjQzd1RlQlRHc3IzUHZQR1NhS2JXN3Z6eFFUNFlPZHA5TEQ1?= =?utf-8?B?Q0MzS3ZuMFlyU29BSndCZlhYVGlyRXpFU283MHllUWlzcWREdFEvZ3FRUng3?= =?utf-8?B?NWZldVJiZktja0RTOEZRR2ZNNkxpYlo2ekIyNHhkalNoSVMxSXRBSlhzR2hi?= =?utf-8?B?RENkMGVhdVlrMEJ6ZjliSHJDMkdWWGxETDBITWdYZVllL1RNZXprWjJGOW5r?= =?utf-8?B?NVpLakRzOVh3THpwVUdCZ1dFZTFHSU5zWTgwSWxuYTgrRjI5OWZTWUZxbTZi?= =?utf-8?B?N0JQb0VjeWFjRUp5OGVOSjU2SHJuUSsxbE0wMmFyQldpMXhKaTNrNFJUUGxC?= =?utf-8?B?YUhWL3hiY3pTRmo3QW1iVTZJL29mUG9DbzZQSXFQNGpMa1ExN3U0Z1Z2RHpu?= =?utf-8?B?czgxeVBkbXA2eFlKS0ZNYWFYS09MaUhPcWdPdFhSYTJDU3djZ1RUMEl3TXNE?= =?utf-8?B?Y1BFOU5JSEFyaVp6ODBPblJQa2RsTXlseTNCVEdtRnUxakpDcVBEaDVQR3hS?= =?utf-8?B?VzlPTmIvSTdxajJPVWNoWjYrQWtkbU9yRGVQancyK0FGL3lKUnJkNE9QWlJB?= =?utf-8?B?ZkNidFRqTGVvZGNyOUxlSjZzQkpES1o2MkU2Mm8wdFRQQzdVUWsycEl5RnZl?= =?utf-8?B?bS9HaFl4by9zdFQ5QmRza2E2dXZadmhiSHdsY2JXd29uL3BldTNpR29HaExY?= =?utf-8?B?ZHE2aXpmdnVIeEJTWHhBbUNtNzErMWZRb2FFOVdSM1JIUzk5TWFZWkpHZEJ5?= =?utf-8?B?OVVCOW90N2ZGMmpESC9pTmNLdWFEdDVJa2ZLd3NaTXQvUCs2cEJ6ZHg1emkw?= =?utf-8?B?WHZQWW9zN21ndFV5My9rb0F6YlR5SHorT242ZzNUVzl2U3gwZ2pzN01nZ2tj?= =?utf-8?B?U1BLUVNna3lyNjFKbTBTWUlNRW1UWERZTitwTy9ZcEJIclozS29reml0R2xo?= =?utf-8?B?aVFOY3Zxd0VQZksvSFphSERreVZWbi8vdVBGSDh4Q1hnTER0OXRTdWg2aURl?= =?utf-8?B?dVdHSThLT3FXdmtnU3hkdmExR0ZsUHdyYjU3ZFpTRWVMeTJWd3l4RVNVNHpk?= =?utf-8?B?aitNb0FnNXFlOEZPUjBXQzY3SGlsd1J3Sk5SQlc5Ui9yM24rN2xUdUVsanpC?= =?utf-8?Q?w0aCqXsXXl7kn7ZRYC5TZR6FvBSmwLV9xwW8/lPhZDjE?= Content-Type: multipart/alternative; boundary="_000_PAXPR06MB78693F3A96A29DB127C274E9CD6F9PAXPR06MB7869eurp_" 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: 0b6e6f35-1683-45ec-04e0-08db4ae83f02 X-MS-Exchange-CrossTenant-originalarrivaltime: 02 May 2023 08:35:55.2438 (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: g2nqxe4NiMco5s0HvhCnUlyF/3jDZ50oB6ZGvK0DUKfghlY+9AL8h9jspMo2VVhcXpxJkqVgv7k4HQPlVe7DaiX4hNI6KKe785W3qbgyPmotMINRb825ffG5qySyqC1J X-MS-Exchange-Transport-CrossTenantHeadersStamped: DB7PR06MB6072 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.129 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_PAXPR06MB78693F3A96A29DB127C274E9CD6F9PAXPR06MB7869eurp_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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.=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/PAXPR06MB78693F3A96A29DB127C274E9CD6F9%40PAXPR06MB7869.e= urprd06.prod.outlook.com. --_000_PAXPR06MB78693F3A96A29DB127C274E9CD6F9PAXPR06MB7869eurp_ Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

One optio= n would be the solution to the coherence problem for Categories with Famili= es (CWFs). Define a wild CWF as a CWF-algebra with no truncation. The quest= ion is whether the usual set-truncated initial CWF is weakly initial for wild CWFs. By initial I mean given a set= of generating types and terms (otherwise everything is empty). We don=E2= =80=99t yet have a construction for this even using 2LTT but we think it sh= ould be possible using semi-simplicial types. On the other hand we should be able to encode semi-simplicial types in the= initial CWF (ok we may need some Pi-types) and hence the solution to the c= oherence pro0blem would imply the constructability of semi-simplicial types= .

&nbs= p;

Thorsten<= o:p>

&nbs= p;

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

Another ex= ample constructible in HTS but maybe not in HoTT is the large type of semi-= simplicial types (On the Role of Semisimplicial Types - Nicolai Kraus).=

 = ;

This one m= ight be a bit tricky because I don't know how to internally express 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 wrote:

Sets don't cover in a g= eneral 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...@gma= il.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...@googlegrou= ps.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...@googlegrou= ps.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.c= om.
>>>> 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...@go= oglegroups.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...@g= ooglegroups.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 = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/PAXPR06MB78693F3A96A2= 9DB127C274E9CD6F9%40PAXPR06MB7869.eurprd06.prod.outlook.com.
--_000_PAXPR06MB78693F3A96A29DB127C274E9CD6F9PAXPR06MB7869eurp_--