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 autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-pj1-x103c.google.com (mail-pj1-x103c.google.com [2607:f8b0:4864:20::103c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8d8963d9 for ; Fri, 21 Feb 2020 22:13:40 +0000 (UTC) Received: by mail-pj1-x103c.google.com with SMTP id ev1sf1777742pjb.5 for ; Fri, 21 Feb 2020 14:13:40 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1582323219; cv=pass; d=google.com; s=arc-20160816; b=J2T4NJcSKhAV1PWtpWqtesne8ZQI0lfc9tn1KBjX8YjcBzgGlhHf8jgBcYXnTOWrG4 1PRVL5rpkbos0W/avusTl5ngJGgbP6nvl/Ra7t3srWEKYH3dHGvxdBwfhHn7u7WCCkS3 MxtcjA4E/7sOaGsb5tz8/F0MdAaWSf1G9avUR8k374sBiDTDG6eRDGLQ2w8jYRc7i7Ly 7T2fR/V8RmsB97CLddqC5tQCteiEMHyiG05CkXJixyEaSohu4SIKlPhMV+wThMQ70d2+ ZPQ5eB2BnxgBCdRc50AD4Bjyuxi1y7JychlPeqLZL5JRO5YyodMIBw5fZkr8dgkJFBjq RYrw== 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=wpL7FeThlAOMVl5Lxf6h9VBgKmEOikbRGCuP0lq0GCE=; b=lfvaqr2e2e8EHoLw7Uhv30DQ3SiQZZe4VQXaa65/5LycBHlGxmdeuOVIQQb66D/18r YMZP3OxogRztaHRLmyh3fwoSFadrRPYi380C+aPZOhb0gm9Mxa3VrFnjEpoNHRqcVCXQ bXwGtMlcvY/QC5S7DDSInDzk9HiwLch+hQGkdDY+yqazGGCiIMSNY2vmATraTtk9/2Te gjSYkEcQfIHZKhPt9AATg6d1j/u4uVnwhOkDBNRFMnVlRqniI+YUtmW47P2Tr0t7WXi7 jXOSvuPn3rU7jZ5DYHUu8cl5eJlEpgbWtTvAvYPZjfnCR75hBSHbtChPaQcq992tEW1y GHxg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=tyglMI3Z; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::32c 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=wpL7FeThlAOMVl5Lxf6h9VBgKmEOikbRGCuP0lq0GCE=; b=Q1MjCN42ZizZGyQzUjlcYO9GbK/LGGVJMiuMj870DAwgnl7tLrWEleTuAGf1gvpKYB z1uPTuGU+Gb0ABwHpQhE53HSa+17mEdKlviRIhgn48Js5Iz+8jPLRRi41bOh1bXjCwzm L8bQ3IyxbXAEBHN3NtQgHIvUmbkkPI1+1ZKmHVchK+q9R38ai2FSWpPJsG0m7otxn+LA V0jCH/nxOrl7RaEaJQGPlCYoOeBI2liqcRbMNGqn0qCpc79uTHdcuMc2lSnYdZPFAHxA QWpp6VnFFkPGvWkCvrE965XdMPma8xxLbieHJc25Ax4OiE5Ex1o9+cZMCH5DsiCP6UUx QYVA== 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=wpL7FeThlAOMVl5Lxf6h9VBgKmEOikbRGCuP0lq0GCE=; b=QJBRUnPl/c6WHLfTT+/YI8uV6EzGytZuNHsIEwAwj1LeLq2wBRKJey8CwdJQv/yRGc 2aZQVPWgcve7MdF+YmCLKPo5jxr9yUTRFX9wSOYUW2LmRZlNNT/l1hUIcRZsWbNdkJDv gefnKJ6oQkmhscIDwSSrHU1635Eg3VcSVeDlpjSxBD0eiNC9UTVd7hoD4WR/Ucb97ww8 Jzt4o0AdTGA2xaq//H97RarLxPV7pvfqXpWKtZ840WkIJb0KdiT7r9rHLqXjKzZtwci8 yttUoFMib59QUr4G4T9pnrwTpYYMGplg7j6ie4701TiWatWzaqJB0/NufBpTCIKWcZx6 1KvQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUrO9oo3QeeXbRCZ41G4crEXYIXBg0TXqnDphHbMsw7eV6i4dvt WcBLJ/8KNzAmknuR2PqiSxw= X-Google-Smtp-Source: APXvYqxz2jvkKCOai94WapsKdMROWLH2DJbjOnk3PFZbyhKBtjx90C5jBc6NykDpOwvWjaBHc3H+tg== X-Received: by 2002:a17:902:82c3:: with SMTP id u3mr36380454plz.73.1582323219175; Fri, 21 Feb 2020 14:13:39 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:902:bb88:: with SMTP id m8ls1233224pls.6.gmail; Fri, 21 Feb 2020 14:13:38 -0800 (PST) X-Received: by 2002:a17:902:8a85:: with SMTP id p5mr39736982plo.154.1582323218663; Fri, 21 Feb 2020 14:13:38 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1582323218; cv=none; d=google.com; s=arc-20160816; b=uUwD9f8I/mLe8exnL4yDpNmPKZLYWmY2hr7TNzbdHYScIhovF1+le9zzIUyJ3ZNS/p vzGpNNNaLCuw5HlgNrHfHlLC+omfHMrVnxhYhqGH3XNjT/njG7weC3K/DPaDIdrKdZKC 8EsLpnlW+eXx+eNdsoV8fi3WcVRrhjoeygFcNIN8YotbszaXYmk54KVjRz9IbPSl1tMB QxRgJxf6BLeWOjUzU1qd4zzZ7xlXywuG69RZsoEVqe/Jz69oVrQhGiH3D7ag3rBTzj4U 6IEPqdqkVtnDSDn9k/Dnl9MMTgWm8cg7v9nx3e4waBMGv95C8eopDFdSxtUbcYWpHCD9 qE8Q== 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=sHmGSrOfHW6C3x9+wqidE4WhINukapLqcrq0wBkqVW0=; b=U57N6Yb1LmJxGKvEc3SOPVeCb1sGORwOMomRPmD1xK1qYP6Pm8S6EApvN9Irr2hZLb gDl5WyHtCs1J8sc/0RMEhSzyAqX2YeEMD+JSZZaetcpZWMN77rFf1AGs0zbzNt1xebWC iOdn7HF4pX1M/j3nxHxG5kzNIhqIEQVi/GgWIVvoinTPZQKLFTyNxcKlIKX5oaEHjvXn Khb+l/u2MaxlTz0qznnfYXHIyqAxf+yr+pIqThLVj5Lq6IDgIxTCB84zzPTnCilXSCky Ppo9AVnLaMHZqpTiIKHbbK2lqmtFkOKDm4MenTztAySsU3B343DMuScnIC6sOqoajMmM fVUg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=tyglMI3Z; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::32c as permitted sender) smtp.mailfrom=shulman@sandiego.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=sandiego.edu Received: from mail-ot1-x32c.google.com (mail-ot1-x32c.google.com. [2607:f8b0:4864:20::32c]) by gmr-mx.google.com with ESMTPS id n20si223685pgl.1.2020.02.21.14.13.38 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 21 Feb 2020 14:13:38 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::32c as permitted sender) client-ip=2607:f8b0:4864:20::32c; Received: by mail-ot1-x32c.google.com with SMTP id w6so3489141otk.0 for ; Fri, 21 Feb 2020 14:13:38 -0800 (PST) X-Received: by 2002:a9d:dc1:: with SMTP id 59mr30229704ots.250.1582323217697; Fri, 21 Feb 2020 14:13:37 -0800 (PST) Received: from mail-oi1-f172.google.com (mail-oi1-f172.google.com. [209.85.167.172]) by smtp.gmail.com with ESMTPSA id z10sm1341530oih.1.2020.02.21.14.13.35 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Fri, 21 Feb 2020 14:13:36 -0800 (PST) Received: by mail-oi1-f172.google.com with SMTP id 18so191704oij.6 for ; Fri, 21 Feb 2020 14:13:35 -0800 (PST) X-Received: by 2002:a05:6808:312:: with SMTP id i18mr4041930oie.44.1582323215608; Fri, 21 Feb 2020 14:13:35 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Fri, 21 Feb 2020 14:13:24 -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=tyglMI3Z; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::32c 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: , 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 model 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 calculation= ; 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 wro= te: > > In 2014, Andra Joyal proposed a definition of an elementary higher topos. > > "This lecture contains a proposed definition that is not an > (=E2=88=9E,1)-category but a presentation of one by a model category-like > 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 b= e > presented by a model in Joyal=E2=80=99s sense (in particular, how strict = 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 Groups= "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/msgi= d/HomotopyTypeTheory/CAOoPQuQc317E8qUEOWJ2JQD_iXAFyE%3DWcttruqd5A8tRpHqttg%= 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/CAOvivQya7JthjksQC-XQ%2Bjuc3N_-O3JJibDjRM8F1hyML4CMAQ%40= mail.gmail.com.