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.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE,T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 5283 invoked from network); 25 Apr 2023 00:37:43 -0000 Received: from mail-lj1-x239.google.com (2a00:1450:4864:20::239) by inbox.vuxu.org with ESMTPUTF8; 25 Apr 2023 00:37:43 -0000 Received: by mail-lj1-x239.google.com with SMTP id 38308e7fff4ca-2a9f8f4ce01sf16328481fa.3 for ; Mon, 24 Apr 2023 17:37:43 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1682383060; cv=pass; d=google.com; s=arc-20160816; b=lXRYwF040V0XLK9oPY8oUpOtrTLqJhNnqMOwl/5wW7AChxtm3UjwiHELINMZT+iNIm oZVjBIF5CZO7+duS5PNWp1OKGaiRW1/6YvkShWSjwKLSL8QGD+HNJIJ3iOIUemhkvyKD k0UF6xAhEi6wmnpMnXCdpCWFffDqFwQ9ypyfgup53BdDfoAd6LZm9uiM9giT4S8hoKIR 0Zp44aZ/LjiXLFpswMvlRR1x9DjT0msOWypoWv7+01AaPKcZmCiLRdIHgbT4yh2jZfy2 myaI6YSTK/2bGgFKQzTnt0DkZaPOYElKPQax6cLdDwidtdxKywmb0V9WWX3QjU8dgkk5 EVFg== ARC-Message-Signature: i=3; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:mime-version :content-transfer-encoding:content-id:user-agent:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:to:from:sender:dkim-signature; bh=L9kwKiPQTg1bas/KGSSyD2yWumpMC8B07zo+3X8BlD8=; b=vZE/PywxNtNIwtOTkk+HYdnhM1Gnm0q1iG5KgngggUuGY4HoUgHpL+mkBDVyzJb4Z0 qS6omjvSX7/KlWGDrxQlzVyR3ghO+xm8Qzd0Peu60jKac+qNDe2bK1l4Kul6o3+1nDiY MS7MTM10cPR9JbUkfe0OlYWwiV1LiEG8zAuM1AtOSinH95jj10uj1bp/mulsvNYv2qXm Lc0tcMmlOhGKEZrKEkN8Nb/GyO/6jpDxMg+/6WUjG4koTnLffhM1cm6Bqs4HxYjACQzZ 6N8CYma0osSMvbzqC520WBECMAMfFBXJ39AafqipYPfxiJgQqIeumdu2jZuRzsHp5xJF IOiA== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=Z1Et+aRa; arc=pass (i=1 spf=pass spfdomain=uwo.ca dkim=pass dkdomain=uwo.ca dmarc=pass fromdomain=uwo.ca); spf=pass (google.com: domain of jdc@uwo.ca designates 2a01:111:f403:7053::724 as permitted sender) smtp.mailfrom=jdc@uwo.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1682383060; x=1684975060; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:mime-version:content-transfer-encoding:content-id :user-agent:content-language:accept-language:in-reply-to:references :message-id:date:thread-index:thread-topic:subject:to:from:sender :from:to:cc:subject:date:message-id:reply-to; bh=L9kwKiPQTg1bas/KGSSyD2yWumpMC8B07zo+3X8BlD8=; b=gz1iXRbrFOt4mtnlf90lEpnu/oSmfy4YUdg89O6vhGRSQJBy/CG1pKrlUFTEAXuf9t aawDuIgFxXa9uopfGITLzSBeyeD/x1lCeiqGWMrZFXO2M+IGowACMif1pKBc6ySP/x6Z 9KZYk5e+Ys/g1UEoHqeASAsYM8OZvZTWHwRIIi/Q1+c5eC8FcrMrLKuWG5t++oCczrcd miymFUugfz7A8KAcTnS3mfnLbYaUPa5SfEac3+96WkUxqeKrX3b+lCh9rGAQI1EJiUWO ueeK8/cITeUN3ARtPafsA6CsG+o1V2MSkWNpkeMpiWjQqqRqati0rlmVkAPtxNlR6T9c otRw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682383060; x=1684975060; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:mime-version :content-transfer-encoding:content-id:user-agent:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:to:from:x-beenthere:x-gm-message-state:sender :from:to:cc:subject:date:message-id:reply-to; bh=L9kwKiPQTg1bas/KGSSyD2yWumpMC8B07zo+3X8BlD8=; b=OCvTCZBtloilH/zwXErwMxxZonOaQ0gbqhag5FODZtQyIA8qHJxoP3VKgCeGm1lJBC DVMXbyjvM6jouAOALX/KtXGtXTaCjwQHGkjo1M3D4AN4PjNwB8mEr3f+2eSbf1EpQvPF ajxBGrj1j7HjjRWyNFsHIh8kd81HqdvzMO3RY3d8o4kj0CBaPwQxQEakunSgOMA0ghdH 9P8Z+kTSd4GSuN3colbNmLsajSo00mosZYiePC6R1i9YwbbsHiXX4pVYRWGYOrNild9f QZplbVWeadriBm4KB4QzLN8i/R2d/zKCNnIL/mGkI2DCOW4oOl44xAnS5wItcyZ9eTCj 2CAA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AAQBX9e1iHtIWVPf66d34H7+qWE6YxBjFRWRPKPM3btuh40pmIWjuXMY L8v1WZdIuMfhWP1Z7qwoL1M= X-Google-Smtp-Source: AKy350ZjFNcC3KmGJ3E+jDzuY/+Wbx33svRTIc0w8PyrnO339W9FHyMA7QGvDjqLH0Cb2X+88GtpYg== X-Received: by 2002:ac2:494f:0:b0:4ed:d64c:ffd6 with SMTP id o15-20020ac2494f000000b004edd64cffd6mr3501131lfi.5.1682383060197; Mon, 24 Apr 2023 17:37:40 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:bc85:0:b0:2a8:cce:bf38 with SMTP id h5-20020a2ebc85000000b002a80ccebf38ls2530185ljf.11.-pod-prod-gmail; Mon, 24 Apr 2023 17:37:37 -0700 (PDT) X-Received: by 2002:a05:651c:86:b0:2aa:af16:5c55 with SMTP id 6-20020a05651c008600b002aaaf165c55mr2142446ljq.44.1682383057573; Mon, 24 Apr 2023 17:37:37 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682383057; cv=pass; d=google.com; s=arc-20160816; b=MSDH1OSRY5lxPR4WiKxBx3GlCF3UEUbnNpSQgDqQcwggK5sWLXNjZnXiPls9hUXoDM Jrv651arRpI2KRRt8pPfW9nYZSYrxQ9JPTKjvCTLqCHapTQhY5gbQY3lXvTpvz5zlnm5 a3SBbAiQJkKpJLCwsAi5BM5mdxPjgvqiUahzRVmiYGPfkFstxS//IIItOuPUzBBop06v YQhcUk/7vf5HSnjpk8goLIs0H/CxP2arZKfV/ZjaPpFTphecWI7k4rzGW9LLdDbuXaJn 0tN5rw0AaDGOvGUxAaro06rABf4QcHv3V1bGLtbPwnFFa04EURlo8tjDF1PuNZQr3ilA EjEg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:user-agent :content-language:accept-language:in-reply-to:references:message-id :date:thread-index:thread-topic:subject:to:from:dkim-signature; bh=VCA5fbF/6FJwbuyQafHINn71TwYDo4YqDyp/xCgfFH0=; b=NyLQ60lO/r2hSisiJGuWUzSLMfvTToG0c+txfHreove4kyGUjIGZNSgpKeRyZNitGM nQJtfR3sOugkSU4S8fBIflFEvph3qx64jMJA1kT+9gKna4uBRfl7hXAmrRBiolsncE8C rvKi4vQZaJXDks2U+21pb0LFGr166sVBAhEKIFGOcrWeXNG6+2RtmXEjcb1dr1B6SAYb 7UuVXw5nSFFFIZXCVzUYkrFmSWpk23t7c5k5kFlrQxvNpZUVRCZJKA+0v8dUyvx9mSgy Pz0xkTZWwB/vv6aruWnNvIUDD0laZSsFrA8hfHc8XlXinODO19D6yfTlNqX8Ds+efAGm T8Cg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=Z1Et+aRa; arc=pass (i=1 spf=pass spfdomain=uwo.ca dkim=pass dkdomain=uwo.ca dmarc=pass fromdomain=uwo.ca); spf=pass (google.com: domain of jdc@uwo.ca designates 2a01:111:f403:7053::724 as permitted sender) smtp.mailfrom=jdc@uwo.ca Received: from CAN01-YT3-obe.outbound.protection.outlook.com (mail-yt3can01on20724.outbound.protection.outlook.com. [2a01:111:f403:7053::724]) by gmr-mx.google.com with ESMTPS id bz18-20020a05651c0c9200b002a8b4c3cf27si634267ljb.0.2023.04.24.17.37.37 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Mon, 24 Apr 2023 17:37:37 -0700 (PDT) Received-SPF: pass (google.com: domain of jdc@uwo.ca designates 2a01:111:f403:7053::724 as permitted sender) client-ip=2a01:111:f403:7053::724; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=TDZPbnVcd11fortAgNlxX6UN31Uh5qHgEkrrbmM0IzxgY5mZIyIQIf9hX5PVjevNcJMQ9wkf5B7M4YncOC5JHfZd/1/FB75CU4g9zkKg7OdPTu7K2obhk3B/fHGZ3PfM5rYiZKvDPOP2tJSmEwQWxiB9Ghw/9T4Wb4e9NJOpf7Svl+WtE3ASvnh+IwLM+VTr5PDt2QefEPgVBKjos7A7H/HPa20+1oyRMtuFXllSzknT+6+EO5mAoR1yqcvimdY8X17MiHn5L/NxFC7UHX+4Ez8cciRJR/Jqq+Y7XfDfkMWkMMtfsiNg3i4sMbRNElmgvZ/ekN879sVCZfnPsIkv3g== 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=VCA5fbF/6FJwbuyQafHINn71TwYDo4YqDyp/xCgfFH0=; b=f4MEnY/tQ7AKCElgIv7yo+lUO2/NhjSGfwOHlp9rOMW5PFeqJINmsRCfZWAgwuwnnN735iXJz4fw9iWdCOSsBVECXkoLEnPF9VcQI1YALho6q2mH4XcgMoaPwEQsps5D0r3wT4dR49tVSSetVGpbVyI4f3SMaSGkXMLEuRtLsO4XeLdN7yIIN6QP6e90sqb3OdBJn8f5z5d72OO29oIzb79Z0WVW5zJpGi49P5j9AcO6ys5w2MWmxBDcLpgA25Q6U6rl8c/2ew2Fj19Q6RL2YKqhf39QnBm0jtS2Ugou80cc0Bu1w6UXKCPJpYQMrur0LRveEsEry1cVEp10/rt+CA== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=uwo.ca; dmarc=pass action=none header.from=uwo.ca; dkim=pass header.d=uwo.ca; arc=none Received: from YQBP288MB0082.CANP288.PROD.OUTLOOK.COM (2603:10b6:c01:70::8) by YT3P288MB0111.CANP288.PROD.OUTLOOK.COM (2603:10b6:b01:f8::22) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6319.33; Tue, 25 Apr 2023 00:37:35 +0000 Received: from YQBP288MB0082.CANP288.PROD.OUTLOOK.COM ([fe80::dd24:65a5:aca3:a194]) by YQBP288MB0082.CANP288.PROD.OUTLOOK.COM ([fe80::dd24:65a5:aca3:a194%4]) with mapi id 15.20.6319.034; Tue, 25 Apr 2023 00:37:34 +0000 From: Dan Christensen To: "homotopytypetheory@googlegroups.com" Subject: Re: [HoTT] Free higher groups Thread-Topic: [HoTT] Free higher groups Thread-Index: AQHZdw4g2rWi4kqjcEuVFT8IMXqnHg== Date: Tue, 25 Apr 2023 00:37:34 +0000 Message-ID: <87leigyeya.fsf@uwo.ca> References: In-Reply-To: (Michael Shulman's message of "Mon, 24 Apr 2023 17:02:44 -0700") Accept-Language: en-CA, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: user-agent: Gnus/5.13 (Gnus v5.13) x-ms-publictraffictype: Email x-ms-traffictypediagnostic: YQBP288MB0082:EE_|YT3P288MB0111:EE_ x-ms-office365-filtering-correlation-id: b4b361fa-39e0-4c8d-8862-08db4525435a x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: LNvwuCflAnzv5/tJ6iryKcIrZEmwXz8oz5gh4xxSTcprcP9c+pdozs1Ew9i6f/L11XiJtXlxkSi6boeJKikBxENloe/G6uVvrbipb5Rx1NFOq3DgMKLcT8ul2R1TLPE/ED2x8eUc+u+30Thc65t4HlxXfkRTd45duYmrehBJKizwEo9p5BsjSEQ1lVXo/BfjWz+ZzFyzCyiRxRII0TbDVdgxYXaC66/1/lu4zV6zQXoStDnH0+XFggj36PewCQDlP8kW328teIwQ6nhic9xgJUFCR8f8/eU80QwFL3gyRZ9lY50ZAfCldmyS6PiwDH1rRbrAGpbjXJymiI3uSC7tOXfX5vGsQXTlVQcSqNYDJg3EgcQsz+/B41VR1QRZ1O+MRyHzhBzwtia6C3SWPpNR+j5lz281LatlEUVNNA17gwCWdxl2HQOHHt8YgyYRTZKcGfp0zMnZ8xhPTQktE/OHiDe71oQ6+/tqkJvn9OLEVsqwrNTIKn5HfcZ/1Ro7ojh6qvWlTbFr5+kLH8Xn+NsldhEcKcGg9i2aep5PT34aBgF2VXT4iQRvGOnKGw85F2Ki+A4E358WFjzWec3slRC7+ZiJ3LMpTFaOWxa2VIx20XF7hetYtLBgDhLPkDl3r2MHH4keCz+wW4RCOyxNALqIxA== x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:YQBP288MB0082.CANP288.PROD.OUTLOOK.COM;PTR:;CAT:NONE;SFS:(13230028)(4636009)(39860400002)(366004)(136003)(396003)(376002)(346002)(451199021)(76116006)(2906002)(66446008)(66476007)(66556008)(66946007)(64756008)(6916009)(316002)(786003)(66899021)(5660300002)(8936002)(38070700005)(8676002)(41300700001)(41320700001)(36756003)(86362001)(186003)(26005)(6512007)(122000001)(71200400001)(53546011)(38100700002)(478600001)(966005)(6486002)(66574015)(83380400001)(2616005)(6506007)(91956017);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?utf-8?B?aFpCUlA1RlFvbTlqL0dKUGhLeUMxajk3bFhaajlpR09EWjBYL2ZFYWlzYVVL?= =?utf-8?B?aktFcjR4UkpDZTJES0NFb0drcTlQaFRTVDBOam84c3FUUEV4UFVmdzJwNTJX?= =?utf-8?B?cU9RVEhMcmZ1NHVUdkNTN0hIVERUa0lYY2pxRnpZbnl3dkxlRkNKWUVBSW02?= =?utf-8?B?NkxBV0QrTDVhZ3dhYW80ZDV2dnRLalRRQm1ER28zZVl4Y0VPamE4RE5jVE1S?= =?utf-8?B?UUhxNURTbzNYN1JoYnk5UVR0WDR6S1hIUkF3TXhKV21qejBveHRYdHFQall4?= =?utf-8?B?UFNuN1dzU0d4M2x6SFpCclhGa25pNnozUkNuM29pQjV6MUhzdEpHcndGT1lR?= =?utf-8?B?cVo5djkzVEJpd0ZiUFhpbEhIamNFaktrd3N4SjNKclJMZTJVMVdBcTVweERy?= =?utf-8?B?cnpaY3dKcm8yT0FYU3BzcFhyZjY1VGQydTVYZEdSaFJNUHFXRU1WV2swMFpU?= =?utf-8?B?TFlPdFZ5eU5tRjZBaHFxS1FLWkp0VEJtd0hVVGI2ejRSWmE2dHZYVkNYazM3?= =?utf-8?B?UXl4QkhlWGswbTJOQW9Zd3VockR2b1ZhUWh6bGdZMi9MZXBzUkk0dk1ZZUIx?= =?utf-8?B?U1lKUTNuWHNEN0l3STlZTXYwdVI3TlBVbEFXNmxRZW85bktuNmhZZERJLzl4?= =?utf-8?B?U29QMWRiTnZKd3hSalFHdStWSUx2cE4zT2l2VVY4OE54U25maXZBekFISmtQ?= =?utf-8?B?NzJHRnlrNjFYZjdKMEk4Wnc3MXE1ZzJSTHEvaXlsaDFXRHNnLzdTSTAzVkRs?= =?utf-8?B?cmZ1dld3ZHoyQUlvZ2crVEVVSWVubEt5eGFmK2hMVk9kc2hCbXluRnVwK3Rv?= =?utf-8?B?aFV0QmlFMkx4dHVYakQySXNEbDU5alI3dVFSWnVsaDlwcDlwSFVUOEdmMEUy?= =?utf-8?B?RjZ0MEZQQWN4TldMamNmS1Q2N0hjWW1XWEEvZHpyTzFPQUhmMHljYitXajIv?= =?utf-8?B?MmZRcWd5bHpHT3Z1L2JtVFpGcmJWbVUzOWJzR2dwK25BNXJvYU92dmw5OXlW?= =?utf-8?B?S3B4L0RDaXpXcFQ1ZEVxZnQyS2E0YVp0ZVJmR3RZUmJoWW9tZ09DUU1OQmUz?= =?utf-8?B?bUtZSHozR1orQjFNTDNscU94b3R0MDk1T0VDcjBCc2pPQVdLVHdTZGRHWGw0?= =?utf-8?B?UXMwbU9OTDFMVk1GclZ3MU5VNXA5THdrRjdUTm15VTlGWkRMVitzQjkvYXdD?= =?utf-8?B?cFcvdTZkU3RObXBmdVNSaEZ2RjNqWnlRWFE2UU5PYm40M2VuRUtmbld4ZVNT?= =?utf-8?B?Kzdwc0VEeS9aYUo1YjZOaG9nYzdHR05nOGVlL0tJOXl3b3hCNndtcWpkZkxH?= =?utf-8?B?dEd2WHpCbWJsTnYweHFlZ1luMTZTalhMVkRqUUZ2c0hxSGNBdjdrT1F5MUx1?= =?utf-8?B?WUFhK1YxY1Jtb1JhdEx4UkpEVVpQbkdicGx6djU1NE5FbFI5V2pTMS8xZjd0?= =?utf-8?B?SlRGYXhqVWFjcy9UK1pHQkR6RGt4SldzWnVtNlpBbmhRcklDTG1MY1JSRHRV?= =?utf-8?B?OHhlU0JwMloxdjVsNmpabFlNOWs5eVhVZUJjemR1WHRHOWJwbVNiUzZ2SDVN?= =?utf-8?B?V25TYmRHdW85UkZTd1pQV2pBTVpkWnpxQmlINjQzcVVUajNGWTlHMVI2Qm03?= =?utf-8?B?dHBQQnptM295NWJtN3JUZ0E0bUNqRzRHV3lGd2E1WmVPdlk5RkZEd3hiL1ZV?= =?utf-8?B?clNDVS9yS0c1SEQ3eVgwS2RTc1FESEdoY2JxbUNUUjU3bjdZR3BLVXdWYmNH?= =?utf-8?B?d3NWVGFjNkRxa3dpZTd2T2U3TXBRUE5OcGFHSUFPZVJGWk1NRWovMHZWRkpy?= =?utf-8?B?bXI4eGx3Tk52bmlPd0NvQ3d5TzU1R1hUdjNDckNSQjhjLzdlTnd1UWIwbXRE?= =?utf-8?B?Z0YrMVFjUDUwUnY5V01jMElva01xRVpzVHdVdDZnV0NSdW92d3krRTMzODBl?= =?utf-8?B?ZnVnU0UwZzByZTBRMG42RW5MekwyektmMlRVMEJRblFScnlOaHpuVnJaNG1F?= =?utf-8?B?NFk1aFlGUG5reUtqYnpjWk93ZDhuc1hZWml4QjRheXJQZytGeS85TzU4eXg3?= =?utf-8?B?dWtEQWowdjBNdEowSkxiUnR1SjZkeFg3MWRDZmx5QUt6SVY0WVhUVkx6OVZS?= =?utf-8?Q?n5r8=3D?= Content-Type: text/plain; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: uwo.ca X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-AuthSource: YQBP288MB0082.CANP288.PROD.OUTLOOK.COM X-MS-Exchange-CrossTenant-Network-Message-Id: b4b361fa-39e0-4c8d-8862-08db4525435a X-MS-Exchange-CrossTenant-originalarrivaltime: 25 Apr 2023 00:37:34.8817 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: ad93a64d-ad0d-4ecd-b2fd-e53ce15965be X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: 6FdDeDiD6plHCp+nLUo1REZvrZfMqcgAQ0UBJwTMbqfjZxw4xDv2Z3mn7Nj0/7JQ X-MS-Exchange-Transport-CrossTenantHeadersStamped: YT3P288MB0111 X-Original-Sender: jdc@uwo.ca X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=Z1Et+aRa; arc=pass (i=1 spf=pass spfdomain=uwo.ca dkim=pass dkdomain=uwo.ca dmarc=pass fromdomain=uwo.ca); spf=pass (google.com: domain of jdc@uwo.ca designates 2a01:111:f403:7053::724 as permitted sender) smtp.mailfrom=jdc@uwo.ca 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: , 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 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 > > > > --=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. > > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/f2af459c-53a= 6-e7b9-77db-5cbf56da17f3%40gmail.com. > > --=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. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D13= 4-46B9-A70A-51CB84BE4B6F%40jonmsterling.com. > > --=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. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G= 9VZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com. --=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/87leigyeya.fsf%40uwo.ca.