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.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FROM,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 32593 invoked from network); 26 Feb 2021 20:33:32 -0000 Received: from mail-lf1-x139.google.com (2a00:1450:4864:20::139) by inbox.vuxu.org with ESMTPUTF8; 26 Feb 2021 20:33:32 -0000 Received: by mail-lf1-x139.google.com with SMTP id z22sf3680882lfd.23 for ; Fri, 26 Feb 2021 12:33:32 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1614371608; cv=pass; d=google.com; s=arc-20160816; b=z5yfPXhyyOZ4hnLfb8BqROx+ZLLVH91ONeuPNnhdp3dxI0ifSj4P640wsRnq8XKncd LdNJtvWUleU0tS5DK6mA66hzt/AUEHKGbisqZSo+pPeBGItc9Z4FtVqM7wLMFm428HZY Wu2LZRm6UsQan4t1QYx9mHVALPfUECIFJcoIKss2QrsYZtd7aJUNLQRQ16qpcxsRmT4s +HzA42e6/10jWlszXpTlsBant2yDOnxyQiMg8+bCZ6LDsNbjfJzpsL1g+mU9EWVBVGwY fKPBzQzGpBQ8rD+Jk5p7/YTFuYYWwRZKYDY+Rjch6v9faCYqwsLqGPvzn33DI4GCekWN cydA== 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 :mime-version:user-agent:date:message-id:subject:to:from:sender :dkim-signature:dkim-signature; bh=LZgEYV4kyPqQ4eTcoVRVJ0JMeQRgeljLQAph83s+aZQ=; b=Jn1w6dppw9uPaJUcr8VUxAiF89TirsBtGUWUgsHaHoytRfp6rd0KI1AQjjpiw8FRaD Js8kFSN7THWN2XTmMgmactwxN6wueDX4R/30As78Q2s4TS0tQjpQwd1SFh3f11LwrKBT 7fA4qeO4G+bvw/Y+gpFILmvIdgdf4ZVkTWAtY2I6QeVtEWmUWlIRixW82VW6UxTSIFVM FJKFIKwSLrx3Zcqef0bZZ7dnMlDKWe9RTuwAb7rM0VfvLUqFlh/4GoN/FsQvL2/CyvjP hWjuzmlViS3SaeMW6FLnNjijyoF9ezPTFI160TAyWP+l5VsFSW/pORoRCA3ygEwGy/01 q9kw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=WQP3BOXb; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::433 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:from:to:subject:message-id:date:user-agent:mime-version :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=LZgEYV4kyPqQ4eTcoVRVJ0JMeQRgeljLQAph83s+aZQ=; b=EGs38+TvGTdAS2PwmWnZKf664ytqST9AdRWY1pXgAWx+5lIE3GGnX+OSYPU6M0DEr8 XY21t22qRYgi3zF++rGd/CFF87IQdDDbG5fmP7e2Kb25JIgjWL3NEVwjU75/6l53JOev aVWIcdTprLhh3/TPoeuutf1uM2mynq10SqQTvNZRlKYLVMVGZB6M1ghWsSa9NXovhPHl Oage0pJ37eiF/qWPDE/Sjlwid3sUn6LSLA1CjLHljvHynp40qA6/puvp3CG4Fq8q8ZUi wlNSXI2gz4DN+hpjWp2dIPJwdM3twhE+XAZBItmRC4JoAqYLawX0CO22IVeMhGZ3lZJA z/lA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:subject:message-id:date:user-agent:mime-version :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=LZgEYV4kyPqQ4eTcoVRVJ0JMeQRgeljLQAph83s+aZQ=; b=NDhx5aK+Vep0LXDF7xm9zPr7xKb8q750J71Ln8LOa7dfQm18tHVb+2wBmGBP9iShJ8 8VpzWoUSFXvvWSyQZogVRgpKScdxRTI0wI+Pe6w/CXYm0gKAFVT1mt7ghay/GBs5vbqd JQ0fVoTqdIHmHBAg7o1KgCI0oMIErSttqBuBAXgONK6n8xJ7HnplyA8NF2+Wr3g95bOF aDwSqELD9OubAUoWsfXhrsLtud20AykGNFZEEUtQp42QAFNsj1LRZMuuivynpBaEKltU RxR0d/G0iZKJL8y+z0tIbb2jrb2hDwFMFavAKJXe9+3u8uLQdXsEwD/Ae+jrgUkJv+rV o6SQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:message-id:date :user-agent:mime-version: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=LZgEYV4kyPqQ4eTcoVRVJ0JMeQRgeljLQAph83s+aZQ=; b=Y8I1ALA7PBZXji7fGMtUEFKNTZ+kv441eb40vX1m9kSprGz7NOyN0SZMG9zWspT8TQ pdYDPAMQ0PGbytHYCZoQBVQEf65FRZ1EOul83cANOTV/mdUhhEivwdXpG7fuNsjRqMBy u2il1zd4ulJRrmn3vQXLM7GFHqIz1k4CO1zuaN3tt8rd98TuUsxGWwWiK2/WWWdaGWph 04B/1tGqU7I4G7nzkb1Fci71mIWdn2xX6bLhobNPQtpCLJey60jm6DcVsKV2btsxCk67 GhgEDMudu62EhjDJ3TJzgPn4fVY3wDwnTVM58Ckf8Xz/nZptumg+FqfmKilCkXrqDN8u pGog== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533KnKr7kKfSD49AjrEnKfDr6uDRU6fsu8lg8KUo4fcSzfokhtjO neG1D5ceBth+d4kuQNwc+q4= X-Google-Smtp-Source: ABdhPJwUXpSmLhtpcUQDGJ2PEdO9qFG6JMz0EbAcpS+kzvMhRl6c4bKgDx3oSTZNND55U/tjljFmWQ== X-Received: by 2002:a19:22cb:: with SMTP id i194mr1534890lfi.191.1614371608185; Fri, 26 Feb 2021 12:33:28 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:8915:: with SMTP id d21ls1733364lji.1.gmail; Fri, 26 Feb 2021 12:33:27 -0800 (PST) X-Received: by 2002:a2e:804f:: with SMTP id p15mr1028159ljg.373.1614371606539; Fri, 26 Feb 2021 12:33:26 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1614371606; cv=none; d=google.com; s=arc-20160816; b=Q4fWDPfDQ5SY4yvpbIaUvn6YEaD1S304JjDX4iBwzSoW5dectQSUZBYTRvZgsSfUfT xJb2DGsdhUiGe4rmlIfF+AgwPX/ir/bCb5kd0GS5Z+x3oGPPT8EA4Gl8qJCl8Y+sOC0c n3Yw53Ay2rN3QDPcqJZRHgA399cOQ1FyceYT+YFWGseic0bXRMdoXTASMOqIjPCdegYI gqdyfxoYixnlPK1f2IMdwJVHvwkMoOV1CXacultoGcO037b9ZFDr3i2HnZNKYNjKJYfN JM6z6it4WjxxkcNstTe14/pbjYP8e8ujus3STgUVQJi52/38DKXLI3hkx9DgeGPy3pjb /0Kw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:mime-version:user-agent :date:message-id:subject:to:from:dkim-signature; bh=t030K/r9B0VtmwWW/KjPISnCsoXbM/qmEvKP8NDDsFM=; b=SM9dFebqp68u/jzSftQokZxPQQuy//tHmhdkgSdWfhnOEt6RAXkQ/seUKElqjFV5CV fl4yU+5x/7HZeS11nH4juACzcSZH3q9zhMWlMQ72dR/SwE8tin/O10bApsoXAv89uAwW LHAXtqIrwQ+AkDnHJIEsWdzMl643ydlF16oVkcT/MX7kRl3ycTKJak8X19BiDnCyTqk6 HxLml2lv2APkzh6E5ISyeypza89116wp2Ouhdf3NTgU/thcKDnsejTwZ1l7+8IBTmHMY PbePr1Rone/0IjoKQ+NllxwgLMfBcwRmh2+B+H6CdY3JPtWBkO7iverhM8lUzi6aBjwM 0DTA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=WQP3BOXb; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::433 as permitted sender) smtp.mailfrom=escardo.martin@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wr1-x433.google.com (mail-wr1-x433.google.com. [2a00:1450:4864:20::433]) by gmr-mx.google.com with ESMTPS id s5si532405ljg.7.2021.02.26.12.33.26 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 26 Feb 2021 12:33:26 -0800 (PST) Received-SPF: pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::433 as permitted sender) client-ip=2a00:1450:4864:20::433; Received: by mail-wr1-x433.google.com with SMTP id e10so9557195wro.12 for ; Fri, 26 Feb 2021 12:33:26 -0800 (PST) X-Received: by 2002:adf:e542:: with SMTP id z2mr5102484wrm.37.1614371606062; Fri, 26 Feb 2021 12:33:26 -0800 (PST) Received: from [192.168.0.11] (cpc1-king14-2-0-cust212.19-1.cable.virginm.net. [77.101.206.213]) by smtp.gmail.com with ESMTPSA id p18sm3622242wro.18.2021.02.26.12.33.25 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 26 Feb 2021 12:33:25 -0800 (PST) From: Martin Escardo To: "HomotopyTypeTheory@googlegroups.com" Subject: [HoTT] Foundational question about a large set of small sets Message-ID: <034025b4-005d-79d1-cab1-67470b3245bd@googlemail.com> Date: Fri, 26 Feb 2021 20:33:24 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.7.1 MIME-Version: 1.0 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=WQP3BOXb; spf=pass (google.com: domain of escardo.martin@gmail.com designates 2a00:1450:4864:20::433 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: , Is there a set in a successor universe =F0=9D=93=A4=E2=81=BA that embeds al= l sets in the universe =F0=9D=93=A4? We can consider this question in models or in the language(s) of HoTT/UF. We can also consider this question constructively and non-constructively. I am interested in constructive answers in the languages of HoTT/UF. But of course answers in the models and non-constructive answers can illuminate the question I have in mind and so are welcome. In the presence of the axiom of choice, every set can be well-ordered, as proved in the HoTT book, and hence a non-constructive answer is yes: every set in =F0=9D=93=A4 can be embedded into the type of all ordinal= s. But notice that this is a (necessarily) propositionally truncated mathematical statement in HoTT/UF. Can you find a set in the successor universe =F0=9D=93=A4=E2=81=BA that emb= eds all sets in the universe =F0=9D=93=A4? (Say from the material available in the HoTT = book.) Martin --=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/034025b4-005d-79d1-cab1-67470b3245bd%40googlemail.com.