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 6694 invoked from network); 29 Apr 2023 17:37:42 -0000 Received: from mail-ej1-x63d.google.com (2a00:1450:4864:20::63d) by inbox.vuxu.org with ESMTPUTF8; 29 Apr 2023 17:37:42 -0000 Received: by mail-ej1-x63d.google.com with SMTP id a640c23a62f3a-95c3f20df2dsf97992466b.1 for ; Sat, 29 Apr 2023 10:37:42 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1682789861; cv=pass; d=google.com; s=arc-20160816; b=ymCF07Axxo74SKxOhnhwgrRtsLmK549LcOotYPdYZuXnzjJkDczRQ50wS5MdPPVxLU R0muD0y37VPc6bocHVlUeo6N+a73cjhUU/ZCq78MePSdVx8jf1UI/N1a2JvtoyXFG8L4 b+yqrBySZXCynd7t+7dLBAyF+511TH+/kKSWrAD2T+rA8YGzmS21+cVIuq7kl2r1B+3h RwY6BpMwe1GUAoUXq3E+u941W4CGqpEe0XB7iKF5ALBZN4oXvWSdiY89ZKXX9ecU2XO3 HW9qSA5cOX5VRPA4sa9YOzLC3lLJnbjT93Lv7stmPtrYmMPseTFwIcXwQmTNQ+lh/zho Mu9Q== 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=xM54kesSOwXE6JTdvLF10/Rs2bIm3kEbILPHMFnkw5M=; b=FR/t6xyyy1qEvBaov/2bR76uRP11C9SiqM3MdsQEeeP6EqhmXifsaP94/ClkPo2IGD Ess6O9O34fbKa1E1iWFoH6jFtwCVLvPucc1ULtJcYGl/gVfFiQ+n95EUYfVDNsHc22Qd DW2JOP2DBi3ighsP077OITLkWmlNW1EF6ZOm+PHRG02peWaMRHb9b/AR2n+dJg/tO6uU W7m/R4Mun0RqmvBVlYpXwuCakyAzBJp0o1c8g5+XEYagR25b5MeHmqfn7r3QbQGycKz/ otfCqbyiGceJ5W/NEp2GVffWORjcJqxgzJOClLtF1rgD4cCU0DfCAolB40Z7rPIYIHfF eU/w== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=enX5oDPC; 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::72e as permitted sender) smtp.mailfrom=jdc@uwo.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1682789861; x=1685381861; 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=xM54kesSOwXE6JTdvLF10/Rs2bIm3kEbILPHMFnkw5M=; b=rWVqUUcinT/BZMGyIBSnn6zaPkJWk4ButUXVs/VGyHqteDwhteED9eQB87sEIGPEta DsvVtMdQc15nsVivvLnvGc3Pyp3mzv/RLEPnTHdKOBUh7jF2Z0iEx1c8Gc1v+703hEDk 9JLogqsoVMAfyGYJGudMnWHhc92cIcRNPUNo87StKwkWvP2+X9QN5neArJO8aYKkrGzw LdY/KqB8ucW6ll3BZafXBZo9H7sccPEVgLVPRNwtPY/ya8M+lnEeJUpPkPiGosE2J2Kz 3vNxP2wmOBB7RmDCLUslQ4A07kwf0wu1WKOkuXsHbA/x7K3IXfyl1KYTqeIyPYJMHyCT AMiA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682789861; x=1685381861; 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=xM54kesSOwXE6JTdvLF10/Rs2bIm3kEbILPHMFnkw5M=; b=SvzoTP8UuXxOttkEh2wODeEb37Tkck9koyMr9c7NWcBamaSXnEHRygvZnVQci5pomx kUSA4BYokxgJzcisawBaJUJ9KEn7cSBLye2Cj7Zz8FtV+STUNDaJUsIxWQlPS8vXgQEy 5ENzMH7OYsuCUD3LGo4QYCf8CuniGr5KnPEbA95bmVl+4sOWi8P8hhf3MlPp5gOocjps 9nhTdiQEsaZ710MNhwUdZXFDC44778IlB2SQjCdCy1ks1ciuPehClrYrB1LZwn8Tto8l tCMdjKl+1MlznKqa3RcyzRxkJ6ZIjUBo+CExiadVYsMxcgGD/hRJc23itqwLyHk3A1Cu dmjQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AC+VfDxuaXDjj+i5xbxbJiQ0aGTt7MKhazVMF6CJ+JKJiqqSRQ8ysrzs pnF7yLqzFOL8u/1HNg5FGXY= X-Google-Smtp-Source: ACHHUZ6AJliXUUeWkmV5g4fNSyJlon1z0Y/8bGViDZZWmO9s1EKOiIQkYugB0ImCYS+eT6frUs9cCA== X-Received: by 2002:a17:907:2c62:b0:94a:5d6d:969d with SMTP id ib2-20020a1709072c6200b0094a5d6d969dmr3509165ejc.8.1682789860570; Sat, 29 Apr 2023 10:37:40 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:3f14:b0:949:87f1:f4ca with SMTP id c20-20020a1709063f1400b0094987f1f4cals2418766ejj.5.-pod-prod-gmail; Sat, 29 Apr 2023 10:37:38 -0700 (PDT) X-Received: by 2002:a17:907:805:b0:95e:f737:d76c with SMTP id wv5-20020a170907080500b0095ef737d76cmr8966755ejb.13.1682789858011; Sat, 29 Apr 2023 10:37:38 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682789857; cv=pass; d=google.com; s=arc-20160816; b=z0NqDKTHds/xRCxq/Q9NZP26Bjy2/xaAhfj3BIAlHBJnmGeRql3P5PxImUQFozhLEm HZdeEqFFxD/mz3umjML9MyyDeb6aHjqw8b9nI+ARforiuj41/V3xvsbwBKiP9et6MyG/ /mAfU0N+7s1ADUo+OKf+VIhTHcXwlWZGG4ArHC/3rs9veecz4LtGi9Q0G73WKxLV6G3O 1ow9Z6vUoIbbLv/H7pZleQbZQYqxD7UVu/cz4e5L8obWJiRnlBt+6DNAFkkzFruqMcV+ a4tLMkTlmLSOkGw6TCyWVt6WD8E5Qn564MxcOONBEOnvOIuwj7mJWMsk0R2rS3Cb41Yf jCqg== 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=22qtluiiqk75grxQrZiQpDPQ/EW7XRwwpKJqiAF1f8w=; b=idjT779IBKOtAI/Rl01sW9ovjb2T5sj9DdJtZRDoCKm1ExSWUTVOlz2ldG9sjBzaoL Men7UhBN4nZGZmHPwuD/cQYOPE0RDHbH+juyW0CU3BU0TjpwMQxu8Sui5KfY3ozk0kXS qnWXHERdgN/A/CfQoWKgMNGxqvB0IJkKlph+Nckwjbt/mxzsf91i+RFbBVrP30Aw70E9 WQPwDY2vGJt9MLGPrNIYkm1bLlCIaCbSJCvehdGFIT0t1d1vDfUDZneAdIRQ87Q4IKZQ bw+8g7RovAmHw/lacLibCiwyi8zZP8FnFzluFGLmsbsuSl17UMtVpCOtD/nXG3wVEmgY UJ+Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=enX5oDPC; 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::72e as permitted sender) smtp.mailfrom=jdc@uwo.ca Received: from CAN01-YT3-obe.outbound.protection.outlook.com (mail-yt3can01on2072e.outbound.protection.outlook.com. [2a01:111:f403:7053::72e]) by gmr-mx.google.com with ESMTPS id p9-20020a056402500900b005026ddf3ee3si1433103eda.3.2023.04.29.10.37.37 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sat, 29 Apr 2023 10:37:37 -0700 (PDT) Received-SPF: pass (google.com: domain of jdc@uwo.ca designates 2a01:111:f403:7053::72e as permitted sender) client-ip=2a01:111:f403:7053::72e; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=OuWoaSASvwGeegwwzeZMeKUGTZCseS3Z2rH6zGj6O12F9Lu2xPhFymLyA5ghAeOveMG1Ufr0CEgDO0eNjcgusFbktVckHRgRdpYJknj/3bL7cd7xtGfecTa1n+MlyaofANZ918aI6nuDImaCDotUdvrExplFUv4y+JLP2j4mMzuR+kWxW/bP9obJM2lBE7SsG/StgzpNEwA6Cj88r7QKbPw9RZhOPSSKjBpZxqWE5Ay5K86MJm+ziOPQtSKvpK3oDTSfkZE0vm3jYKK2MFF5GCRllZFEiUA2LGeSWTx/aBurHNQmlL+SSd3GJo40b/BYpvc12YiceuwoKinESyj8tg== 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=22qtluiiqk75grxQrZiQpDPQ/EW7XRwwpKJqiAF1f8w=; b=YVyb5GFV5zQwY6Wzv3i5cKNjcrHWtxrZZI51aYrEPW+BjpraHiQrCksXmDxW6S9IHf5lgzH+Q97nD7pJ9d6jA+z2dmY3IO+KCUfasn3bNpzf5CHK0H4pFFMIELiQoZsBQt1RqPW3lH1oJu05QvcAMt+7dZKKaDeO/2sFZ5v0fJjrd825OYdz+WEggNIMGd+6zkXJ3TswX7Sg4NyksqrJuVxIzzqDis26M8VrEZdsJrLWVWt2nCiYlHRm5n7cUHPgSaezsIFzKkgWwmS768u9L5fniZjnD8bcPlM0tVk8A3YVYn1SaeCnUww5cn87mgoZwWz7FrAUkaCIj7V+TkysUA== 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 YT2P288MB0091.CANP288.PROD.OUTLOOK.COM (2603:10b6:b01:f3::22) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6340.26; Sat, 29 Apr 2023 17: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.6340.026; Sat, 29 Apr 2023 17:37:35 +0000 From: Dan Christensen To: "homotopytypetheory@googlegroups.com" Subject: Re: [HoTT] Free higher groups Thread-Topic: [HoTT] Free higher groups Thread-Index: AQHZesFJ2BSiWWx0ZEO7KLfmkAXudw== Date: Sat, 29 Apr 2023 17:37:35 +0000 Message-ID: <87zg6qy4gx.fsf@uwo.ca> References: <87leigyeya.fsf@uwo.ca> In-Reply-To: (Michael Shulman's message of "Fri, 28 Apr 2023 10:59:48 -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_|YT2P288MB0091:EE_ x-ms-office365-filtering-correlation-id: bcdf08c4-2c22-4b21-d20f-08db48d86b8e x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: yFALNHgmtUbBUmjfSmKwwly4aJCxy4yCcAPtUqGvH7NRobLlzgy+ncjGz6RAS+VOziuGAVd+jYKeVSYOTH6IBwYPN+jNObqw7t9jussS2Se/Mz0Ycjjkm4AO8GG/GJLhJrc5GbjfO5hQIbXQWwIoZa1FAtaY/eO+M2moTC5aeZLSTSnlsD3+2oTY9DloLtdFsKZwnLaynW3gQdZdpWia9COhNxky+v6eqz5sKYZsamuQf86sLPkJy220nALZzquWaMPH9aK1f+EzTmy6p/ZizFyPv1LcI06/LwTA4ShqnASlV5vjsPLsaNrzqIbRg9WhgUv4lMpvO2/cHTBznrzVMGOAJTk9uey8CkCkcPfabhJRHq3t6I/XGPUYvJnE1Shg7aqOY9Hgrv2G14B1dCCS/ta8Da03EsAr9kc+PleK33pfQkYNh/jEK8saTdpWHJimgWTlKDZBpzSN50bTVjx9PGzML0XwXp0nQxGW3p8hS68wCLQwBNQHVjdfDJvEnGjvLTEEnW76za7/n24FCmiNH8S2DAMLKrtMwoD67PvYi5QmVT6gSsOuMdgMHfjx8Y9w1VWGAKOXOQynphC/tPlBVaNtKaYD3kdWI8frosfY9Q2Ohts9TY48NuNaCE7ODs6ZVdOvkuY2aygSUFMoukimmA== 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)(396003)(39860400002)(376002)(136003)(346002)(366004)(451199021)(66899021)(36756003)(86362001)(38070700005)(38100700002)(122000001)(83380400001)(66574015)(2616005)(53546011)(6512007)(6506007)(26005)(186003)(6486002)(966005)(71200400001)(478600001)(91956017)(76116006)(66946007)(66556008)(66476007)(66446008)(64756008)(6916009)(786003)(316002)(41300700001)(8676002)(8936002)(5660300002)(2906002)(41320700001);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?utf-8?B?NVRweEJqSXNjOWpLOVRPT1dxZ1Vma1hvZG9QSTMrZzdoLzRkSkhid3duKytk?= =?utf-8?B?N0lXbk1lQ05yczBVa3ZBY25jbHFpaytwaDhYaUxXdzg4OHRFRW5MeXRuYklj?= =?utf-8?B?NWhkbHpiOHVCVnZWb1JEY0lhT3ladnZXSkQwcWcrTWg5K0IyMnljb2xCb0dF?= =?utf-8?B?QTFlWStoOUwrTWt0dUFIZlJHdWdybG1FWVZrWDlGQTk3a015MG5VTnVvdDZT?= =?utf-8?B?aXpiV000TmdzN3JXT1Qxc2RpZjN5M1hNNnV4U2w0QmFrNExGM1BKMW9nSXVL?= =?utf-8?B?RGExRXU3Q0F4cE9ZYjV0dkRHU0tPcXY3Z2t5d215b1QwRWljZFBKN2JXcUtE?= =?utf-8?B?dnFEUzBFWWNYSmk5bFNlaU1KejVqdlZFZmVPWXNnbjR6eFV6aGcybzZOYTZY?= =?utf-8?B?bXNGenVXT09WdEFSSzZCVDdVZzVyTkNXZVJXSHBIUFBCRFVZUitLdlVBUEZX?= =?utf-8?B?SzRsSmFvUllHVG1saFYzZ3JuOXM0THJCZ1h4SXV5aG0va3I3cXpFVjBESFRz?= =?utf-8?B?THg0Q1AvYjVMUTJ1bFBtYm5ic0lKUkNuSGNyK0RuUHpYZlZrdDBVMkpHMlo0?= =?utf-8?B?MG4wUFFVbXhkMFdoS0cxN2xuVDMxYkgwM3N6Zk9yNkdtdjhmcE1RUkNUcXQ1?= =?utf-8?B?YnpwRUpoMWROUkZ5Nkt1ZFRRSGVPY3V4azg2Y3o3bXMraytBLzl6eFJ2MDNL?= =?utf-8?B?MjdEL2NQYkpHc1EzRmFiWkZQcncwT0VNNTRlN0pHeWk5emxFWEF0T2E2YmVi?= =?utf-8?B?YzZ5ZWhnZjhFNHZNSU1sVExONVRISXhJMzZwV1FzZ3hsU2E5VUd3YnlzSElt?= =?utf-8?B?SEI0c24xNmgyZlBIbVgxVDRDLzRwbnQ3Rk1qZkM2YXdJSGYvaTdVTTR1T2Vh?= =?utf-8?B?MCsycVE4endIWUtIOSthcG0rYlVMSXVIZ0cyODZxVUR4dFFhZkgxeWVZMEZQ?= =?utf-8?B?Y3lEZXQ3dkNJbDdoN24vVWJiT3hEaHVlVzlUVyt4LzZvblhoVUJXZkluUFZu?= =?utf-8?B?N2RkRDJ1bmlTSi93S1pQdUhiZ1V2bUczRGY5cUd3VnBrSXlDbE45Vytjcitt?= =?utf-8?B?U0NPRGhva0FBN3B6M09OUVZIbHh2TFFQYzVyVXNEODhZdFkvS3hFL3NBQkVm?= =?utf-8?B?c09jcEVNS1pWRklubnU1Zy94dWtIaDZMZC84MzB4bmZ1b3ZkdjZ3ZkUrUEE3?= =?utf-8?B?aEg1VGJRMjcyQmlJZnVhb01PbEozSTYyRkJ2WERyWXc0K1pPT1ZiNjh1aDUz?= =?utf-8?B?Y01UQTVFZWpZR2RTNWVUVXQvRld6cFBiL0xHYmdJOVFwQ0N0UFczNzBpV1lO?= =?utf-8?B?RVpSckE0WlRldHUyUU9peWdVUTF4TXZ6dVBZdFdTU3VZRitQdmdnWjNrYi95?= =?utf-8?B?bWlzbzU3eHFpdElCUXFWKzhLZDFrTm1GdlJXaDdjNkRsVWh6a29ZTnpjaEww?= =?utf-8?B?N0tNeEVFMFJsU1pBRW0xaUpZTzZ1dngyVUJEVXBYS0lseitJclpaV3FIUFBD?= =?utf-8?B?cklvWStkdTJRQVdCWXVvTSt2SXo5TENjbEc2cGhmWUNtc0huSnI3dnN2clpu?= =?utf-8?B?bEhnbjR3YjhCOUtSV3VtTzhycUtMUUZlWTkyM1VvaW1Uekh3TVZYVHRpMXpq?= =?utf-8?B?cmtVdk5JQ0JDR2Z1bUpuTTdIeXVBV2IwNHB4bGdZdHpVdk9sUC9JVEhRQ3Ru?= =?utf-8?B?ZUtHMnMwakR5aWJLZEpQakIvMlBFdTdoT0lHQ2crMmR1ZEFiOUMxWFhGTFM5?= =?utf-8?B?VmFsbU93TTBXV2FQemh2bWFPRmordFBMTStVWjFjVU81MDkzdktpbXhOV3hn?= =?utf-8?B?R0ZJRmVjSUtaRUh0K1NBRDhNUDB6VVYxNi9LNkdLZmowalVuZFArdUZnVTlr?= =?utf-8?B?K0duZWxWRjhLb05MZEtvUlp1QUV0TE9BZkdpM2d6OCtqR3pMSkhpeTZ1RkJi?= =?utf-8?B?MWZOM09mdVFmUlRCdkNCMUNPaXZjRm1oc2ozampRcENEdlF0R2cycUlSbW43?= =?utf-8?B?bzhCNlNNQlpHWmUwNlNVWE9CMGdGaThJK2pqb3FwVVI3bjZ6YUtyUi9wdVRu?= =?utf-8?B?UDJZcjdZaXVWMjl5QmNyNm0zNGF1QWROMkZDQ1dTR2dBRnAyYVFHbzh0ZzVV?= =?utf-8?Q?zULc=3D?= Content-Type: text/plain; charset="UTF-8" Content-ID: <0BFA5460F776484CA4AC0C8947962A77@CANP288.PROD.OUTLOOK.COM> 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: bcdf08c4-2c22-4b21-d20f-08db48d86b8e X-MS-Exchange-CrossTenant-originalarrivaltime: 29 Apr 2023 17:37:35.7363 (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: NsRnUw5XU1TW4oCpDhxgme6ZYnsuewBIr3xUvUviyHaFe7vJwBjR0FWbcHx9oNjs X-MS-Exchange-Transport-CrossTenantHeadersStamped: YT2P288MB0091 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=enX5oDPC; 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::72e 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: , 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 to = be > true in all Grothendieck 1-toposes but not all elementary 1-toposes, such= as > WISC and Freyd's theorem that a small complete category is a preorder. S= o > those will be true in any Grothendieck oo-topos too, and can be presumed = 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 wrot= e: > > 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 > > =20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/f2af459c-53a6-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 > > =20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/D102F774-D134-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 > > =20 > https://groups.google.com/d/msgid/HomotopyTypeTheory/CA%2BAZBBpPwgh1G9VZ= V0fgJFd8Mzqfchskc4-%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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit > https://groups.google.com/d/msgid/HomotopyTypeTheory/87leigyeya.fsf%40uw= o.ca. --=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/87zg6qy4gx.fsf%40uwo.ca.