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-ed1-x537.google.com (mail-ed1-x537.google.com [IPv6:2a00:1450:4864:20::537]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6ac47686 for ; Sat, 23 Mar 2019 10:44:08 +0000 (UTC) Received: by mail-ed1-x537.google.com with SMTP id s27sf1939293eda.16 for ; Sat, 23 Mar 2019 03:44:08 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1553337848; cv=pass; d=google.com; s=arc-20160816; b=fufN1XXeGBlK13RDqDJt8EC8M5ar7xbp+5U2qIr4gV+SCiG5xSyLHuhDRuBHPnQ3C0 5JVvPjslHuol1Yv2UZgkIT2NsiNYR6TsZgxhwSH9OUVg6JQdxVmw6sNLKFvfJMqvcnU2 3PYoM2ZicRkDLYjdEnMc3ewRgu4tAmreHp0Yhw1LkcE13npcKhlW+QjroYM0Ecr0BWGJ b7dTnMGAHw3cc01LXzK/BNsJanC6prinwzsy0TD1AZbO5R/25d5dcu33wfrq2Vsbqcy2 o+Fwhp1b0TLtZ89Nm/130mMXLlPWUiUokqsKk8BIQvPvc7zWYMF3eTsF4D6ufDbXluK7 r9Rw== 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:user-agent:in-reply-to:content-disposition :mime-version:references:message-id:subject:cc:to:from:date:sender :dkim-signature; bh=hHWSKWLuqmBFTrUpOjbjK4H7dCBKz/dBgb5BleO1KdM=; b=yCuQTzn6spwt9cw2HJceiU/vN1FX6VvRddjwniNgeUkztixczj3ZtGmG7c16G46EPF IlsVtTLcj0kA44PlCIK5w9s6NBv64KvwOM5IZHbutv4aHE795335FAAfJUlcfvAZT6Sr bJhuq+i2uzwx6YsWc2MJVkvB57c4k+Yhq2IU2RxXTy0EUEAOB1IA4FBv1JZs8r8hyTzC 483tKjymicUq1RkOkRO+aNTLZVhYTh/Z1K/2qHRcbbq7XrscfpIIdmN9UTac4m61Z4NN Y3EbGdDCOxpqeDWncA+B7lTCIOu5JYzhcK80zRXyEL86YCa4H8dShvK5wGSp1xj6NNGX Miig== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-disposition:in-reply-to:user-agent:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=hHWSKWLuqmBFTrUpOjbjK4H7dCBKz/dBgb5BleO1KdM=; b=qnK7nLaSJsNSxFpoCZAgsjbhnzyMbJCjpSz64rPbfQrF84d9Xx8IWtWdT/ahtE2XaP vi3efz8oj5oVnpH3fX8QNUAX8VFvTmSK6rk3y7/O5/Rf9eY7rgb49Oyok4pjsLdrQe2w /JWyPcyHgrYHYdP0GCbNYDrxbrYHTY9TGfZLtkqwK/xu7hKx7IDBsiBpVnMZYWbmfegy VxJ1BZM2lcqmmBzR6COvxtO5w1uNU/zxQFWQO7iKsCwOuq7Zy+KtDyX2YbkBaCKa6IQ4 LBzq7OQem8V+D1TbUkyLrfz7Vc6nP2AyTTnrzGiKcv9/N4hN6k6Nyhh07xlVNoarcJfb if+A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:cc:subject:message-id :references:mime-version:content-disposition:in-reply-to:user-agent :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=hHWSKWLuqmBFTrUpOjbjK4H7dCBKz/dBgb5BleO1KdM=; b=CRHVSSpG7gsahckWD3doBbSTaE7G8TIX3s6ZmmlyavoC1CoL5ic+0VDMsVWhmwscaM LJbuxYU4FOqratWqKRibLol3+O4jXmc6zleXLucS+T8SoP/oQ93lskGy9nobIPHZZprP NZGpiCFTFV6Bah9lZsIRuGbuP1qJQjsbzxmRD6jXHyVpGIJmK30I74LMH5ay/j7DM6p0 p1VO5S+0xcwAsS2FzjsZCXd6kR7UPgfR2yUk+OG9EAkRTiyaUdo9epHcn9un0/7aMOAj V/aoEHLojnMnfvbbDdA7f40PAWL29w+annf+sNM8fGCr02mgnyIgCHS5mDXXVf00bFsW 6KVQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAU0z2GUJxjK3AQ0rvcb4Vqt55KYu4GqPPzgjplJjKYljyp2pkET /zfXHAh1+b5rxWiaO01vCrE= X-Google-Smtp-Source: APXvYqwkctp+8FRhr29VVGk86aLEyUbGkmqryOiS0UVqsiHZo75KZGLJv2IeDGr47e7fbC8AtTp14g== X-Received: by 2002:a50:a484:: with SMTP id w4mr9442054edb.193.1553337847995; Sat, 23 Mar 2019 03:44:07 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:b491:: with SMTP id w17ls514924edd.7.gmail; Sat, 23 Mar 2019 03:44:07 -0700 (PDT) X-Received: by 2002:a50:b36d:: with SMTP id r42mr9874300edd.199.1553337847577; Sat, 23 Mar 2019 03:44:07 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1553337847; cv=none; d=google.com; s=arc-20160816; b=OCwDJWL5V6J+eje8mVN5M908Epz8fDeJX66r7xqwWMDPg4yhf0XA5xfZJlsSmjT3is sLhYMC8l/dDnptLIsZKshMy/tGkpLQ7D/njZ+mvrftWYRlmIxMURLd1kxCDm8vAyOWLh COhPkqb/tPekUG7KAXHlB+VcMt8umk1TSBgw/vsJI57oOZebKfKHmYhMwB20T+hwUwUn XJXrYdiF9KlXZljFooxkY7f6p48PQ+hXdvT7mLhU9/z0DCwpymvrGimJH6+MpVRfV4mn uS/A2FIKBPEpZ/KxbW6k7zqbjDcQZzu5iv1nWhdBtnpG6MmPRCCtXO/HDXQcVX+IJzJb tcPA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=user-agent:in-reply-to:content-disposition:mime-version:references :message-id:subject:cc:to:from:date; bh=CKsHdKmjG0KbWURce/r9HZK70GwOxCVjk5mFzp0j8pI=; b=Dps/hJMQjhykEsYwg7vVfo17xqBylbcNRlmL8fuT7ZhfpHdlEWQKcMhk6ObCBxlutl BCVWyWDxF4Qs4oUUyboDr3v41qOHExDFUs9wOYVmAyFSCPmftXgr8vCfBfRAtKLwo79R iD6rWUYQ9P/mzCBW/K6MG3HKcdBAvZ9Vz9DN5nJ8aG7kPASRsYqOgpclboTwcvMj68dH NtCRdTC0YJ/BibHuNFkx8r1F3sAEfLbzjRYldKtO8iLA8Lt+uLKr3iJGi+QWq+faVq8E tZ2H/KYQXJ4PIBV44vuaAmWrvWqwfmef1qcWLTwoHa4W5mw/qrbgulpi6ZXHmE36+C8v 1SWw== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de Received: from mail-relay231.hrz.tu-darmstadt.de (mail-relay231.hrz.tu-darmstadt.de. [130.83.156.231]) by gmr-mx.google.com with ESMTPS id i17si157774ede.0.2019.03.23.03.44.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 23 Mar 2019 03:44:07 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) client-ip=130.83.156.231; Received: from fb04281.mathematik.tu-darmstadt.de (fb04281.mathematik.tu-darmstadt.de [130.83.2.21]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mail-relay231.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 44RHFg1tsyz43wL; Sat, 23 Mar 2019 11:44:07 +0100 (CET) Received: from fb04209.mathematik.tu-darmstadt.de (fb04209.mathematik.tu-darmstadt.de [130.83.2.209]) by fb04281.mathematik.tu-darmstadt.de (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id x2NAiBVC005620; Sat, 23 Mar 2019 11:44:11 +0100 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id 046FFC4C66; Sat, 23 Mar 2019 11:44:06 +0100 (CET) Date: Sat, 23 Mar 2019 11:44:06 +0100 From: Thomas Streicher To: Michael Shulman Cc: "HomotopyTypeTheory@googlegroups.com" Subject: Re: [HoTT] regular and strong-limit universes Message-ID: <20190323104406.GA10592@mathematik.tu-darmstadt.de> References: MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.23 (2014-03-12) X-Original-Sender: streicher@mathematik.tu-darmstadt.de X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.156.231 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de 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 set theory there are the Zermelo universes, namely the V_\lambda for limit ordinals \lambda > \omega. They have nice closure properties in particular closure under exponentiation but what they are lacking are closure under replacement, i.e. for all A in U and f : A -> U the image of f is in U. Type theoretically this corresponds to the possibility of defining families in U by recursion over some A \in U. On the other hand in realizability models modest sets from a universe U with excellent closure properties, in particular for every A \in U and B : A -> U its sum \Sigma(A,B) \in U again. So it's very model dependent whether there exist small universes with excellent closure properties. But of course Prop or Omega is not part of such a universe. Thomas -- 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.