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 10383 invoked from network); 29 Apr 2023 18:57:37 -0000 Received: from mail-lf1-x13b.google.com (2a00:1450:4864:20::13b) by inbox.vuxu.org with ESMTPUTF8; 29 Apr 2023 18:57:37 -0000 Received: by mail-lf1-x13b.google.com with SMTP id 2adb3069b0e04-4edc5526c5esf671568e87.1 for ; Sat, 29 Apr 2023 11:57:37 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1682794656; cv=pass; d=google.com; s=arc-20160816; b=GE6jIB6kOXoDgNlJlT6hztKBg148jkFtlEXEa4EyyzpUa3yux/i2VjhjKbq6VYocP3 b1LZbjhXkBRZy39xGSjOzuI5s+R58C4CMGHZvxw46w8bAmz928XNbw8Tqval8cjcwsW9 JpgsrVbPNkRf/rNkxOU25R+vAvXH8w2rDbLr97aakP4CuwjWfYT8l+YTJ0oblUHBAvV5 cAvHdTzGGbT3gOuh9WYp7tKql56Cbf/LJnjBFwfIc66Jo/kKyRkMZqvSrGupUumsCu6O ol4Btbltv5XijegLcpV8gGko5SKOiEGcMy5I9++XnzVtP9eYWu5gAbvcb65uuzBpy3/7 xQQg== 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:cc:to:from:sender:dkim-signature; bh=DjFyqJ6gsRhtxKsKXxXpDHkfVYSmvKjGiiytaqyJKvA=; b=NZ5Nhv2n2HLYQQ8cyWPExWck4PwQbcH9xjkOnSVFW+onEV8E+cVLyvsrSNB3cLTy9E 6Rfx9z/+JdFynrcghzp0YR/KSOEA4M4HY2vNpDbr31RM8asH/xi4V/e4i4ai7IoPjxT/ 2/1Eo5sOq12+QnHWg6OAOt6NPYXlcXsIQ4HVbvI0SyzdtBgARBfFikhZ3ezGgsJz8+Io B2emF/RvxH88XGGonQoP2utPoBsdIzw2PjbrkE+f1iYdo8KHOMmJOprGRmLG4KzhbYHd SxhQkDr76Ka4I9QwLpx9A0ZfA81Vy1wiakJoVIQgq7hXNbmLUCplYCTvUDp6SLFYlZLH p6IA== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=FwK2fBqh; 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::71e as permitted sender) smtp.mailfrom=jdc@uwo.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20221208; t=1682794656; x=1685386656; 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:cc:to:from:sender :from:to:cc:subject:date:message-id:reply-to; bh=DjFyqJ6gsRhtxKsKXxXpDHkfVYSmvKjGiiytaqyJKvA=; b=T9Gokba+vA5fqb/KXwekl2CX9e0ddMP77p2A7l6+Xgtrk7Nk22Xc/8+lQwQTIe3rel 3hikvtRms2qvtaa6iz/6bTjgrFMhIbY3+i0cowjKRX+nwqZscL6vcLw4miVZlA3/7eqK hGO3rr3IJhBIJsjWYvH0hEqpNsCLfTO7T7r+1uUJJvgG5GpbIFR4kiV1msvAqonCM/gr LHz7vG4lxmds0P/uHw7cPSw+n1ynYeyPz3EwZk7j/r6hfwVlsrzFyMWoZHj69phlB5iO W3LseEwpyub0MFvgNcTk7Z/E3YCBqWQ/1sRjJ3gnMYskcDA/MD8zCHcl0mZHBcq7RXWe HLXA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20221208; t=1682794656; x=1685386656; 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:cc:to:from:x-beenthere:x-gm-message-state :sender:from:to:cc:subject:date:message-id:reply-to; bh=DjFyqJ6gsRhtxKsKXxXpDHkfVYSmvKjGiiytaqyJKvA=; b=QF6r32Q0/Azzw1chFww1xAy7S6qqXzvu7D84u1iX+781lzZ11HOtCA3kGqKlpc3iQN 1GmoStzuby0XJ4bmYwXaXBSNNl5yO6j0kcQrsk7kfUo31OV6S90UnsndqwMgxGrQMx1F XFvqpi/4xTyq1d7YlVtVWcV7M7UGJ4zNAqcSI3htuGJIrn7Sbh2qk5Q9RBdbeuA233IS RhN7tb/Qn0f6xE1XA08h5/K7RzupRTjcPMrOPli+dGz/Q/hDYQnZoOq2PqJG0eZzWh9b vD8MnaWqxah5jIoZS0KrLtPHy/iVpJnJb7Mi0DGM96I2dIecJpqbm1UUZ74F+R1LcZgI bJOg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AC+VfDz6AvdYMzKgD5STVc5D9Yu0FiAAh+dmn5pN/2fWziZ9/w19eU8R ORte+1nctLt9JkKb4/aPNI8= X-Google-Smtp-Source: ACHHUZ7FdFiMstDAUS3u0xNhJRjoUKDLeXa9dIFDw7XA2omTe9cGweQRYb4uz+fKIlaBI6IFG04GsA== X-Received: by 2002:ac2:4475:0:b0:4eb:540f:2bf6 with SMTP id y21-20020ac24475000000b004eb540f2bf6mr2166661lfl.11.1682794656058; Sat, 29 Apr 2023 11:57:36 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6512:110f:b0:4e8:c8b4:347a with SMTP id l15-20020a056512110f00b004e8c8b4347als62784lfg.1.-pod-prod-gmail; Sat, 29 Apr 2023 11:57:34 -0700 (PDT) X-Received: by 2002:ac2:59ca:0:b0:4ec:89d3:a8a2 with SMTP id x10-20020ac259ca000000b004ec89d3a8a2mr2453177lfn.43.1682794653916; Sat, 29 Apr 2023 11:57:33 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1682794653; cv=pass; d=google.com; s=arc-20160816; b=xxdd4NidCg8TEjVdrGtbSn5Qg+bQ9YMh5DP7biTOoa8+YUeSy2Tix0qgeIkWJnJL6w 1sc83VNBZZgHsKtY0ndzuDWHDGcnvJE1/nbtDViYbZa3p39vEIdckbx4XjugCHo2oV97 Cr73AavzT0R9c+8GJGS639sdur4m2B4yHuiISG16QldXmltVEs+LZeQEA4y90jCTWPTo jvBAXKU6Gy5sGbH10SdAo/ADoGYc4u9m11mFvh94Bd6ynqsEvzDr1fmvzjS8GwY7mWyd TbZwtoOxxZBBrQZfIjD1uI3Yr0OTyLVUDnSabOB1Ct09Ixz1smZmuFV/nO4FioBLbTys N3OQ== 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:cc:to:from:dkim-signature; bh=OnzYuj1kuJVUucEpWz+zmEMjmD01iwnkKijwR9bYfU0=; b=rX286I3KPGSyL6e+/R+HaGTvr1JE4mkKgzmpwkyaaZALa/Cyo+ZnicSUo0nHubm1qW k8sXm0AgR4I8W5chULHzX4vp3M+tY7zmA/M/aA8ZOFRTEuXIpHxXxXeheBefvvTm3jW8 AjXnTxpFrlvbWZJDbEgcPCZVoVnond6JdL/a1TRCf3WKDzEoDvlPvRBW7vxXwT1nNrrz HqFHv7fy04tQa8eiLGM6VGt19zjzD0uMOKhZfLbojif4DB4XYPDwex1Jlo1u9Jc+GqGH LQa2Gv3L4S5/n5kl23umTgrKwhZTPhoUbX4B2wV1Ln/e95gHPhayqUY5TLgBIg67wbfA bjwA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@uwoca.onmicrosoft.com header.s=selector2-uwoca-onmicrosoft-com header.b=FwK2fBqh; 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::71e as permitted sender) smtp.mailfrom=jdc@uwo.ca Received: from CAN01-YT3-obe.outbound.protection.outlook.com (mail-yt3can01on2071e.outbound.protection.outlook.com. [2a01:111:f403:7053::71e]) by gmr-mx.google.com with ESMTPS id c35-20020a05651223a300b004efeb1773ebsi1260260lfv.11.2023.04.29.11.57.33 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sat, 29 Apr 2023 11:57:33 -0700 (PDT) Received-SPF: pass (google.com: domain of jdc@uwo.ca designates 2a01:111:f403:7053::71e as permitted sender) client-ip=2a01:111:f403:7053::71e; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=maZGGDCGwttYBjRv0l3q2z6ptxnRQ5Apdm9oac70NiccPq103+wyGb5DxfjkGegBeLb859ip+n7T0wK+VeCDt/m5BSxfo5N4aL3qbSR/WYL7lH+W8xHTPJ3kd/tCq65nBFTrhaek9e7S6h2URydX415W65o/zi6DTE0qO+m3vnoKZ9GJAa0yWxm3foI4yHBzeCJGwRPok+GE9RIOCW5tVg47qxJHebFiDgH7XY6y3FoEonMrKWaTVZTVMt6GrWQELd9NCzvEVKJW3K9KSsoI07jT7CpE4DJImtiAyjXi4dlaZ+3a0TtAIudO2gx4KXhN1fPCtAKQLre7Mw0lB0mdtQ== 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=OnzYuj1kuJVUucEpWz+zmEMjmD01iwnkKijwR9bYfU0=; b=MGJB6Vasrrap1J6e2EiEINVU2NEBQI3DXCBhkvB/iR/bEhw7fpZkKRT61B+DuIAl/Qwwtl6VFVgyykpZWymUO+sCxZiRYY83xVwxTsU9sIvzKE6ILvmdntp0dKxF4m1i8xQEWv/8Cn9o/C8541rovuq6aLRu2ESlHHxCn/lq/oDJkf7rVq9N9Big1OjZGpGtQrPvbam6H6JUuhSbZAekdRdS4+2xGZ97iU8AoHzTLTKgoBsfLkmbQrQgwwzKbl3doY/dffTa650Ltot166kJDRKV9R1yk7JQ9AQwaElL6gVQQAN0RFcyAY+32piTH2u6aGGJya+hBfunBMEfePLwBQ== 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 YT2P288MB0089.CANP288.PROD.OUTLOOK.COM (2603:10b6:b01:f6::13) by YT2P288MB0137.CANP288.PROD.OUTLOOK.COM (2603:10b6:b01:f3::20) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6340.27; Sat, 29 Apr 2023 18:57:31 +0000 Received: from YT2P288MB0089.CANP288.PROD.OUTLOOK.COM ([fe80::6ced:af59:e448:542f]) by YT2P288MB0089.CANP288.PROD.OUTLOOK.COM ([fe80::6ced:af59:e448:542f%3]) with mapi id 15.20.6340.027; Sat, 29 Apr 2023 18:57:31 +0000 From: Dan Christensen To: Steve Awodey CC: "homotopytypetheory@googlegroups.com" Subject: Re: [HoTT] Free higher groups Thread-Topic: [HoTT] Free higher groups Thread-Index: AQHZesxzxECCXAdlIUadD6wxcH+RXA== Date: Sat, 29 Apr 2023 18:57:31 +0000 Message-ID: <87r0s2y0rp.fsf@uwo.ca> References: <87leigyeya.fsf@uwo.ca> <87zg6qy4gx.fsf@uwo.ca> <21ED9406-6C3A-4B26-A74B-34C2821C97B6@gmail.com> In-Reply-To: <21ED9406-6C3A-4B26-A74B-34C2821C97B6@gmail.com> (Steve Awodey's message of "Sat, 29 Apr 2023 14:37:54 -0400") 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: YT2P288MB0089:EE_|YT2P288MB0137:EE_ x-ms-office365-filtering-correlation-id: dd3286c1-1794-48e3-ad12-08db48e395ea x-ms-exchange-senderadcheck: 1 x-ms-exchange-antispam-relay: 0 x-microsoft-antispam: BCL:0; x-microsoft-antispam-message-info: 9HbOlWMU2xYg6iJNFxfZR5whmhW/XqNUwEGzBqCdboNZWGOB4sdOPQAnxnmHlUy5FlEQ8LewwHD7rH+Lekb0/R89MTmlnevU26JezWttVL57UhPmMO/oAEsHWO6qlxWz6lDZqASYeP8/DTLRUuKiTbe8AmYVr3DV+SR+thz3vW4y/Y/3/5rsrY6ZQYcF9c8v+qjFeEgPYqkTb+KbIDfVnHGAqF2t6O3cI+zm7qw4kYrVzuDpHTSFP/1GYQi8XF4RF42cAEiM8XwRzX9Ro54ZY6Znt7cBdmvsaqJ9HVPER7WnU7xT5ZRy7DIwtlfxCiYg+gH9VIFUg9T2tUU3WUaTk+kUUDlten2AQNZEY1HMWDm/HBUMlCgnzkbMgxuo1TKVvLMW9eb1YtMkGZrpev9eyIFIyAprF7/ACeSWZ/vp+Sm/XMait1WvSYB1viDg/t58KbkjY43jkguQ6IHQZw8sfglMLf/AbEpwzoNCqX3eTcV9J+egXJagvvwjv6oy8PG4aDNYEba+hrFAzGMEUu9GfMpUDidq8q1W9bNysATXldW/Mz2qtTX+x6JSB9yTvO/4xCd2jla9sCicafT3jdRmRn5TY12lgrpgP7eB0iS+5U77peaWEueQ4VRxvoMT65dgLNpvLUy13tl9rb2W2h7aJw== x-forefront-antispam-report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:YT2P288MB0089.CANP288.PROD.OUTLOOK.COM;PTR:;CAT:NONE;SFS:(13230028)(4636009)(366004)(39860400002)(376002)(346002)(136003)(396003)(451199021)(122000001)(8936002)(478600001)(38100700002)(8676002)(86362001)(41320700001)(66556008)(66476007)(66446008)(64756008)(6916009)(4326008)(66946007)(76116006)(41300700001)(36756003)(786003)(316002)(38070700005)(83380400001)(66574015)(966005)(2906002)(186003)(6506007)(6512007)(53546011)(26005)(2616005)(66899021)(6486002)(71200400001)(5660300002);DIR:OUT;SFP:1102; x-ms-exchange-antispam-messagedata-chunkcount: 1 x-ms-exchange-antispam-messagedata-0: =?utf-8?B?MWhINVhOemh3eE1wTnVMSTZrM09ueThyT1VQaXpYVlBhWVB3QmpQVWNmQXBW?= =?utf-8?B?NktHYWd5SC9ia1RhbDNTSG9KSmJYVkRrZWQ1bXhoRjdIdkZScmVJYWFqM2hv?= =?utf-8?B?SXhYZTJqdFdWenhBQUl3RDYvK09tQUp0anlRQ1paYUhPdWcxajdQK3BtSDNG?= =?utf-8?B?RE5IK1g0aG5GMEIzRmFYN0dhV200cVF4Rm41UmZqaWx4ekMzblBkQzFxSGZk?= =?utf-8?B?Z1hlWTdkeG5yRExlZTBHNHFZdXQxc3NHQ3FLVUtkcWppMjB0aGV0eTdrVzRo?= =?utf-8?B?cWkrMXJucGZ5bGVEOENvcjFnQmxGSTQrNVlKTG10RGtIbmpGTDc2ZjN3bGdk?= =?utf-8?B?eHBpWFlwNkRFZFZGYnVDOUx4RzRHT3dIVjlHZXRxZW9tTERrU1JCWHNzRmsz?= =?utf-8?B?MDdRbWcwS29oM09nNTJLay9SR05zODJXb21FTzl6ZU5Gc1BIdEtqdTVTL2Vr?= =?utf-8?B?RzlSNkJiV20yZ2l6aGF0QVEyd3gxcXNMQTJjNmZ6SkFHLzUzTTViT05EYlpT?= =?utf-8?B?QjQzYmdTWnZiTkhGUHpoclZESEdwR3dhMzl4c3JaOHVZdU5RK3RzUm1qVGwv?= =?utf-8?B?RVRtVThsSFBFdlVBbEdsN3RVUnpGeEVNMHFMR1o3eWVleU5OaElGNGlUNVVl?= =?utf-8?B?VVhrMFJnbG80YitSalZBMDJzclJmSlZVQktHa2x4MkpLbnJJT0MxbVVMczBx?= =?utf-8?B?bU5jODA4eCtQNGdWNXNRcmdSamtpQ2FNMWFtMit1cTVobFhqNmZWNlZ5L1dQ?= =?utf-8?B?REhSRHZBS3Q2UTEzTnZDRjcxUnlHTHhiS09SdEY3WEhPR3dzaTFEWWc4MlBw?= =?utf-8?B?RnBTVGJXZjVkMHl0NWtaSTNQc3UxN3lBSWRUeVJuS2lQME9CWXFUWHJIMHo2?= =?utf-8?B?eW8wUmM3LzJURXFiVXB3SUtsWFlVN2RkazErQklaUWxzUFZqUW44QVFib0xB?= =?utf-8?B?NkdNcTZvNEdJZkdZcHh1S2xjdkJhZlplVmJSOURadGRxUU03Ly9hc0dyRXpH?= =?utf-8?B?Q0x3VEp2QTN0UHJUTGxzSkVqakNwWWlDUlBSL3NQby9aTVNVeGIwS1R1SmVJ?= =?utf-8?B?aTVINzZmd3pHSVZWbnc3TXBPVWpMQWEwOU05aU5ZOWtBRk5mMGlqQUFST3VB?= =?utf-8?B?U1FMY250d3ZTZzlJaGNNMlFtbWgvZ1hnbW9BOE4vcUsvZnBwSWdaNmxQSGx2?= =?utf-8?B?TWtnbGt6ZmNNVGFqdEN6aUg0WkpqM3BNV1J5WitmSE5NUGg3R2RQWHZ3TGk1?= =?utf-8?B?eU9vSTcwTi92ZGVoSldiL3kyWUFxY3UxZTRzUThLZjdRYnk2K3VlY1RGUExQ?= =?utf-8?B?YW5DaitLYmtKajdmRSsxUUlVZEFsRWRwSkhrc3NxZGlrN1JsdGFNc1NBMjBi?= =?utf-8?B?WkZuYmF4T0J1Q0tkbUFjaGt5K21xSDl5bURjTU8vRExVYURuUDVMb29DNi8v?= =?utf-8?B?Z2RzZ1dtL1JJaE0rd2NRRTZDZ3A5VUQ3TkZwbHJOakFMc2lBckNOS2N4d1lz?= =?utf-8?B?WEc3RndPYUlWZTlZRk4yL2xDNTZkdjVKKytia3gwZEI5SnpoNkszNU5xYzFI?= =?utf-8?B?TFBxc0hYN0NZMnRKR2JxS2NJNnBDY0VQS3VTR0MwUGZJaW1tYlZGNDlQMDhy?= =?utf-8?B?SVdCQTNFcjV4ei9aejhQT3MyRUREYm5hY0ZpSUdjZmI5QXhvL1dRWjVHbDdv?= =?utf-8?B?ZUU5QkRUTzAxYnltMUxDYVFtRkt4SlJTcnhIY3ExOURtc1oxeFU0ZEt4aURh?= =?utf-8?B?YjhUaUN3Tm5YSHBkVm45NldSeVRTei9oc1gwNWM0clMvTEZGVnh6S2tLcUFI?= =?utf-8?B?aDhVQXVQQ0JacGY2VmdkakpmTTBtdnZCMVJmcWU4VkNQYUUwbnpIeDl0d2Fi?= =?utf-8?B?bTVUMjBsRkVTemlnSC90T1VDUiszVzIyTm5kaXBUbUdQL3pjcUQ1a2ZtYktm?= =?utf-8?B?VEZxZXZvOG1pMnhrMkkyS3MzK3Nudnpici83R0JRSEJRZVJvbWhZaDdEY0ZO?= =?utf-8?B?NHd1eHF0WGZBTkF0eTRCQmdHZjc0VXplRS9qK0ZOd1dIVElQaVB0aDJaYlpD?= =?utf-8?B?RTI3WkUrWURCWlB4RUdjTjVIK3h4aG9QdGNqaHdLdzJ4NWVSWEFvemQwa1p0?= =?utf-8?Q?wHbw=3D?= Content-Type: text/plain; charset="UTF-8" Content-ID: <5EBD671801CB7F43B1D67DC20A03340C@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: YT2P288MB0089.CANP288.PROD.OUTLOOK.COM X-MS-Exchange-CrossTenant-Network-Message-Id: dd3286c1-1794-48e3-ad12-08db48e395ea X-MS-Exchange-CrossTenant-originalarrivaltime: 29 Apr 2023 18:57:31.2730 (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: B5n8W1/CIPj/A8mdP4jvinlJGYKkyW0N07aLrMYX639//HLjI50SB1G0kZNkKYmQ X-MS-Exchange-Transport-CrossTenantHeadersStamped: YT2P288MB0137 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=FwK2fBqh; 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::71e 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: , 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: >>=20 >> 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. >>=20 >> Dan >>=20 >> On Apr 28, 2023, Michael Shulman wrote: >>=20 >>> The existence of hypercompletion is a good suggestion. >>>=20 >>> 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= . >>>=20 >>> On Mon, Apr 24, 2023 at 5:37=E2=80=AFPM Dan Christensen wr= ote: >>>=20 >>> 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. >>>=20 >>> 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. >>>=20 >>> Oh, what about whether the hypercomplete objects are the modal >>> objects >>> for a modality? I'm throwing this out there without much thought... >>>=20 >>> Dan >>>=20 >>> On Apr 24, 2023, Michael Shulman wrote: >>>=20 >>>> 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. >>>>=20 >>>> 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? >>>>=20 >>>> On Fri, Apr 21, 2023 at 5:25=E2=80=AFPM Nicolai Kraus >>>> wrote: >>>>=20 >>>> Hi David, >>>>=20 >>>> 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? >>>>=20 >>>> Best, >>>> Nicolai >>>>=20 >>>> On Fri, Apr 21, 2023 at 8:30=E2=80=AFPM Jon Sterling >>>> wrote: >>>>=20 >>>> Dear David, >>>>=20 >>>> 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. >>>>=20 >>>> Best wishes, >>>> Jon >>>>=20 >>>> On 21 Apr 2023, at 12:04, David W=C3=A4rn wrote: >>>>=20 >>>>> Dear all, >>>>>=20 >>>>> 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. >>>>>=20 >>>>> 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. >>>>>=20 >>>>> Best wishes, >>>>> David >>>>>=20 >>>>> --=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 >>>>=20 >>>> --=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 >>>>=20 >>>> --=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%2BAZBBpPwgh1G9V= ZV0fgJFd8Mzqfchskc4-%2B-FXT42WQkzmC9w%40mail.gmail.com. >>>=20 >>> --=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%40u= wo.ca. >>=20 >> --=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/87zg6qy4gx.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/87r0s2y0rp.fsf%40uwo.ca.