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-wm1-x33e.google.com (mail-wm1-x33e.google.com [IPv6:2a00:1450:4864:20::33e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 925d5a10 for ; Thu, 18 Apr 2019 10:09:30 +0000 (UTC) Received: by mail-wm1-x33e.google.com with SMTP id f11sf1551836wmc.8 for ; Thu, 18 Apr 2019 03:09:30 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1555582170; cv=pass; d=google.com; s=arc-20160816; b=ZPNVXs0sfApz+95cNIHqPBidNtSVhYkrkXvbWufY7glvDvnYb5zXY91OeqWFLuMuGW /FJxmV5InOzSubg6yyqZVfrkq+02uEz5INiVmxMJMxJykT9/BSeGjfVNlq1EEncRZjqa h+HYQm2yPrDQWnWJH5M7xeWyw9plZlaBssHN5sRuvJTBbbX0ZjFxx8pmkK98n5p9nokx 2ULEfX8JfuuUv0q2scqkMDeuFlyPUoJ5ZsZeRde5l0tarPY94uXq5kX/Hr6IGZmFHdYT Ji6GYqy/fQdBq8L2Kk9HRsbp8MNYRHK3sMGR1eMyUjFkWIvS9btfAUmCNS41l9HGFdM2 /G/Q== 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=U+xjXKtv4n34hiQKPUgqkax4NXTKjNf2VMEoOMqwlKs=; b=GnzEJUPSZZthM0MvzInwAJP3Jz7ek3JGWqXRIM2O8EuuJ3DUPr8hUB9aZmQasNTWMY zm2ASRTJFGURqpe9+r+1BbNjJ4fH0qaU4Z2o2skRqBDVq+167aaT9jF3O8uKQibXtBFa BJn9H3vkuX00Md+9EtNY9ofmjwg+vZc02wCCgLjliMzJPxyD2hbzaoYku71ACyI+3slP SO+pHvRI4PnLxoNgUy/jujOD0v6fWAG1khk2c8FtXr1ZUmvwfy5WmIcN9u0CKLTnpZ// nfv5Lwqka5W595E97mi9dpLT7KEs0QXzhEJlcUHg8SOl7wDyE7lBO3dC8wYMV2E/iT79 nB4w== 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.252.150 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=U+xjXKtv4n34hiQKPUgqkax4NXTKjNf2VMEoOMqwlKs=; b=eR/cULeUZe3iLP4nXrkuPE0pVmtaDO4rtjZvWGU+4ZJeZ3KgPqrbV76yOslAUTeviL 1FNHraRu/Wb8Ccwbf2IV3rlOXoksDkdA6vx6QhvmMgw/jvVJyqoE6KBzy7vPRR8eXj8G rRoaEWNabDGTYoi1jx2KKvmzgskat5ur0/UzF4JY9jpoMgheonE+ZZtSltc0wbw9f6nb zkjQwlf/n8WcssPMPo2DPGceJpwUswYq1C/M0H8EDBNZbf5J054LLxXDpMvxmbAFr/OK MwbHOdOjNsboW31/wnlvDOkcKYIJbiD1b0RGKL5tnBUvwzeqF54ExSna4AImvSMfNpYs PLeQ== 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=U+xjXKtv4n34hiQKPUgqkax4NXTKjNf2VMEoOMqwlKs=; b=gcJ/f3FEXdMzRl1H+rt+osSON+WOSVBQWr5otsFYZfqdNqqUGOHS+JGF2GE3CdUk0K T43+ttpLjQ1qub+rdk9uvQIxZde7nvnbRTU4O73DOb5PSnv39HD2xgwBvwKydL2krDee 4/UtQOzsfylyCbhKCrks/5o8nkEPHcj9OeFGeuLcT2fIfbSPms6fCiwz41h/CiL+C/Wk lO7lQGKABWAn7pHaEomVnkIZn3RXjMnDJfhaDBq1EzfkyWV4vBtAwzVEkRh28RE+jodF q5afh5TIWEnstypJGrldiDc2YROXlsnCf2YhBw6PzBddQSSbwNIggvTyFcRyVtGUIizL NuaQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXleS9pZ9t7tZX+TZ/XgfLuI3tu+QHx9IpoTSYEOyy3ntPttooT oOR35LrhZDraTYgUK90LCZ4= X-Google-Smtp-Source: APXvYqxCyacNdnoyV0uzFqoEYjIAjgu4vf/tfwxeh9WQmjKlBI5760MSIz/dWFBKO9TqIlfQvRAVhQ== X-Received: by 2002:a1c:7208:: with SMTP id n8mr2602136wmc.46.1555582169921; Thu, 18 Apr 2019 03:09:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:6342:: with SMTP id x63ls502485wmb.0.canary-gmail; Thu, 18 Apr 2019 03:09:29 -0700 (PDT) X-Received: by 2002:a05:600c:20d:: with SMTP id 13mr2469363wmi.60.1555582169480; Thu, 18 Apr 2019 03:09:29 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1555582169; cv=none; d=google.com; s=arc-20160816; b=A06IUGA0dyYknQVJoCbNlZM1lyp3uRT9xtJwrNyN3Uqm55SHRpUCfAUnMKrwntUgwV BRMpoZqjGHNMJ/TLr5g88hNHT2C69yYmJt/CtCLKmufzwGXWRAnviExpSdp0g+CFu40M CRD5m58lm8l2BLcIiFbxIsBhmgquNSp7wfzJjAVg/XwqwRa7VL7FdrxYz7cKPxJ2i33h PPUy6HDg4gVZo6l32qRpJiKoFWcylrubeZ+2AHDbiywzulMyA+cFAQ/piLAZnAkLLI1L EB7hjxlJtMB4k9Zz/k/72GVMC5/00dhnJhQx0aKvm61cVFeBCsK0D45VXemFzQ3eBaa2 Ua4A== 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=/ah/FhChDnnvIAtlYK8yEvQuBdxYgmqWVmMhKKLfRFU=; b=LM1GT8e5bmATu556guTDeS6/L2mfay2qxqJxIst/CEZ/095LktOMmNULIUQg1L4ek/ oUHBeubaHtAbSk6BxnBfbeXqX9HG4h1uh+lnPdqjMHFoGdz1SFs3IWPQ/dIXaLRYaxst dkCc17Oo2Hfcq/7dhy5XPX1gulBGz542AUxU3anKWTSqUiAN5PeETXOAO2WZ55iafZOX J/jjwBPPdWTB98ScGpWGd2Ro4Tl1DPHI/7ksq5JYBEndYBmQhHgL9rmr1Emcicf4MVPM hkKw0RkO1+RuztCyhJjv2j+T6lbg2pFwX48jfDNDQfCqXRsUFYEBPi+fWRAq+R2cDHQW opLQ== 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.252.150 as permitted sender) smtp.mailfrom=streicher@mathematik.tu-darmstadt.de Received: from mailout.hrz.tu-darmstadt.de (mailout.hrz.tu-darmstadt.de. [130.83.252.150]) by gmr-mx.google.com with ESMTPS id p14si140490wmh.2.2019.04.18.03.09.29 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 18 Apr 2019 03:09:29 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of streicher@mathematik.tu-darmstadt.de designates 130.83.252.150 as permitted sender) client-ip=130.83.252.150; 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 mailout.hrz.tu-darmstadt.de (Postfix) with ESMTPS id 44lFFj1Mwzz43pF; Thu, 18 Apr 2019 12:09:29 +0200 (CEST) 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 x3IAA52P028278; Thu, 18 Apr 2019 12:10:05 +0200 Received: by fb04209.mathematik.tu-darmstadt.de (Postfix, from userid 11003) id EF47BC4C7E; Thu, 18 Apr 2019 12:09:28 +0200 (CEST) Date: Thu, 18 Apr 2019 12:09:28 +0200 From: Thomas Streicher To: Michael Shulman Cc: Martin Escardo , Homotopy Type Theory Subject: Re: [HoTT] All (???,1)-toposes have strict univalent universes Message-ID: <20190418100928.GB24001@mathematik.tu-darmstadt.de> References: <655fcacc-0d88-47f7-bcf6-3a0e27ea10fd@googlegroups.com> <7724b923-fc14-0bd2-57b6-ba341f5641bd@googlemail.com> 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.252.150 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: , I only had a rough glance at your paper. But as it seems you don't interpret directly in the infty toposes but rather in some representing model structure. No complaint because I don't expect otherwise. In any case it is quite an achievement to get universes "strongly `a la Tarski". 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.