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 autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 21539 invoked from network); 28 Feb 2021 15:14:09 -0000 Received: from mail-lj1-x238.google.com (2a00:1450:4864:20::238) by inbox.vuxu.org with ESMTPUTF8; 28 Feb 2021 15:14:09 -0000 Received: by mail-lj1-x238.google.com with SMTP id b24sf5426501ljp.9 for ; Sun, 28 Feb 2021 07:14:09 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614525248; cv=pass; d=google.com; s=arc-20160816; b=SOhsRhvkHtfLwWOFDNWJ07tnVuyt38S6W+EdjfgYmuT3EFk6piwkFEyI6zELZoLuDf nXlrIoMKe8lpMAvM5yepI9WwVCmObO3Pjd1VCLbThwAMZEzv0cIuUZLEfheM2aAR5c+R z8oC9hsT0E1DE1AHqHwbltM6CcbX3aepTcWFoYqlutLjVf91DZcetwEbf+dWoiKblrog Cn5OjDdyomG8kTkqQ6Edhd+T/ExG7xghJKxRv9zv3Y2FSzh0i4/4Y1DnPJZgOOgb7B2f 9s/D5qLATYR6Npj4tRQwSd3HaD0wIZfyG6V7ym83moJjVK22Phk54MjHTqF6TENlRKiV b5Ig== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=A+7jmOcK8+v4iLT7ZIETnxPDm+X9xyLmTAR8jMlr39g=; b=NCnZhQHLRFpgfnJ/rQoP1buFZhXLPWnAnMqs1oaBQWnBFbYgLLGmB/b/mRqRdfJvu6 1fnWKZV7nVp+kHwf46/InZBiW/NkCfIC4863f7nQhVCYrpKycHEYqZwaS18Uo9MfHvVv wkbexQxkN1ZCCPBKQBDcEHHgfbuZ6FBaCYnCt32l6D445hb1zeyP9cSP9i54REpOsRzP U2aF1PPCK4+w/BDd7wb7qEepC+KbeHMRc7aNNWbGEhKfBkykxxFwOcO56J2eXfbTIPew HfEhfyjioTNcTYKyh3Xmjheq3w74o/C1p8rVd3n1ZUFe+G6LqBOmOEeipLIKDO+vEjSg tFJw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=A7s5QTZR; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::62a as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=A+7jmOcK8+v4iLT7ZIETnxPDm+X9xyLmTAR8jMlr39g=; b=guxmfK+ivtjEhPG5KBZLut5+pNt/5UXprxVuSQmtND2PVupTFd/vclVidoOqFwUcO3 IpAUTEhkvAU2WLBUcPmr6ENeKYlHKsJRo6pgmEhCULnDM9gRY6Zw43WQAZiXSsEsVcNa bmGR65zdqQ5p98cDZZM8q5l1j2bLDfAOI9HFmMpMHCNUENl3Z5akn4+IziQ5HtGX6fgS BcPu3w9dBuyUq7ZxnNBtYiFNserav1siSOBJO6ll78fNk6FYNkyGasDVx/vZqt4FF3JD KRKjKQ7+iWgUOn7r8eLAkSBZ4CRFi8UkfRva4bLN2bbDXx9m1Wp1eH+/KAGdex2FhPp/ bBYw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=A+7jmOcK8+v4iLT7ZIETnxPDm+X9xyLmTAR8jMlr39g=; b=EY4NjgQvMt6Fzf5fI5sXuEweghIjRDbZt9cECQXpiQSNgBG4QS+lmmJ9ulM7VQknpH Mhdq/Urgh1cgOD8QJ3h0Xq5ko41zJbRtc2IlrOG6bsJEopEaoOQz4WRjlT56cG9iTsBN Jd5FcEyUmtoFF6Ia5G/ZlTIYP9sKXXhht8Vb0X7op0tXWkdlPQwO4Ji6jfFM3g3dS/MT EChEvVqME4W2j4SzRDYZofvnEcqxUELBV6R7uopIkDgVN+I5PqX1Bp5UIdX9Wp74J5jc r15aKExOSERgxsPOVuQyePRHE+P3Zygytc1W194EoCCJqgUWIIUVrnmgrOS8UGa13ta3 f7oA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM531sxSr8znjlXwIWL2vxJT2016ycCub6JPgiqcjS2uJJwGws3nMn ZCYvzDA4+jOCMQVe6w8L6PE= X-Google-Smtp-Source: ABdhPJxKoA7ID6LMpSoVTQ8XhaNxbnMEiZTgxDpdRR2snwaGbXyXGlPFdYnaS9dwnAFw0dCDHa0JMQ== X-Received: by 2002:ac2:5d4d:: with SMTP id w13mr4129880lfd.63.1614525248351; Sun, 28 Feb 2021 07:14:08 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:b4d1:: with SMTP id r17ls2368088ljm.10.gmail; Sun, 28 Feb 2021 07:14:07 -0800 (PST) X-Received: by 2002:a05:651c:1a3:: with SMTP id c3mr5377341ljn.77.1614525247169; Sun, 28 Feb 2021 07:14:07 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614525247; cv=none; d=google.com; s=arc-20160816; b=anQjLME0HfUEU9mfrc3EDPyM6pZnZsg7HQoXbFLUFAKLK7o7byrKLrcuQNK5mXCs36 oVSawl7ss1NTCBeRQQmMwVFA3PJ2Lf+xAZKMJkaaZAWGjjvnckOYGSJZqivaVIiAj63q 46CDYHo7+isG37s6zqZOM6AOsiv1N46EXqYyZ1fZkabUpOmmlIDVgPn3vcpgr7xp30Io w5EOk8pXd6cL5N3IkNKT8p3d2SEpKI1nfr5p3wRNHeXXthzIrSzdNiglT5JB3HPhQDbG d9rgq9/65PwzarnGlw71n6RPEtj2tdY8YzD15KtBugB/aZgeOBVzTMbVp9S8mm+27f2K XCMA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=9QgcUfuNtsGEyw1sCxzBYNMWikFYl/s+Zc9iUOs62pY=; b=ZfRQFY/Uabg+hVsGN2gwg1K5TLNHg4aX445HQfbadGaja+GxkLBrMdc2wlD6XcFTF2 o9lVYTxvkwNvxag6nIWfxsW/H4a0LAvotcmxZuX24KYBolaAuhQcCiy3slCJ0KXt64lO pi+N3bkkbl8jluuIW8VmFzkA6STUgMKZ1SvU+NC5GwTPgJ5FQHhTlJhpCsfcvcKtYCrW fmpkTjsVxjJm6juQnQLdF5YHTy5sy/ycKsbvlhU+TDdV/2jNZORR8IIVzLpdaSPQ6wya MPW1+M2l7Q7I9a2bjYTzlaMz9zjnOlgvCD+KcpisQEJ2H610+ut+f+wSmlpPdWmNzTSb NeCA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=A7s5QTZR; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::62a as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-ej1-x62a.google.com (mail-ej1-x62a.google.com. [2a00:1450:4864:20::62a]) by gmr-mx.google.com with ESMTPS id c6si727851ljk.2.2021.02.28.07.14.07 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 28 Feb 2021 07:14:07 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::62a as permitted sender) client-ip=2a00:1450:4864:20::62a; Received: by mail-ej1-x62a.google.com with SMTP id mj10so3356914ejb.5 for ; Sun, 28 Feb 2021 07:14:07 -0800 (PST) X-Received: by 2002:a17:906:3b84:: with SMTP id u4mr11885632ejf.431.1614525246713; Sun, 28 Feb 2021 07:14:06 -0800 (PST) Received: from mail-ej1-f45.google.com (mail-ej1-f45.google.com. [209.85.218.45]) by smtp.gmail.com with ESMTPSA id w8sm10973511edd.39.2021.02.28.07.14.05 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 28 Feb 2021 07:14:06 -0800 (PST) Received: by mail-ej1-f45.google.com with SMTP id mj10so3358490ejb.5 for ; Sun, 28 Feb 2021 07:14:05 -0800 (PST) X-Received: by 2002:a17:906:654d:: with SMTP id u13mr11905467ejn.299.1614525245523; Sun, 28 Feb 2021 07:14:05 -0800 (PST) MIME-Version: 1.0 References: <034025b4-005d-79d1-cab1-67470b3245bd@googlemail.com> In-Reply-To: From: Michael Shulman Date: Sun, 28 Feb 2021 07:13:53 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Re: Foundational question about a large set of small sets To: Ulrik Buchholtz Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=A7s5QTZR; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::62a as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu 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: , Yes, that's it. And I guess you are right about leaving out the endoequivalences at level 1. On Sun, Feb 28, 2021 at 4:45 AM Ulrik Buchholtz wrote: >> One can then get a >> counter-model to "there merely exists a set that covers Set" with >> presheaves on X * 1. > > > This I didn't check. But couldn't we here instead appeal to homotopy cano= nicity? Since Set is a closed type, if there is a proof of the mere existen= ce of a set cover of Set, we could extract a specific term for one, and the= n obtain a contradiction in the above model. Sure, but it seems a bit overkill to appeal to a hammer like homotopy canonicity when a simple presheaf countermodel would suffice. (Although I suppose there may be people on this list to whom the opposite would seem true....) The semantic argument is that in presheaves on any category with a terminal object, the terminal object is projective, and thus the "existence principle" holds: any closed type whose propositional truncation is true is already globally inhabited. (Of course, the semantic proof of canonicity is similar, using projectivity of 1 in a gluing category.) --=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/CAOvivQxadLL6w0FehP3owkF%3DHP5vr%3Da3tcqm3FA_hGbrcOZjqA%= 40mail.gmail.com.