From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-vs1-xe3c.google.com (mail-vs1-xe3c.google.com [IPv6:2607:f8b0:4864:20::e3c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id c109ecc6 for ; Fri, 22 Mar 2019 13:03:18 +0000 (UTC) Received: by mail-vs1-xe3c.google.com with SMTP id t85sf772468vsc.21 for ; Fri, 22 Mar 2019 06:03:17 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1553259796; cv=pass; d=google.com; s=arc-20160816; b=cH7xbuEwVYh8V0Ed0Qh8vCaFAhs5Q7vKW1I5kXR2u1Oq6bJ0PJEE6IW42novT4sHWk m8pcc4wCPOu1j3IpPXe4lTeNUpConj0E8m9zDzLK5WJbDBzGrjksCm4ndDLaSNiOFCHq eIWmfZomO7JOiVTFYEkmDfK8Sqwv4d7pDkniF0LnC8aN6Geh0vc1Smf4CaWaULAp9y9G eNbvpZmXmzVh4wuOy3MYx+9uaniCPE/JdICObzM+yTiajx8uefdHbi/cTRoDXyx5YVTc nKTSIOW4zyShNdKFOAovkXOwgnPQcipzHcqw/Fzy0kEd2TncOGjjJiFGXh4YrmbHUCNR i3Vw== 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:to:subject:message-id:date:from :mime-version:sender:dkim-signature; bh=AAq+50ReTx7cZOafynMYA9FoMDdWnGVjARDa6n158fM=; b=bzPweOI5SLSe7i+wGGMpzs398mptfeDGw108S2liqswCsq9PIrkMCccY5wIzZrwHjv 1vIweHqpAn382UtmkDiZHyeg4yWXaZzuqSoSudvk7VIEYVtsgDbISS25remuAEl+7e/B LWQtZEf358SP9STEpUPyIr2y3ZJOEady/RSdSU9xLTVF0vNJ80xofYXmjBY0a22H4VFh cpEHSGxDn2T+YMIh/Lqr70vohZnfU9I0B/qmccwFdXXrS0yEVfKK2yums1cq0YBHCiST jjJ4dSaMPlWk/t9IXJxLiCWQXqQYDpGXk/LesVIoQyLC5MDYj+x1Mky9UVpglbMZ7HHI szxA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=XEGIakZq; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2c as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=AAq+50ReTx7cZOafynMYA9FoMDdWnGVjARDa6n158fM=; b=LGVvMxF9PihR7sazW7Swwr9rvAormcUic7kYaU2gHPSbmhYCWQIKD0uOYqlJw2Y2Tx QAzRnaRpiOezsAXbqpAsxdqBG7c0gwjDBBqaHwBs54qR0nNCgg6Lld7h/zdxHnoIF3F2 6SIXW/loRH/+fXtydEjiKzuQQjNkDvUincYuXTjX6nKd7FnLbykrTRwTDALuUuKmLi9Q 2D6SbyqNpeLGtDNGOj32qi9sbjXtFjBhEWKOuDSIbSXBH657fDomPZvYbQD/IaGl/1le geP09gqPZLXuUCRbUSuU03mnUG/h9lKTuTF9uVJXSa6YFaUA2n9af2laI6Gshonbkftb sEzA== 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:from:date:message-id:subject :to: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=AAq+50ReTx7cZOafynMYA9FoMDdWnGVjARDa6n158fM=; b=M9NCjgCcTXJx33RTELRQ+CfoAbg1xx6QIE0bMY1SPv6OI1a+yLXNGdkjHrC/QkTjAq 3/NTJHKdKeBGtTA69s/BkywlzJXxIKqjoQA7APvO2UD0FEk6+r841RV+hhAuKGkh532e Q6V5prUC2TQ+bZ5fi0dDwduHdol+3FMckAtZPxEpjvbf8OmfGrmmJWvLy5v/L7JCB/w1 4rXJFBCnUk+RJR+fbzFfpDts/Kyo7PQFv2+A1nhjPZd+lj4va/ef+SseJX9VGk9EvVYe ZGzoX+dqFJpSDcx7DCrMK6XA8HQ9LbqWQxRPwxUmAYRIFiyuLzWuSBmxjRauaiG4z2hL fSIg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXDkkhgSls025keUSgIpWdiKC83rswtLYS8D7ntI0UdYJR/kaHN PFba/NL6UEFlDfwt+1fDBLE= X-Google-Smtp-Source: APXvYqySHxlW2k1yhV8XPFA0ErF/S4T2wBeF5VmM/QqtU+DPVhXfQA7EPxNcG3UVMhJzGe0hmRwnyQ== X-Received: by 2002:a67:f78a:: with SMTP id j10mr5631612vso.46.1553259794640; Fri, 22 Mar 2019 06:03:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a67:6805:: with SMTP id d5ls2003164vsc.4.gmail; Fri, 22 Mar 2019 06:03:12 -0700 (PDT) X-Received: by 2002:a05:6102:252:: with SMTP id a18mr5836059vsq.214.1553259792792; Fri, 22 Mar 2019 06:03:12 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1553259792; cv=none; d=google.com; s=arc-20160816; b=D3eIQ95jEhcTbqT9JeZBtd7q88JSpHVvDz6GlGuZiriHOL57c1dlI1e+IXhJUmrKMq Df5OedUUtVdE7sYgUYonMe+QoTzLicHVgDxEMSN/CYiWY9odOGUXSGy3v0DB1ErwdD6o mVJy08D/VR3bWSoBvMhh0tlCmrY+aXGht3uDQTHpM8KI4Kzj/BHtxWC1O9K/QC5ok397 ahI8rLJ5h7Q1P1mtNRleh6jKjsETpdGN5IgEy4/lOqBkrLZxrWLdIlucf8FZXe54bv7p Ry27JHoxp3De5pbzTzXUYRzJ2hOQEOJemmk+3ZiZEOABXo+XA0QD9iFqUVu9ScnQtmyl DEuw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=PKU6hsw2cDETLVTzx41ppf6gawSReconNnXETdFUOSo=; b=UlZuqhZMQjNzXDwxwce6JRW5XOsGtW07K6vPcJUXcEUVAgw94qk4qLx6NLkWWrFlOQ BbR9SivUp5dvd8muTeuvrcbZ+/Ob6ZKtr/cy2nLXJcQBoljA9EAF/Sz8ES4A6Yph0mFp rc1BeAW+sJGd4cwTB4+Iz15effRKD2LFIBMiU9pxztqyAUr2TOGugpagP43vXWyMqTwl vqaxlewEYuyaBJwZRK8fdAUaBU+hmqDqSYv7hn57WWp5tMnhp5aRwJm5+OHRJhTC77Om gk0BxhDeqGBSIuoUc/3cCF537a79gSWNCuzmhfz1oUod8N6PwXSaoiV3yqq86F9M7PDt 0WbQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=XEGIakZq; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2c as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc2c.google.com (mail-yw1-xc2c.google.com. [2607:f8b0:4864:20::c2c]) by gmr-mx.google.com with ESMTPS id n137si196505vke.2.2019.03.22.06.03.12 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 22 Mar 2019 06:03:12 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2c as permitted sender) client-ip=2607:f8b0:4864:20::c2c; Received: by mail-yw1-xc2c.google.com with SMTP id v127so1652624ywe.13 for ; Fri, 22 Mar 2019 06:03:12 -0700 (PDT) X-Received: by 2002:a5b:bc6:: with SMTP id c6mr7665663ybr.204.1553259792134; Fri, 22 Mar 2019 06:03:12 -0700 (PDT) Received: from mail-yw1-f51.google.com (mail-yw1-f51.google.com. [209.85.161.51]) by smtp.gmail.com with ESMTPSA id 76sm2601304ywn.10.2019.03.22.06.03.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 22 Mar 2019 06:03:10 -0700 (PDT) Received: by mail-yw1-f51.google.com with SMTP id l15so1239339ywe.8 for ; Fri, 22 Mar 2019 06:03:10 -0700 (PDT) X-Received: by 2002:a25:2d51:: with SMTP id s17mr7759271ybe.458.1553259790461; Fri, 22 Mar 2019 06:03:10 -0700 (PDT) MIME-Version: 1.0 From: Michael Shulman Date: Fri, 22 Mar 2019 06:02:58 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: [HoTT] regular and strong-limit universes To: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=XEGIakZq; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c2c as permitted sender) smtp.mailfrom=shulman@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: , In the usual constructions of models of type theory in ZFC set theory (including homotopical ones using model categories), we take the universes to classify the sets/spaces/objects of "cardinality" bounded by some cardinal number k. To ensure these universes are closed under both Sigma- and Pi-types, we need k to be an inaccessible [1], the existence of which is not proven by ZFC. However, ZFC does prove the existence of many cardinals with weaker closure properties. For instance, it proves there are arbitrarily large regular cardinals, and indeed arbitrarily large regular cardinals closed under powers (-)^A for any fixed A. Similarly, it proves there are arbitrarily large strong limit cardinals, and indeed arbitrarily large strong limit cardinals with any fixed cofinality. If we use these cardinals to build universes in type theory, I think we can probably obtain something like this: 1. For any universe U, there is a "regular successor universe" V such that U:V, V is closed under Sigma-types and Id-types, and V is closed under Pi-types with domain in U. 2. For any universe U, there is a "strong-limit successor universe" W such that U:W, W is closed under Pi-types (including binary product types, i.e. non-dependent Sigma-types) and Id-types, and W is closed under Sigma-types with domain in U. Has anyone studied type theory with universes like this? Or more generally type theories containing universes with weaker closure properties under type formers? And what can and can't we do in such a type theory? One thing we (apparently) can't do would be to iterate (e.g. by Nat-rec) some construction on types that sends a type X to some type that includes X in the domain of both a Sigma and a Pi. Are there naturally-occurring examples of such? There are of course definitions we use all the time that do involve a type in both the domain of a Sigma and a Pi, such as IsContr(X) = Sigma(x:X) Pi(y:X) (x=y). In this case, there is an equivalent definition of IsContr that remains in the same strong-limit universe, IsContr(X) = X * Pi(x,y:X) (x=y). Thus, we can define the h-level hierarchy by recursion on n in any strong-limit universe. Are there other such constructions that irreducibly go up a universe level, and would the resulting inability to iterate them be a problem? (Regarding HITs, in set-theoretic models I think both regular and strong-limit universes would be closed under simple ones like pushouts, and there should at least exist regular universes closed under fancier recursive HITs. Of course in homotopical models we don't yet know how to obtain even inaccessible universes closed under HITs, but we might hope that if that problem is solved then the solution would work for arbitrarily large regular universes as well. That would for instance allow us to define spheres and truncations recursively on n.) [1]: Apparently one can also construct models of *predicative* type theory in much weaker classical set theories like Kripke-Platek, with "recursive inaccessibles" used instead of actual inaccessibles. However, if we add impredicative axioms like propositional resizing, then I think the use of ZFC with true inaccessibles seems more likely to be necessary. -- 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. For more options, visit https://groups.google.com/d/optout.