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-pl1-x639.google.com (mail-pl1-x639.google.com [IPv6:2607:f8b0:4864:20::639]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6ae3111c for ; Thu, 18 Apr 2019 10:17:16 +0000 (UTC) Received: by mail-pl1-x639.google.com with SMTP id 65sf1221014plf.22 for ; Thu, 18 Apr 2019 03:17:15 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1555582634; cv=pass; d=google.com; s=arc-20160816; b=ZckwNz1yUH5OlUIlX/6SHZCPSj/fpzyA8qG8Kmanz/E7XbP0YIxudg4Ov8JzZvMhF1 7tkIUvEU+nLtfKsTmk6QWdnDVMAPHGLLU4AMwKNCwYUWSalZJscau0hEzuUnP7sqQhgD TY8K6r2JtAm9llA3YtIJYSQbkLk5pGDpSmhIKBbj2B5N9UXUtEaPKsAzyzW/PQlPCX9t 2TWqsKSmH0bP/gJ3rFRGwn28rDh947QdGPXAduYvXh3M8JIH7FMJar8NwWAP0KRl5siC wwgYYdYEo+47C44PPAWODT8bBEYAbv4baf6jnHFFLaFAVZFzdP5+yJ092OORhPzvfxbv FgjA== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature; bh=X2pQvpZSRWagVh4lCRqvuJ1y3MiiD5XmQHXxk8CgLKk=; b=C5ED7Rq8bYSMJPcD3x0G3qj9RkmOvK0KLgVscEkt8ehEOAtlQTyMWIZhaDK61KtIGd 50DqOqzhiNKUDCHMBXOn9XgvhPEBRyax2dwfITHfiQcmf7onFChXfSaeakEFDMWlS5ka Emn7wtJghdzBUrI9FGRh5Zitqrx7pqlw1qAImbxLbhvXnHEdj9ptl4HaFzsIGL9nBmm/ mBItNA3XiDF7LJVBtYmDFALQ6ehGeOHotmliLEOHK8nbv3FiLm7JQNt48JBRAjOoR+0V c0Y6FXCDRZrbhdot6ySReatMigaVBMzmIdl8VV3Qk184FchmRkPvsgIoE1rcyU2qSbgU 71yg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=iqWSAAo2; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c35 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:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=X2pQvpZSRWagVh4lCRqvuJ1y3MiiD5XmQHXxk8CgLKk=; b=ZF11jU4P/Yiz/8ksoo2WAR4zX9y7wYYFxPZGXWm+i0PVJoRSqCjvPLMRfjbOVbtVwD Rda9AHn4Er2NGdAZP3ELBf1x9RZ0mwIN4Ur3vyN661exS7oJfrX5Avce0qNkvjUHiHnr YOobZ9cPJh46N85mV2paSUcIzTtLofyLOGiFZFA9TbXjhrBtS2My7MdwsJO/IYOLgLdA aw9/dmWxlMvqZr1Spb3Xcqg8lim/XowDW7q3m6Zo+vidpEQ+mQmzEHUZALhsN1X0FlxY C4cFPW7KceyaASdxZ/orO2ZdZtrYJATVOMJUw0NModTuH2P08VqG0Gs5B6b1pi3GYn6n 6wOw== 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:references:in-reply-to:from :date:message-id:subject:to:cc: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=X2pQvpZSRWagVh4lCRqvuJ1y3MiiD5XmQHXxk8CgLKk=; b=aRlR84CgPF8KpEAm/UBsj4/y8bbLCOlWpkYVseC0nwyl+mDfKDXUfbIF9dSryqT8/Z f84tEsgMXrAGDo0Z5aVYP2hVF5KdWWA9fkYvyK4Boa6p4mSmdmRgv7/h1EDFpyMHYHtX DlWML9Dmzqa9K1xoLnpuh+OY7ne06jXfg6hNMXzyht6j7PCd57rQudYIm/kgpR6m9GNj uxpSAT7gbNXFCSD1vQI74Pw5NZCZ7BWLYAamRAUjDSxAofydmiYoVdSU59bqpdCZbnjQ uxjLzor7kUljXhXh/3rIrObCCuPHhFSbmIZ0gcxxWeig35EngQvrg2pcvtweKiJMfHjB YDpg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUpPn8LDd6M5iQqu/UvbKIznELXu6OyqoObcQUn0pudF3cJZ6QX rNfWQDBwk4pTabllwTp4jbg= X-Google-Smtp-Source: APXvYqzZ+MASIkmXrYYE8br4KvS/LzCPbZtZtzoqL/HO6ScKllNU780K3eCfiw9eVFwfURPYO5GnSg== X-Received: by 2002:a65:6289:: with SMTP id f9mr88881625pgv.380.1555582634655; Thu, 18 Apr 2019 03:17:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:bb8c:: with SMTP id m12ls566310pls.16.gmail; Thu, 18 Apr 2019 03:17:14 -0700 (PDT) X-Received: by 2002:a17:902:7044:: with SMTP id h4mr50764251plt.274.1555582634279; Thu, 18 Apr 2019 03:17:14 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1555582634; cv=none; d=google.com; s=arc-20160816; b=B+MgS7RdCLP2xGKRUmwFoz23UIIcVAWuCtRn49a1sRxik0pI8RmG0ceLsDFvtW7Bou N2FGntKuYe3hK42tqPKSfyxB591ZkG7XOkT0fy+Eq/QPv27au0NaI2CVfNyShgKRP06T V2Td0gGp+xj0GPRmc7JoZXSLgtOB2LdpNVnL+ItH2ejfBLbzD6fkDbY2Jfh4vqGyxDbt CpgAAGE7Mu0iKtTu3Zl1iTCbLeSarqebJlRrnf9BD2Be4S3f4rfPxSi04EbCFOikF7AS UWPpiXdMqNhegy+ARzDCNA19+cm3Hm2jXRlar5AifmNV7S6Hi2EfGyqYddLSfDODm0q3 CtJg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=jUZoe0k/fyPoJUcbfxAV3bNGxp8qur4r8XjfyqxuexY=; b=EyHixKT3E6SfI3fRiN7xAieJxKA4cphkWKOS7Xp3ww79REwkXKIdNABQ1B9clPdlGO 0Ti37dpswOVJdo/7gRf5DPbRkYsW+L4UCTuvwhYxvdN81tpWn/Q/SndkZXDRW3XQQk2n jU3UehOq0egPd3Eb8IaMD05e6DWCgaiMzJ/HAZcLsDPC/L/YV+RIISsiikCWEPoX04zd PwyzLNqT+pzlnx475FdhOzWUXuv2gfM2taqxx3Ce38psg1TT3qQ/4fvhrT6LUSWIgLXZ zITnJ8Wmbv7xyKRbDjrIRhkYZ4ODRYtqFZ5vbekmb9TjOwj1ytPxSUJ2jglGSqjUYDou Njwg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=iqWSAAo2; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c35 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc35.google.com (mail-yw1-xc35.google.com. [2607:f8b0:4864:20::c35]) by gmr-mx.google.com with ESMTPS id q203si118506pgq.4.2019.04.18.03.17.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 18 Apr 2019 03:17:14 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c35 as permitted sender) client-ip=2607:f8b0:4864:20::c35; Received: by mail-yw1-xc35.google.com with SMTP id u3so90802ywa.13 for ; Thu, 18 Apr 2019 03:17:14 -0700 (PDT) X-Received: by 2002:a81:5788:: with SMTP id l130mr32591344ywb.372.1555582633408; Thu, 18 Apr 2019 03:17:13 -0700 (PDT) Received: from mail-yw1-f42.google.com (mail-yw1-f42.google.com. [209.85.161.42]) by smtp.gmail.com with ESMTPSA id 80sm532313ywh.97.2019.04.18.03.17.12 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Thu, 18 Apr 2019 03:17:12 -0700 (PDT) Received: by mail-yw1-f42.google.com with SMTP id j66so559332ywc.10 for ; Thu, 18 Apr 2019 03:17:12 -0700 (PDT) X-Received: by 2002:a81:a410:: with SMTP id b16mr51834044ywh.421.1555582631942; Thu, 18 Apr 2019 03:17:11 -0700 (PDT) MIME-Version: 1.0 References: <655fcacc-0d88-47f7-bcf6-3a0e27ea10fd@googlegroups.com> <7724b923-fc14-0bd2-57b6-ba341f5641bd@googlemail.com> <20190418100928.GB24001@mathematik.tu-darmstadt.de> In-Reply-To: <20190418100928.GB24001@mathematik.tu-darmstadt.de> From: Michael Shulman Date: Thu, 18 Apr 2019 03:16:58 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] All (???,1)-toposes have strict univalent universes To: Thomas Streicher Cc: Martin Escardo , Homotopy Type Theory 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=iqWSAAo2; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c35 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: , Right, I would say that interpreting in a representing model structure is the limit of current technology. Maybe one day we'll be able to interpret directly in an infinity-topos, but not yet. On Thu, Apr 18, 2019 at 3:09 AM Thomas Streicher wrote: > > 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. -- 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.