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.4 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,MAILING_LIST_MULTI,NICE_REPLY_A, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 30277 invoked from network); 1 Mar 2021 07:52:30 -0000 Received: from mail-wr1-x43d.google.com (2a00:1450:4864:20::43d) by inbox.vuxu.org with ESMTPUTF8; 1 Mar 2021 07:52:30 -0000 Received: by mail-wr1-x43d.google.com with SMTP id u15sf8863203wrn.3 for ; Sun, 28 Feb 2021 23:52:30 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614585149; cv=pass; d=google.com; s=arc-20160816; b=Lygmy4ND6XKxN5QeMAbSc52NXOO+z7hragxIPSxTn0EPhkxNFYthjl8iUvlPyRdbrd sDn//vLhY/7F2dde305UPy+g+0wMWRq1cAnURcBuHi9Kpf3XBCTRg5CHP0spsEE3/LE9 k7NV0CBWhDZCfU9jAaqfuhMy4fhxLR5Z2pR4mJ91YYaWCLLgaLCbPM9uuxBqjuxcM0gj 4M/RNjwc+bXAECpnJrk3sF04krI+rsww8mV7bD5HPThyfVe2CEDaBXWGWJftpApNsruA xKUYlrLBiQCRaHZptiuuAWAq315T8c5eoqiiBwC/nYvvpKAJloYZNbnmTORWKLOBm1rc RSEQ== 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:content-language :in-reply-to:mime-version:user-agent:date:message-id:from:references :cc:to:subject:sender:dkim-signature:dkim-signature; bh=iMIOYS47lNgeH3vICHoBEP3XOEq5aXTZ9MA/o5emCac=; b=1J1jCuFE/UlplK4rVI5Nu1S9Nb4kU7j6aUeF1zoqM7S2mmghckYuJlAmS0GSpGx9vV q0EQ7CXoAQjnNgtcqmd9aN4aFUco00FZlersfuwQeKiXV2kbCanlC3TYV6nh0O8qhIGW R0HFTrP4gMOpiEmIJFS4LEbBljk/A+Df1yIhnal6lDqnN3q4XAtl36D11z449s/+yFut FJLfgVY8sIns3xWRvhJPNIPCcNuoq2tor2LQX7iJ5DzIBbasOq5h+fiAAW7HmE+qTVqJ FkyvCrVvXsY+Yw+eKgHzyhuqpwSDHu9HDWHEuunetGhdYlXQptrSLmbRVswWTLyoKlBp A1vg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ZN0NLaRg; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::32b as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=iMIOYS47lNgeH3vICHoBEP3XOEq5aXTZ9MA/o5emCac=; b=j3t7SKZjyrD29tCkYPeTiqQCtiCMCFxxdQO7SBaqFqUzL0Nr4D7CVRyQLmXwxYiOko emCgUXALrqCmdESO9Rn7s1phIvI8NbGoY64vlFikAYcWyIo9eBp7SVI9NKhjJ+dqCTF0 Nv3jf8JOpPzc78NDAOGsngxrrB9eCvWhDknyQja/I2rN13XDmf9rLyt1qzjp36cG2kjH kuTTGbvSzeQ3IZEM1sEe/xDcPQhQL8ZgQuHudcDqFZJTpVzY5cGfcYrQhB3BpdHu/IeQ DNCvm7ocONx6gJ/mhyTD09hHxgnOLOfki76h/3/eB8Eons1jmH3lCYdQC2kAjFr+7J1I oh1Q== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=iMIOYS47lNgeH3vICHoBEP3XOEq5aXTZ9MA/o5emCac=; b=skBYT/2lfKXFkSGVwBPL+p2yfkKlR5RXR2vCfzWx4MA4nBWbQeI2VRqDms3NhJUR4J gUyX6nTe4L5DDg9y59p59A756w6QYYucE082z2JrQhxL5XYrjgDNRFaJi9lcIkdWep28 xrrBdKggLoISGrqCh6zw8gR1NK+ZGeHOo6k82gfI71P8jR+5lwuLGW80FfNGuhA4agXR EOVuZPgGAuEaTGbmnc59QtBeanG37H9awuh4gPSwM4c/bpJ5Ro4pfirlJTdWa5Ps7Bai I6++hP4+D2h+6/rTfuIRf/hIpDsMQJPG2e+OVI/yC0FtwIfJuzy4bboiDeVCIhitbzQo UGQQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:to:cc:references:from:message-id :date:user-agent:mime-version:in-reply-to:content-language :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=iMIOYS47lNgeH3vICHoBEP3XOEq5aXTZ9MA/o5emCac=; b=bhap7CaMkGQPK5myV6O61QFaKTBZeeONaG83oHNv0B04uA+SBMdxsX4u7Dk2aw1wvu jUYIqKONb7SKZ07itHACh77G+mhZ7pr6pDnbA3uSXBCA5jqYjhthQOyyCqmJaYZYRVQL ZilaVJc0TpyY4+/ITGRGpYL48pc/NqmDGHQGOIerqGZ6fZzsJRhLcZfvi1DcqTk+1kZJ q3RrDSUaXdSaQ2XKL0WaDbfi+fIUy5FW+ffn+sia/Jwu6nutI9v71FxBpgeDy1nIECcC tp9nic7IWAINVxRR7ETw1iEeuc9UnowphH1TDCQLuPfbmi7Dm+OOInOSAb8ZTnCcTDxR 6/wQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533RpTeee0TScJIeOGmTr4BOzaYMSQg3zSznB2/V2ZVEIFAvdQah GI/2gh5gYFRiggi5FZi3V68= X-Google-Smtp-Source: ABdhPJxv0xfMSruEnqKWvRS6LUdMnn1kzcV2gVP6rnS/UKkhVgkZN3Adtx6oN5Ph7b6ha6pcnKoesg== X-Received: by 2002:a1c:e383:: with SMTP id a125mr14477719wmh.125.1614585149291; Sun, 28 Feb 2021 23:52:29 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:2e44:: with SMTP id u65ls6328383wmu.2.canary-gmail; Sun, 28 Feb 2021 23:52:28 -0800 (PST) X-Received: by 2002:a7b:ce91:: with SMTP id q17mr7128813wmj.28.1614585148316; Sun, 28 Feb 2021 23:52:28 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614585148; cv=none; d=google.com; s=arc-20160816; b=DSaQnSLL5hSwRLokpoLsOMlFy9P1wj1Pi71gqDGTzx/eIekJ+N0ub+w1jxoYn6+nRu AUJOb81ftMy3zsQt4Zr2Se8E3CU4WYtiCx+4mSUpXm1RHIxexAW4a7AeuUxou4OY1UTR lSvDW33PMSX2ZtT/LYYe3tq5M9fT587P5ExVQrcKbAPM9Z8bpxcWy5FZZ3ZIu51V6ci+ SgoV1wLTkKGV9i4HAw9xYtsaXlEWUIj7IQOYVKStMu48K3md9IR9e613Oy3yDkWB99pz NUH9/c8Zl6sD7T5T/Vn/1xtCpNyNpVlKO5EZv4s6h5eOglcNuS28FYVXyxqhqHjFLSgW 8sjw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:references:cc:to:subject :dkim-signature; bh=VACwGrfPgpKRCHTRqKFBshSjttV6ixSsJ45tBqfrxRM=; b=QTT9q12cUMdR+MEObS64a3gxNh54ng4GbNDL+BCGLeUzUVI4CFUdw2lJ48SoOkxLeT 0wDOcLhoIL9RHjZRAv52CufRusgh+NDcuCM4MVqtcwCRoHTFZpupeQDuTP0mrRLZEVpD L0PgAAWbTc6B9eh1NOSbEyJZ3uQ18PK4hjKWpTzFIa/Unp3Z2xgmKLh6cKPmBcEIXZr+ q1ursg/0Hbd95ONJ4Xl4p6yJl/vd0biveJQqZ4lb5icXtO8Wtn82xXTggmINEsM7JmBk 6AVCvDplmFvXPelCdf69nVXnzuRAaQn8MYTvyNfHDVEDKEv9EbCxabZON/uQHLP+GDOC m5Gg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ZN0NLaRg; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::32b as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm1-x32b.google.com (mail-wm1-x32b.google.com. [2a00:1450:4864:20::32b]) by gmr-mx.google.com with ESMTPS id b6si73952wmc.2.2021.02.28.23.52.28 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 28 Feb 2021 23:52:28 -0800 (PST) Received-SPF: pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::32b as permitted sender) client-ip=2a00:1450:4864:20::32b; Received: by mail-wm1-x32b.google.com with SMTP id l22so2976459wme.1 for ; Sun, 28 Feb 2021 23:52:28 -0800 (PST) X-Received: by 2002:a1c:195:: with SMTP id 143mr8857611wmb.147.1614585147994; Sun, 28 Feb 2021 23:52:27 -0800 (PST) Received: from [192.168.0.20] (cpc1-king14-2-0-cust212.19-1.cable.virginm.net. [77.101.206.213]) by smtp.gmail.com with ESMTPSA id b7sm24212081wrv.6.2021.02.28.23.52.27 (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 28 Feb 2021 23:52:27 -0800 (PST) Subject: Re: [HoTT] Re: Foundational question about a large set of small sets To: Michael Shulman , Ulrik Buchholtz Cc: Homotopy Type Theory References: <034025b4-005d-79d1-cab1-67470b3245bd@googlemail.com> From: Martin Escardo Message-ID: Date: Mon, 1 Mar 2021 07:52:26 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.7.1 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset="UTF-8" Content-Language: en-US Content-Transfer-Encoding: quoted-printable X-Original-Sender: escardo.martin@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ZN0NLaRg; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::32b as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , Interesting, Ulrik and Mike. Thanks! Martin On 28/02/2021 15:13, Michael Shulman wrote: > Yes, that's it. And I guess you are right about leaving out the > endoequivalences at level 1. >=20 > 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 can= onicity? Since Set is a closed type, if there is a proof of the mere existe= nce of a set cover of Set, we could extract a specific term for one, and th= en obtain a contradiction in the above model. >=20 > 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 --=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/b21281e6-2de2-c126-f139-b7df3107078f%40gmail.com.