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=-0.9 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-pg1-x53c.google.com (mail-pg1-x53c.google.com [2607:f8b0:4864:20::53c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e23f1cb2 for ; Sun, 23 Feb 2020 23:56:39 +0000 (UTC) Received: by mail-pg1-x53c.google.com with SMTP id n7sf5498247pgt.7 for ; Sun, 23 Feb 2020 15:56:39 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1582502197; cv=pass; d=google.com; s=arc-20160816; b=wPjmqYXA9/8LnYWihFwcR6uVB/u6bk9j+Ndb6l70rSqwnZx9T9XFGS3D+3Saw7glN8 3+/jvXOeCL0gKuxF9+/0SQkSjGpv9wb/uzbWuhXRgKjeajJ74LEB1n4HrYZBbVUXsGFu dVHAu8bV4AMkxsSBL3Q/svA7nMLDdXeVpimWS0vOTQ9BXVTJHUZvurYmDmCrY+ewNsox VhBGAQrz4CfLGYPe+SNH0MqBaYSdnqYKFhWGt1e/IK+92TFishpZ200H9JhGlZVphjti cSZg48dCdkOMwtV9UBoRe8hpRFsD9xQal/jHziR2iLahHaxiJdaxdwZ0lap32JRd07Nd lDEw== 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=gnTekJ258YPkBVdwApoBH3VZuDI+q9VoWNlFn0cNBZo=; b=YFaK/cQ3QdcWhn/V+5VZk+BFOclI0QiFnr+7TIkxiF//QZDdlBcwKaQfeECnTjad6A gLxNem0+U8gSzdTRFBV6Vrn+XSNziLJ4w7W1sG3m9sKN3ejGO7nSaoYewNc11N/d92qC zG5svFDhkZEJHxqimK+rZWkGh7oU12tpADVl5gj11uIEKi22sLC3+zr2jkrBsBWQTDqw FQOkzLnDJmUdLwI2I6PICZl2Ql7m7IliXmjmrswY3kYfZKW1ET5e/IMA6lg2HDDNCC6v Idh2afziBTbxkmuhRE4x3e/+oHt3GEoRLk/iVOadF4VRuEc3DKa90o2bGwj0ZyR/xQVs lBeQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="t/OZmwy6"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::234 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=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=gnTekJ258YPkBVdwApoBH3VZuDI+q9VoWNlFn0cNBZo=; b=LUspJ3XHBXVRc30BNjWwX0vU61cW46Gh6lb/Zc9p4BOolCFd6hePOaKSEFwsPbgtnz Dk4r3dXq4+G9syv0pM1IF3PusLdacMszw7iJ2eHv/F4wtioZ6mzTK7LF23nM2uV3lxYv H+0Fh/zeGB9OPct58J+4IrOGRolw7CVEAB1B7EEcmdqlxbYmvtIODIX3b0yGWHrY6T2h rKpri8/5HNbSVXWT7EnuwagRKbhRqxt0W8i42fZDfwP2QRFReuGzPSVAcjSoaThGogY9 s4XdEuEO3bJaadNkr6DuFismMX6u/SYftpkf7GwhBcj9kpsuWEawqRARyc3ZLmzVsvFX B+Dw== 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=gnTekJ258YPkBVdwApoBH3VZuDI+q9VoWNlFn0cNBZo=; b=VTvfG7L/iSeK7X5YJn6EGmF4ADzUEzn7qVOVsIS1QIgi/bwjFntNzD77gsqFUAGSc3 VfYnAaEcwq0haN9+C3SzKCW9lSFb5VL9E4ZUCgWteh1sRzycNR8CWQ93aJIyfRPS0Mfq CoMAWp2DIC6xjw1sMzQp2kg4Ernd1vmjNBQqNPM93EGzPheL3OID96WetV8H+Toj2eYt JAcgwTolnxMVfUQGG/3j6Z+Y0cyBjwhLAyoOX6D+tCWy62VGJZxk5Fjhe7lm93o3+A7E VIA2VFflXpwUh0TRkmnhT6AQd1m3S0g0nqUDkI7ES0ee3/tXk/p6sbAVwRbCroJM3GcM aL7Q== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVCwrr3gLcZZX4Rt0yNxMDTVBhQjAP2lYl4Aci9V/53Z2G7n6e7 dW2FxrDYxlb9bHk96bgd+ME= X-Google-Smtp-Source: APXvYqzs6XVUiNxp4o3kPIoV1wrF1g21PX/GacmP8Vn2QNdd8PSHxRtCCbFuTnIcOR2V4OY1vGkPWg== X-Received: by 2002:a17:90a:23e5:: with SMTP id g92mr17618875pje.14.1582502197233; Sun, 23 Feb 2020 15:56:37 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:2a04:: with SMTP id q4ls2602355pgq.6.gmail; Sun, 23 Feb 2020 15:56:36 -0800 (PST) X-Received: by 2002:a63:505b:: with SMTP id q27mr50198174pgl.39.1582502196663; Sun, 23 Feb 2020 15:56:36 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1582502196; cv=none; d=google.com; s=arc-20160816; b=o+6MzlugN9RrCuQ7f7grysmS+4JQvoJjB+vhbayuHw53bqZPEhmHnuMdYHZrlvaSPl I22ursz/YG1r0gW+DW93pwUJtI0WjGnaJ5x1VJgRxzVOUUfUhtUlC8WxLRVj6jqZ75o3 zvXdbRFlIEqHT06Jac4RFwpJC6rW3BcgGRiL2XYlaar/8uDGQ9eGldKjsVlP4bOOYk/+ 0AO1imzuh8BtcGDpHL5MRSxozvR1nL5wDXDXVK7QVFTUrvaAX+M7J+3CulKVMeVKDQEM SBcbTpsVxJTKTXoXQg+3JBexvdpgw7nPXYolTbz6SACNn/B5k5GrgD9xIkUNtMIK/enj pE6Q== 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=BJV+Zw2BF/5eTck1dwfLGgHpdFv21PTS2kK7Fu4kvlE=; b=SA2Pd8sSH5jy8y4uQgYmod33ADDzhQsUergNulJiTGN1qzkY/4fQUAMVbzhU61R8cD T2WMPxoI4p3HILWGITBOgGjhHkxHjbGmY+MCnXezjKnzd8ub6BPcUOzYFTSXECQFOTva uAx6h5UiaJUlg8bn9dK7FCNtoyWpxiVrMXfml1XdImNP+4RNnIHe6y7Bb5wwIGc2tVOl NMmsloKS6VQVT2w+Bn+bYqlME6oqRixpAkIeMyyXRvMqhn49m0/PysJXPhz2wEeWqWyA n0vwL8LtRqHh+FNt6X2ZAOV8W73QvII6//Eu42nXlffZSuEs/QNqNcXhDjumB3wNqKaT Yxww== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b="t/OZmwy6"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::234 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-oi1-x234.google.com (mail-oi1-x234.google.com. [2607:f8b0:4864:20::234]) by gmr-mx.google.com with ESMTPS id t34si597427pjb.3.2020.02.23.15.56.36 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 23 Feb 2020 15:56:36 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::234 as permitted sender) client-ip=2607:f8b0:4864:20::234; Received: by mail-oi1-x234.google.com with SMTP id b18so7356736oie.2 for ; Sun, 23 Feb 2020 15:56:36 -0800 (PST) X-Received: by 2002:a05:6808:b22:: with SMTP id t2mr10536037oij.40.1582502195772; Sun, 23 Feb 2020 15:56:35 -0800 (PST) Received: from mail-ot1-f44.google.com (mail-ot1-f44.google.com. [209.85.210.44]) by smtp.gmail.com with ESMTPSA id l80sm3491395oib.37.2020.02.23.15.56.34 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 23 Feb 2020 15:56:35 -0800 (PST) Received: by mail-ot1-f44.google.com with SMTP id 59so7133960otp.12 for ; Sun, 23 Feb 2020 15:56:34 -0800 (PST) X-Received: by 2002:a9d:12a2:: with SMTP id g31mr39239327otg.283.1582502194562; Sun, 23 Feb 2020 15:56:34 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Sun, 23 Feb 2020 15:56:22 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Joyal's definition of elementary higher topos To: Bas Spitters Cc: homotopytypetheory 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="t/OZmwy6"; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::234 as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=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: , Actually let me modify that: (G3) holds in any type-theoretic model topos. And since coproducts are disjoint, (G2) is implied by (G1) and (G3); while since the initial object is strict, (G1) merely asserts that it is fibrant. So if the initial object is fibrant, then all of (G1-G3) hold. The initial object isn't always fibrant, but I wouldn't be surprised if every Grothendieck (=E2=88=9E,1)-topos could be presented b= y a model category of this sort in which the initial object is fibrant, at least in a classical metatheory, for the same reason that every Grothendieck 1-topos is overt classically: we can simply remove from the site all objects that are covered by the empty family. But I haven't checked the details in the =E2=88=9E-case. And I still don't know any way to make the NNO fibrant. On Fri, Feb 21, 2020 at 2:13 PM Michael Shulman wrot= e: > > I believe the best that's known is that (assuming an inaccessible > cardinal) any Grothendieck (=E2=88=9E,1)-topos can be presented by a mode= l > category -- namely, a left exact localization of an injective model > structure on simplicial presheaves -- satisfying all of Joyal's axioms > except those involving coproducts (G1-G3) and fibrancy of the NNO > (A2). Most of the properties are easy to show from the definitions; > G6 and G7 follow from the fact that it presents a Grothendieck > (=E2=88=9E,1)-topos; L2 follows from an adjoint pushout-product calculati= on; > and I showed L6 myself most recently in > https://arxiv.org/abs/1904.07004. > > The extra axioms (G1-G3) and (A2) hold in many examples -- e.g. the > injective model structure itself, which presents a presheaf > (=E2=88=9E,1)-topos, and probably also other examples such as sheaves on > locally connected sites. But in other cases even the initial object > may not be fibrant. Personally, my current opinion (subject to > change) is that (G1-G3) and (A2) are unreasonably strong, and > unnecessary for most purposes. > > > On Fri, Feb 21, 2020 at 5:23 AM Bas Spitters w= rote: > > > > In 2014, Andra Joyal proposed a definition of an elementary higher topo= s. > > > > "This lecture contains a proposed definition that is not an > > (=E2=88=9E,1)-category but a presentation of one by a model category-li= ke > > structure; this is closer to the type theory, but further from the > > intended examples. In particular, there are unresolved coherence > > questions even as to whether every Grothendieck (=E2=88=9E,1)-topos can= be > > presented by a model in Joyal=E2=80=99s sense (in particular, how stric= t can a > > universe be made, and can the natural numbers object be made > > fibrant)." > > https://ncatlab.org/nlab/show/elementary+%28infinity%2C1%29-topos > > > > Has there been any progress on these coherence questions? > > > > -- > > You received this message because you are subscribed to the Google Grou= ps "Homotopy Type Theory" group. > > To unsubscribe from this group and stop receiving emails from it, send = an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > > To view this discussion on the web visit https://groups.google.com/d/ms= gid/HomotopyTypeTheory/CAOoPQuQc317E8qUEOWJ2JQD_iXAFyE%3DWcttruqd5A8tRpHqtt= g%40mail.gmail.com. --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAOvivQwXyK0QMj-F0%2BCcEV1VjQoFTDh9P7P9630chx1V9Hpapg%40= mail.gmail.com.