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-qt1-x83c.google.com (mail-qt1-x83c.google.com [IPv6:2607:f8b0:4864:20::83c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a186186a for ; Thu, 10 Oct 2019 21:20:28 +0000 (UTC) Received: by mail-qt1-x83c.google.com with SMTP id h20sf7150414qto.7 for ; Thu, 10 Oct 2019 14:20:27 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1570742426; cv=pass; d=google.com; s=arc-20160816; b=ZwyOUJ07yRmRayjAuzzKbHbgumrsotONN5nE2UVfuzHihpGyOJkIMSOEN0qaOu4zBg bR1GHuWK9HUkyzUeDWs7MTwMcVJbngmEalLibQymWudUzUMxsxj8NLYJ1esfC82ljcv8 71eC4g3QPhE4OkHAVpARuRNc+tYJH3jTUbxoUfqtjYdjBtQ8C0M1/DB/q0U+D4e6uPV3 s31qjZDLGDe+Y/qrA7Zok6YfVPZ6L2qAHrhS9if7Tg/Y2HAvfdiV+tuIJf2G+PMGHrTH S3+gvNWrUQE4Bsy5NUQI3yFF/1pBMF/qMnLpoUuPZ4eWrQTB/D9z1Y6VgECfW/FEVv5j xDZQ== 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:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=JUXmaIvUJcH8v31mxMb36Fn7Cfa5er8nZ80KIHoIv7I=; b=0f2oEGn5bNvcg5kWCFaefMWKbC7+7eJNjN6bb9zBjFDroOqPdUDVKID5Liv+IkQpFL t/q/MX0h0Yz1OvNUs0FxxEesUccEOoUd4W79hwWwl8MQg5tM/3i6Zx/oq4Xm3clYCdes FvWY2eDeymRsu/g6i3h+rGfEqs0EA8WoIxNjC3M5mXq4R9ma1Gd1DNlbPd4O0WGK73I7 Fbrc0HKOphWaVruccSQDNH7K/v5CBMNDbDnRPL/OB424hxEi3xJ6Ai6etbd3ONacL0fi hKWsLSGD7o6FpODwA+5g9fE7qCc83e0AxXj9ZLzHgM3RHhakGwvZbNCzkruPHY9OIPG4 smow== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=j3LPAlyP; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b30 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=JUXmaIvUJcH8v31mxMb36Fn7Cfa5er8nZ80KIHoIv7I=; b=QOnt2+HyCp2bJNeu4u8rKlxHdDQ1O6ALZCro3IJ/AxfNL/c4h4cMtFZwjT1F4XDcdI yBrwLZXiQYKY6TM0ibgHJPg9PCQl+nptHDHg1+BcbiQNsqwuQYH+PP6HgQth4s4K0fPg HFTGFX6NC5dKKiFqdnMegqnp26Bgc4ymnbBsYI3PF44bfihXJDMAT084TvLvhvtBMeB0 vB5wJ4BtLUX7NHbUKwz2BqLEEpSHfeJRJ8hjkjAwvwnIDqLtn/TngGHnlhcFTTq9zL3H IcSyoCC6myztFazSKNf+VlIqLC+UknYASAJwMJhIGT/x+Os9lfwSDWAcEAljRzJsYzND sl7A== 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: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=JUXmaIvUJcH8v31mxMb36Fn7Cfa5er8nZ80KIHoIv7I=; b=CUgxa+jKA6KWU+xZed9MiKbWz3tpkxz5qgi0Zps9j1p1okR9Y/v6ZmZHFGmLWE+iAv Lw4ZmKdfBBnc2Val7AeBpJPLFp2lfJpcwU7BaOy8qvRWFfsVj47sEN3RkXLondYyQlye 22llhQrrKgopFXUEN5vyulRcw65F228vQLJN4aLrCLbXsvis3nXfI7pftBvtgLLldFKA ZnyoPwh2akySuBpwtDwfdnnXWahk+aF/8R2WTYUod4hd6bFW0PNlDo8LneH6S3qore8v zyMq7X3NooEr09rQBO00JJBadEKuGwFedWd10240qnuLYK7l4FKdhHhs5Ci5kyk98ga1 BnKg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVWncqFP2wRbvNf0+Gn4dPKBrWv0YnuphMqE1eM3PFlHLKQRe/R udt+XSjna/kj2CUrZS47zN4= X-Google-Smtp-Source: APXvYqw07VtanP21rsKTUeAIhQ3qb8cynAEBwBkR/D3lUx9g1brySlRo2NH+R7yl5HcrHVeWn/oMrw== X-Received: by 2002:ae9:c302:: with SMTP id n2mr11686913qkg.69.1570742425910; Thu, 10 Oct 2019 14:20:25 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:620a:131b:: with SMTP id o27ls882137qkj.12.gmail; Thu, 10 Oct 2019 14:20:25 -0700 (PDT) X-Received: by 2002:a37:628d:: with SMTP id w135mr12080701qkb.6.1570742425394; Thu, 10 Oct 2019 14:20:25 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1570742425; cv=none; d=google.com; s=arc-20160816; b=HmEkhhJ+/bzWTx+EeMXabXcOjlmPynsdwfh3e2phqaLdWMnpxfURQSoX8BcQl99Fnn 0bEoBUNA4uNL2r5O8b/x+GUxj9Fjv48kZIzy0BPJGTmdHmHYZVfR5w3v3pdGJFHULeU6 jJ6FNTyTzxX1Z5T0kU1bRqUnTc9x9o5CrVPaUMqWS42gU5F52As6L/3AUt9CMkOUyPjE NmhEONgRsrRzUMza49N4TfEns7U9dlCQDbc88sSWyClQRC8hEUmwBWaaxuYkTeDKKtGB rHTIWEWn66ht92n3xTBkfXX2BhT98ikHVJ4rRQ2Nxrbaca4D1AcgJbqauAfVovs0LIDb q6Ew== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=QZfaMTM4bwKn7WU/7FYJG7QpMvaRbIeLSCYjltwGw48=; b=qOuZmiWuTsMRpHAEpFtZc+cPDl9758tCjoQXX930aRwkxhX/LwSV/iiOkD75niBqtQ xyISt576Ns4RT2UdZlgOltqA/8nKfmYHAkNquEqZNfm2EtMadc/xpgYvIijr0oadm9sZ KigNytik1K9+Yy1HIwL2HFWdap2z98d1c3MOdC99MySeZcbCNr5v+ZdanwV1nB6aWGps nGsAdJ/IuEjUjJMqh7UqnrVI8KpU/JLNT3zJgAbyQV/vlvvT7fQuPnNIWKffg7jtlDre PwYs5Bugn0I7Wci7zQq04Opjo8TeUNbE77D6Jfi/DS78c+rr+w0pHUvXSWrl+JtioczM T8xw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=j3LPAlyP; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b30 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb30.google.com (mail-yb1-xb30.google.com. [2607:f8b0:4864:20::b30]) by gmr-mx.google.com with ESMTPS id w41si697706qtb.4.2019.10.10.14.20.25 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 10 Oct 2019 14:20:25 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b30 as permitted sender) client-ip=2607:f8b0:4864:20::b30; Received: by mail-yb1-xb30.google.com with SMTP id r68so2428316ybf.5 for ; Thu, 10 Oct 2019 14:20:25 -0700 (PDT) X-Received: by 2002:a25:2784:: with SMTP id n126mr7785226ybn.279.1570742424777; Thu, 10 Oct 2019 14:20:24 -0700 (PDT) Received: from mail-yw1-f50.google.com (mail-yw1-f50.google.com. [209.85.161.50]) by smtp.gmail.com with ESMTPSA id v40sm1608407ywh.109.2019.10.10.14.20.23 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 10 Oct 2019 14:20:23 -0700 (PDT) Received: by mail-yw1-f50.google.com with SMTP id i207so2701202ywc.9 for ; Thu, 10 Oct 2019 14:20:23 -0700 (PDT) X-Received: by 2002:a0d:d714:: with SMTP id z20mr8559462ywd.246.1570742423537; Thu, 10 Oct 2019 14:20:23 -0700 (PDT) MIME-Version: 1.0 References: <1b613bab-505c-4880-9778-4e3206872294@googlegroups.com> In-Reply-To: From: Michael Shulman Date: Thu, 10 Oct 2019 14:20:12 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Kripke-Joyal Semantics and HoTT To: 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=j3LPAlyP; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b30 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: , In the 1-category case, Kripke-Joyal is a specific formulation of the internal language of a 1-topos (or more general 1-category), involving a forcing relation relating objects of the topos to formulas in its internal logic. The existing work on internal languages for higher categories, including all of the links provided by Ali, is not actually Kripke-Joyal style but is a categorification of a different approach to internal languages that directly constructs objects corresponding to each formula, the connection being that the forcing relation is a representable functor and the interpretation objects are what represent it. I understood the question to be whether, in contrast to all of this existing work, there is also a Kripke-Joyal-style approach to internal languages of higher categories. I expect that probably there is, but I don't think such a thing has been written down yet, although I hear that Awodey and Gambino have been thinking about it. But my instinct is that a Kripke-Joyal approach wouldn't make the coherence questions any easier, since it's basically just a translation through the Yoneda lemma; any coherence technique that can be used for one version should also work for the other. On Tue, Oct 8, 2019 at 9:36 AM Ali Caglayan wrote: > > Hi Alexander, > > I think what you are asking is "what is the internal language of an oo-to= pos". This is doesn't really make much sense as stated since we don't have = a definition for "internal language" in an oo-topos. But we expect that onc= e we can define such a notion, then it ought to be HoTT. This will require = further work, but recently there have been some big strides towards this di= rection with Mike Shulman's work. > > The Kripke-Joyal semantics of a topos of sheaves is essentially a diction= ary between the "internal language" of this 1-topos and what it means exter= nally. I have quotation marks here because I am not being very precise and = phrases like "internal language" do have precise meanings which I don't car= e to look up right now. > > You are correct that these have been used in practice. Just look at Ingo = Blechschmidt's work. He discusses on pg. 199 briefly the thing that you con= sider. > > The thing to note with Mike's work is theorem 11.1, which shows that ever= y oo-topos can be presented by a "type-theoretic model topos". Now you can = think of Kripke-Joyal semantics as a "machine" that can translate between i= nternal and external statements. Here is a page on the nlab that shows what= this will probably end up looking like. > > To get an idea what such a machine might do, have a look at Charles Rezk'= s "translation" of a HoTT proof of Blakers-Massey into higher topos theory.= The key point here is that this proof was not known in higher topos theory= before. It is a very natural argument in HoTT however. I would say this is= pretty fruitful. > > The reason I keep saying "probably" is because nobody has actually formal= ly written down these semantics that I know of. Kripke-Joyal semantics are = fairly technical already, just look at Ingo's thesis. And you are correct t= hat with HoTT there are lot's of subtleties involved. > > So to answer you final question: yes it is being investigated and yes it = seems to be fruitful. > > I will add however that apart from Ingo's work, I don't know of many peop= le using Kripke-Joyal semantics to actually do algebraic geometry. It's tru= e that Ingo discovered some new arguments (generic freeness) but these have= yet to catch on with "regular" algebraic geometers. This is because even t= hough it is a 200 page thesis, it only covers foundational aspects of the s= ubject, i.e. the basics of scheme theory. There is much more work to be don= e before it gets mainstream. > > We will probably see algebraic topologists using the internal language of= (oo-)toposes well before algebraic geometers do. Since we already have exa= mples of these almost being done. > > These are just my thoughts on your question and is no means the word of a= n expert. > > Best, > Ali Caglayan > > > On Tue, Oct 8, 2019 at 4:07 PM Alexander Gietelink Oldenziel wrote: >> >> Dear all, >> >> It is my understanding that the interpretation of HoTT inside higher top= oi is an ongoing field of research. Much of this business involves subtle s= trictness properties and things like contextual and syntactic categories. >> In the 1-topos case there is the Kripke-Joyal/Stack - semantics. These s= emantics are easy to use in practice. Naively, it seems one could lift the= Kripke-Joyal semantics by not asking for truth but simply an inhabitant of= a type. >> >> Has this been investigated at all? Is it ultimately fruitless? >> >> -- >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit https://groups.google.com/d/msg= id/HomotopyTypeTheory/1b613bab-505c-4880-9778-4e3206872294%40googlegroups.c= om. > > -- > 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/CAB17i%3DjTaw4CD3Lha4fkKFgcYLpypzzDa0J8pPT1eYnZV1qUaQ%= 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/CAOvivQzEpWEtHZvNKPJxBnYPBxh2XhKB4jobVT0BZmn%3DvP42QQ%40= mail.gmail.com.