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 17148 invoked from network); 27 Feb 2021 23:00:30 -0000 Received: from mail-wr1-x43c.google.com (2a00:1450:4864:20::43c) by inbox.vuxu.org with ESMTPUTF8; 27 Feb 2021 23:00:30 -0000 Received: by mail-wr1-x43c.google.com with SMTP id e13sf7060257wrg.4 for ; Sat, 27 Feb 2021 15:00:30 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614466828; cv=pass; d=google.com; s=arc-20160816; b=XNCfuT8XQyJdlxpsAz4VFrHq8OfCBpsuPbR/skFTRje9WPQo5G5RqzLQgsRDTj02w8 RLEDn3qdVeTYpJLKF26HGQpIErLAR79hoC7TyUBNEGwOwKdMoRt8Q0heSExECmNYN2J7 RR/4gQHr6rAngTvJx8qRwbCUdyHa0ywNmSHFku7ryng9TC8sRhyPdMbwgyRh3V0xJ5t9 wYZ11IjWCgwWeL4IVPWcwj+K1haDr8ufT2SD5y2kUL/oeqHiF8+dGvI4pddToU+C+gQ3 OXK3Xfibaj4Ghv2URo4n/4Af5DfEmWVl6YOMf/xPKzQQk6juOE6qwQkO8uaxCH3vMFtY yYtQ== 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=X9TgfwwYYkJpstk+Be5UTRp8xiO/YmK+Y+pZ2glO6xc=; b=ttz3YDpI2wcXJtp2PMeV0F7NStgjRW7+tfWSruhWWLP5dopkRIh6O08o7SpxP4dq3g F4CuSkAGiaU1jmwsmi9fynvlgdtrgCrkdTsFXE5teW2rYWh4/719ZZZx4JG19KL5apyo sxNTdonSYbeoMH9M2srCSqq0gCliOzWwf9xv9CJpMC47TbUk5i3nQ60czjxNLUT8G18H xdx1Oq5WpK67y6brKfmcd+yb/u4cq9RNvUHx1pCoArMmHyMeHFHIUCX/oJoThTMqmsmf 0PEXpE26prGdAhXkUwKUzU08dGOnSlSRmG1MDPaAYXQ5DT0QN8DB2YpmCTZsqPQCrUSG /1GQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=Xh7IyGdA; 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=X9TgfwwYYkJpstk+Be5UTRp8xiO/YmK+Y+pZ2glO6xc=; b=HNijAl1gAB5LOmTWt8tMWecSDaJmPlA6T8GLhF9uJNCjFhzhzmKdfv25OFEQm6qilt ud3F9Mp+wOzeI0xntks0akdln/nF3aIftoC6e+EgvqoDPD6ZNb4AUWvS23qD1iW2bLST Q24E+hb153PyZPxLJRdpOTzUlgPF0qxIJ0m9n9CPJsmfTQpw4hPXjFGsp3C2sRQFwIrL deeCnWWMJfJkX2oCKdu/bpKnVaswh037eCqc4YBCEml5eoQYH7taYJR9yGovAmiSmFTA 5JifTRZVbFqytxIuUmwCkemhglNtSYa1/4kCNhIwXr6mBt8HabJysZCkb5pq6xsFcU0y s7FQ== 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=X9TgfwwYYkJpstk+Be5UTRp8xiO/YmK+Y+pZ2glO6xc=; b=PaVVkpSnSJBPr8AsVo0tbXRxRB9UFUw+3/jAnYFA4EaOpkKJ8M7mgG0nxAkB7n4eUt oAs1YldDUPphR5BH0nvWBp61qU2FZMhyJMTjr8HU37PgRdauVptRI/HzgGK89eLfOyWP ZYnevcZ6Ow5u/sLJKTOCLMDz56JEpUa43KUYL1iYl6YW7GBRAnWxHbm+k0Kt4p6v5FhD c7TY5pGh0N8hGdsEgjP6Xf+5UJ4kPZTnhGK4LPTvM2yJ672SPVXok5Iy63QVatDLyJbo 3twcNyk5EutUeTDs5f3s2tQTsfreKt9ySzGveGtfcRu9P54UVR+mNMzVsA/W//PAbkov q8aw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM5326a5YtHYaqKN6ULMO0sowpJspCQ2T4LtZevCjC5QKpUT27sF0T /yHi6/Fh2SOK0CbF2or4gG4= X-Google-Smtp-Source: ABdhPJxiC7ST6GBOz83l8I7q5KNc88+V6rDxgqPM8wRuD8XQDsMmdoWPOKzsXlE5BO3Ew7QkBTCGDA== X-Received: by 2002:adf:f2c3:: with SMTP id d3mr9817511wrp.380.1614466828127; Sat, 27 Feb 2021 15:00:28 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a5d:6a89:: with SMTP id s9ls6223991wru.2.gmail; Sat, 27 Feb 2021 15:00:27 -0800 (PST) X-Received: by 2002:a05:6000:2cf:: with SMTP id o15mr9440483wry.184.1614466827137; Sat, 27 Feb 2021 15:00:27 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614466827; cv=none; d=google.com; s=arc-20160816; b=FQzDQrks07Y0wYRAD1GE9y/fNo4jCY8BPe15O+F61tZyfcjRFaRlb+ABCtWubqMh7F VrBRDOczZcwtwnO+d+w/KcAohr3/ff1EDNMAhGIiUn7ZwgvJqenYk0368FRkgshZH+My m9twhULlqE1pQk5eDc5B5aiCpCauPp71sSolImmXKoVJbDILaFTH5NXB8VLyXhqZxrP6 loP6JHvRbuzJmO7evZwlVZ5AXX+VL8Ms2ylJ8dGj1I/RBVfnRKTPb7raFXACdJ1dE9g6 OL1wOkC2vK4GKLqat2Cf+26Wbi1JNeLEkDZ8oAWqe5SLA9HTVq2I6B7bjrXb/gbasHm9 SxmA== 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=KLK4ZVfoMJPDBHzeMIILDe/lFeGIuGJM1xO9ALGku2o=; b=vB9u5hGmfwntygLLADm4Y/EnG3C62lrzqYrUfFT3J56sBVEW0xRBFchAtB+I+R2zMj dpf0dnabYfn+mtZxe7WuM2Ge679yx1MSU6JwEEej0LOJw8QZ/9gK4Ic2+8wFg5PnIYZD JASdCiTtCB9CXaX+NzZt5gIr4sk/PIHs9LlozzbOP2taDv+BQrcOVkDBt/BvHutTe472 AJ5leBkoRp5WiFdwKwpQQD7jyXysQ7yFeJYF0GUjbk1ojRo43H2QK7OiiCvsUuaxFR5t FAfv3EhS6MOqOEwbt67sCoz2fDbY6Zp/fT4ixtQz6sDIU6RnbOgrcJNtubEWNLfbBLBN UFLg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego.edu header.s=google header.b=Xh7IyGdA; 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 h16si4247wrx.2.2021.02.27.15.00.27 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 27 Feb 2021 15:00:27 -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 a22so21211972ejv.9 for ; Sat, 27 Feb 2021 15:00:27 -0800 (PST) X-Received: by 2002:a17:906:1759:: with SMTP id d25mr9547598eje.524.1614466826666; Sat, 27 Feb 2021 15:00:26 -0800 (PST) Received: from mail-ej1-f41.google.com (mail-ej1-f41.google.com. [209.85.218.41]) by smtp.gmail.com with ESMTPSA id 14sm8372633ejy.11.2021.02.27.15.00.25 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 27 Feb 2021 15:00:26 -0800 (PST) Received: by mail-ej1-f41.google.com with SMTP id mj10so1121757ejb.5 for ; Sat, 27 Feb 2021 15:00:25 -0800 (PST) X-Received: by 2002:a17:906:25c4:: with SMTP id n4mr9562572ejb.359.1614466825455; Sat, 27 Feb 2021 15:00:25 -0800 (PST) MIME-Version: 1.0 References: <034025b4-005d-79d1-cab1-67470b3245bd@googlemail.com> In-Reply-To: From: Michael Shulman Date: Sat, 27 Feb 2021 15:00:13 -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=Xh7IyGdA; 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: , On Sat, Feb 27, 2021 at 2:43 AM Ulrik Buchholtz wrote: > Unfortunately, I don't know of a model where there's no set cover of Set = U. The counter-model at the nLab for the general statement that sets cover = groupoids (https://ncatlab.org/nlab/show/n-types+cover#InModels), using pre= sheaves on the category-join B=C2=B2=E2=84=A4 * 1, doesn't work for this pu= rpose, AFAICT. (Using a general 2-group G and presheaves on BG * 1 won't he= lp either, I think.) I believe a counter-model to "there is a specified set that covers Set" is presheaves on the 2-category X with two objects a and b, X(b,a)=3D0, X(a,a)=3D1, and X(b,b) =3D X(a,b) =3D B=E2=84=A4. One can then= get a counter-model to "there merely exists a set that covers Set" with presheaves on X * 1. I worked this out a while ago but never got around to writing it up; it uses the fact that since these are "inverse EI categories", there is an explicit description of the universe (http://arxiv.org/abs/1508.02410). Mike --=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/CAOvivQzawyMqT4uZ7%2BKbB_PftqbMzB4V8HUvgpJPSoe32p62aw%40= mail.gmail.com.