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-it1-x139.google.com (mail-it1-x139.google.com [IPv6:2607:f8b0:4864:20::139]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id da7b7f1d for ; Wed, 17 Apr 2019 23:44:21 +0000 (UTC) Received: by mail-it1-x139.google.com with SMTP id t13sf4334972itk.0 for ; Wed, 17 Apr 2019 16:44:20 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1555544659; cv=pass; d=google.com; s=arc-20160816; b=Pn4ijqtxOCtJF+efzgerbUbotkojXR7al/hifwyEAdhWkIspSEAzum5jV3h1W/F95G waBFIAe527bnOKfflDir5szFdlWHjqy+FYx/t3RXCaRelZ1U30CEbG9zfJetXcneIcV/ DrNxBQB+fMcACscgdV4KMRvWzuOwBvSIVqRVXajk9a4Psvzz/Tx1D6FpvDBdvJIIeHuD UQHuUF3k35XF6N9QIq1lPPQUgkbpNXgELartRmpNqRxJUjkD/e4VKQ//FEaXp/uTrSGz YMlGQs5qRCPQIcPfKvRaagshNcRUxaEHtBUHKeBqe9oaf2Q7TTkTptv86hruiubOS9v+ 2XFg== 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:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=htaXuYKq02anQT2/Si+xz9PDKFgW2PniG4fA7NT0N1w=; b=Muh7Ri4EEosS3ndiVAy6dtlm2Atzm3Bt7kSX0Clet0MUvIroWPWiQQfRNOt7BMVSEQ Ih6Bv3KuvPBcGVdZVXJwai5TUNlpFwOkdPfK+napEkOxwTwwo57sJpTXX7oCkZJGqnM5 dwibEveXgjI47w1vM8TEV5/RHNThFRHzrGcgaBKcrC7v+j2JVqQdd3HdQculHHD9vUSX IYwlAOEnrVnryjKAsrzDUiKhNGlOA+5l8jjHoIX7ChdppRdinA+T2ZfdVpy/Y+RXp2hu gScims2pFAICo+Ory950seEv17hIgO+aZPIh4XE19bkqpente/Y+Skt09Te5wV20S2ro DzHQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=r2A1DoXE; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c36 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=htaXuYKq02anQT2/Si+xz9PDKFgW2PniG4fA7NT0N1w=; b=pnR14dfpSdg8+I7WIhkYIdgXSjFeW8tWyTnIXeZ+1da+LHomdHizFRqWcLSyevB1Pl JMkeD3OivYXULOrUZ2zjfXmLaUKBT7vyO5fO9zEy5tKTnkNQzyS0DPnZlDA9Mm6Lvjs7 N4gdYWXmZyo+wKSg0Q15/e99IzMCEZEYAn1hN/r/S/iLRgEUk9D6AWwvm9bx0JdpT7WN Cf5HpR/ZWyQ3K9orSgUguLsvxYkZalewuF7/6eGwLFFbL937+FlXc7mQXLbpvy/4IOUb 0ihKBarOdPgeUzD3u3qenOOltBDGAS3cyEhurZ90vlIfprpk0O5m+QArtdJGXXCKPQK2 Wjrw== 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: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=htaXuYKq02anQT2/Si+xz9PDKFgW2PniG4fA7NT0N1w=; b=sOM64lA3AGJmdNoVWBxj+7AfHsdSlwUcoOybkC/pPAPx3Iw2wUQEA/RuzXIOrektBt MRsozjuzLabQ4ngEBZO/097BJj9iWay4exLd9y/DygzAbl6lQ5IIHLUi4qzgqwYEOV40 RxA+B0RD9pcXZrh9P1N2Fu5AwOE9bRmZcStefl4jgkgg8KncJY8FRxcNWaiejI2BeEAe kAq0X6wnvSK98PdmGNJSKE2s5HzNS4yqWZLFT7kiOjRX4a0yAO1GRQ+kXi0VaMVMocdx qlW11xSuF4x5RYKKxyfyUQtv+30ywQ9B+NPxlLuT2V7l04KlHjAr4H3GKu/nDtMyP2RI 4j+g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVoLd2x39kEThVpOf6ODbGZwZrKh8cfu0hcHXvdLvPaP2Eelvqu JMOb4/HbLxEZy3P+5ay6plI= X-Google-Smtp-Source: APXvYqy6omSFBgLGsr2nHWbSCzHG3p4jp4xZjcGi6pRVARWcPkTtbaCMMDxs88uatUYyMhHfHkAbSw== X-Received: by 2002:a05:660c:685:: with SMTP id n5mr1100034itk.57.1555544659564; Wed, 17 Apr 2019 16:44:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a24:455f:: with SMTP id y92ls112482ita.1.canary-gmail; Wed, 17 Apr 2019 16:44:19 -0700 (PDT) X-Received: by 2002:a24:1d15:: with SMTP id 21mr1064737itj.164.1555544659161; Wed, 17 Apr 2019 16:44:19 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1555544659; cv=none; d=google.com; s=arc-20160816; b=Sg4WWHCSC99wTF6u2LcO4u5qnUakG4WnGzr3nY4D5QgGsp70KiUG1C87CRWCbbSUud zF5gmozHukVtlWAkvpnN3Z1wPSxmhobUS+3+CZJfo6QQBLsCRP7r2zmZhX3WFHJZMdv+ BKKGoGFn0nB/g9Yyf6cDySRQK6T7kv9v5PLHzmypqRjGG23Ysr40P7WR8qhZZOhcrWnJ U3OSrf1jJ5K6lpmaEpeYvXebhB6YSLecO6HM8cIZI+UB7AX3DlubXWNVd3QMaA1oOFFk ilVq/EOeNZzxMfQLhSasm+mDBrMW8pC1u1LKezx38PDz0jJ368RX5pD3viNYhJpTwgEQ Mkiw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=kWJiMw0GNvj91vec9NL/ZZBMMTMAORahWyfrBsXxMhw=; b=JPKxCWMBnEVt85kHuWnPzbo2KvlG6kKA9L1GOc1E9YeuDdIlnvYETdUXyRBAqe9iL4 ndt4rGRoYdLi03v+xfvgQb4pWC5b73MnYgbO9WPSiP60L97kMeNwc1Bw3e7gxJdVYJGM VlncgrS/gRPpT3Pr9j6nEsmq3MfJ+ITkc7UIo6zV26ne6+I/8t6a8jsSuvTYLDfjkkff Zp86xPqN4sNI/mZX09ZMupPuP0qrd1wBPo0OJcRT64pgKvA6MVd3bKnOMPd5M3QBc9d5 GkJGYlP+sWvclz+ahp3eF6FjZQHTyz2bHei68nE8oARodY+auPKmxNtMLHHwAoaOO639 CZtw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=r2A1DoXE; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc36.google.com (mail-yw1-xc36.google.com. [2607:f8b0:4864:20::c36]) by gmr-mx.google.com with ESMTPS id u1si412513itj.2.2019.04.17.16.44.19 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 17 Apr 2019 16:44:19 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c36 as permitted sender) client-ip=2607:f8b0:4864:20::c36; Received: by mail-yw1-xc36.google.com with SMTP id e76so136375ywa.9 for ; Wed, 17 Apr 2019 16:44:19 -0700 (PDT) X-Received: by 2002:a81:4993:: with SMTP id w141mr73264978ywa.126.1555544658527; Wed, 17 Apr 2019 16:44:18 -0700 (PDT) Received: from mail-yb1-f169.google.com (mail-yb1-f169.google.com. [209.85.219.169]) by smtp.gmail.com with ESMTPSA id h3sm127511ywa.61.2019.04.17.16.44.17 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Wed, 17 Apr 2019 16:44:17 -0700 (PDT) Received: by mail-yb1-f169.google.com with SMTP id p134so201007ybc.4 for ; Wed, 17 Apr 2019 16:44:17 -0700 (PDT) X-Received: by 2002:a25:5285:: with SMTP id g127mr14525279ybb.202.1555544657555; Wed, 17 Apr 2019 16:44:17 -0700 (PDT) MIME-Version: 1.0 References: <655fcacc-0d88-47f7-bcf6-3a0e27ea10fd@googlegroups.com> <7724b923-fc14-0bd2-57b6-ba341f5641bd@googlemail.com> In-Reply-To: <7724b923-fc14-0bd2-57b6-ba341f5641bd@googlemail.com> From: Michael Shulman Date: Wed, 17 Apr 2019 16:44:06 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: =?UTF-8?Q?Re=3A_=5BHoTT=5D_All_=28=E2=88=9E=2C1=29=2Dtoposes_have_strict_univalent?= =?UTF-8?Q?_universes?= To: Martin Escardo Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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=r2A1DoXE; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c36 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: , Here's a brief summary of the steps: 1. Every Grothendieck (=E2=88=9E, 1)-topos can be presented by an accessibl= e left exact left Bousfield localization of an injective model structure on a category of enriched simplicial presheaves. 2. Such presentations are right proper Cisinski model categories, hence (as we already knew) model MLTT, even with many HITs, but not previously known to model universes. 3. The fibrations in an injective model structure have no explicit "cofibrantly generated" description in terms of a lifting property, but it turns out they do have a fairly explicit "algebraic" description in terms of the rectifiability of homotopy coherent natural transformations (a homotopical version of "coflexible algebras"). 4. Now define a presheaf U by U(x) =3D the set of injective fibrations over the representable C(-,x) *equipped with* such fibrancy structure (suitably rectified to become a strict presheaf), and we get a fibrant and univalent universe. 5. Finally, any accessible left exact localization can be presented internally by a lex modality (using the recent characterization thereof by Anel-Biedermann-Finster-Joyal), and the universe of modal types for a lex modality is modal, giving a universe for the localized model structure. For more detail, you can read the introduction to the paper (or the whole thing, of course), or look at these slides from last month's Midwest HoTT seminar: http://home.sandiego.edu/~shulman/papers/injmodel-talk.pdf On Wed, Apr 17, 2019 at 3:59 PM 'Martin Escardo' via Homotopy Type Theory wrote: > > On 16/04/2019 13:06, Ali Caglayan wrote: > > Mike has released this new preprint on the arXiv: > > > > All (=E2=88=9E,1)-toposes have strict univalent universes > > > > > > Quoting the abstract: > > > > Thus, homotopy type theory can be used as a formal language for > > reasoning internally to (=E2=88=9E, 1)-toposes, just as higher-order lo= gic is > > used for 1-toposes. > > This is awesome. > > Perhaps it deserves a short explanation (or at least listing) of the > crucial steps gere in this list. > > Best, > Martin > > -- > 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. --=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. For more options, visit https://groups.google.com/d/optout.