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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-vk1-xa38.google.com (mail-vk1-xa38.google.com [IPv6:2607:f8b0:4864:20::a38]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 781a67fb for ; Tue, 8 Oct 2019 16:36:33 +0000 (UTC) Received: by mail-vk1-xa38.google.com with SMTP id q5sf8479001vkg.20 for ; Tue, 08 Oct 2019 09:36:32 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1570552592; cv=pass; d=google.com; s=arc-20160816; b=cQrrJEVAfWnXRL8stL2HLk5M/MbYnrFFYhnEK9XJG9A5z42/DzNsAsWfMzij5Ld4DF uKtanWpjp5Mse4o8w3QzCq/01Rh7x1wEi7eqgOqDYvgj4CIIJVQ15itLtXYCWZR3eD8I 2dOE9rZbQVGSL6V3pQcNsTOY1ELXDeYi7PGX+G9gCwg7R1MsHWW+PGu/xZbl+89GUZiI aFuMhvbar+WbUdjMa/DnFB32FEAiXwMpfvsSlXyyMJQvBz18xNDI8/CpM92DvqC71orR N7Ae/7zPDspJ/lPqR52uHVrteNRL2JnKBWoanUEk9mjxp1aXvmKQldO1a69DTgAA7Uiq z5rA== 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 :dkim-signature; bh=ftfcCWaAnWObs5Kl1eat92LtAjd6ojQxtWaqCvzgZuc=; b=wn8k/XYDednTB5ZzZgq4LKhQkhgE+UkIh8/StF0BvzEmhRGAmVOjtz7q9SBCGZA8cx 1X1hEBzrTsNzQeJzXmmu5hPAkkdowjFfsQksjH3Lw0ejNwSirfr668pcHvaGmzM0IX63 bYn3NGnd43hWBTQm4HY01bD3a9C/SKpLPrIvGYoC/Vi/JzkPPpPgZHqxuPui3YGo3hY9 K/xpj699n+S7S5tE79KrjMKeO3/+qGfbhjfB1GnjJQuoK1+tR7tozJDLj+P//3qyRefd tIBVb2Y4ltuaSi5zeCVEglfX8aFbTc9c1uO8vRewFwOhl+gI2AMVa1+7OsZUh0Etftrw Tr9w== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Wv86ha9s; spf=pass (google.com: domain of alizter@gmail.com designates 2607:f8b0:4864:20::430 as permitted sender) smtp.mailfrom=alizter@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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=ftfcCWaAnWObs5Kl1eat92LtAjd6ojQxtWaqCvzgZuc=; b=AuW7+5LETg3dcHa3ZXmI5PlIDqC8ivh0KDwFCMSEvrOeQ5dpaN8reY2wrPPWViiez4 rNJ5CIMgmK/vpp36xRjLV25On6koK1hhfXvk9VOOK3lyPmU+ZzcXVW7OjWQWtWsTm7uN Q3uRHpBgd5fWprh5Xv/0OGPidYsPbpSt5yjjOxIgYhPR0Oo2RydSH6HcsAWZ47a0SL9u i3QACP5L63GxXDv8al38NzAnLl1PALHiJ/iCaYFCnBrNC7QuRATZot3zkcR9WE2nDvQs uri5BVc+Cwp0jgRoDUU8Jk4v3yUryhQjAeSoGHGDeY+WvS5zjSl9ezrf9U1i/yTijtOG u81g== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=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=ftfcCWaAnWObs5Kl1eat92LtAjd6ojQxtWaqCvzgZuc=; b=HfuSVUrEgym7Vr2hh2da0v45SoS0SQ25bwCgdY6pVWLmadUXdmnYCU02eQ8P+fR2ex 4Xxx3EvTDKcixnDgXTVZCa3P1wv0mUB6crIMdp8EHqRIwnvM1Cj1h+xn6OjPrpNzPdwU xcWsaqeg0fnVspLUxhQadrn1jo8amt/RqqyG+p8ifevSKfcrCWW5DRrHmN6ItuIYlgDA ICjmi+p8TFwMADV2D5+rOeP+Z6aJ2x2TW140VLqoReGRMut8Y5cF6lwOBFwqY/4oRxAQ bg8Jx0XdBPkAifbwM2UAog/+OPDtDIPkOECo+OZrFPYmyKBiTCxIzIpJI0h+zxRXpcgz Rtlw== 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=ftfcCWaAnWObs5Kl1eat92LtAjd6ojQxtWaqCvzgZuc=; b=tUNqjgIPhdRAnB0XlzHjNX5y9mOj40UiJhrriy2f1vx+UaLpZI8savEtCtnZ5kkmWi e4EZb455LpPthx0k9V4moudFYRv/0NG76hTjY/NyW4hBcansYg3XMkR12F/MQ8BFJR3y Dv1OaKTfm9t0lbVREFs9Yry8aU9vMzfy/nmuX1/WC0/Olw8IPLkzZUHk5X/+2nLWWdOU uV/O3mA6SVYxE++Kv/tzPgia7Jy4RQ/6toDEQD91wELfdiMWdTeu5jhwYhhxvIoL6bO+ MwzQayjH4+9adeozm0cStoO3zdOElwS/uEyxhJ2vayG/mq5fOjlL7xSMTJMdsSay4azp W0UQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVHm4Tgd4VVkeypPGpgc4pR4muZscAF/g6e4GO/fbmjdHgQQOZ8 UmDbaMH58fYgU3W6QP+l4lA= X-Google-Smtp-Source: APXvYqyjTSpuoTpSA6hwp5n1yHzHDp/vTnq08zNnmR7BZzZSg8eiPPpOXYToJX/CCVjNAef1o3USVw== X-Received: by 2002:ab0:5eaa:: with SMTP id y42mr3320310uag.70.1570552592051; Tue, 08 Oct 2019 09:36:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a67:fc55:: with SMTP id p21ls390527vsq.9.gmail; Tue, 08 Oct 2019 09:36:31 -0700 (PDT) X-Received: by 2002:a67:6e45:: with SMTP id j66mr19120203vsc.177.1570552591123; Tue, 08 Oct 2019 09:36:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1570552591; cv=none; d=google.com; s=arc-20160816; b=ynjOojfP73vynyw6gq/FWmYThvDs6/BUlYPTbjYYf8Zy736UkMZz8mAaZ1JW597X9R 8ALuurZ4yPTCyNjabo/ko7BfCAITmNE3d7KNxzxiGkjdMO6gCPI8TYKoZ5ywWfbAJNr5 drSCWipHaDbRrT4CHf5sAHxlZjCAKtZsC7+0tvhO9w96S/8MQwUqNCAD9kj4t7Ssa81P 6bi3svKIwTnQIoRs+IeAx55+y1+2mR95/kNtNtqncWB/10dQCQkqLu4N3ZKzp3BHIQSA SPhtVGBf+doTn4THPtcSXPYFkVO4tnXmKnB+oJJWHNLIiKNwIZebktnKXxvNmfEeiXUA +GBg== 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=LOBU25RJZnMtp0mCQrDm69foYYH0ClCwGd8U725s6C0=; b=ZyDGZSFi+bkcVACIdxI24DqgLR9CIJSn33utz8/b+O1RTQ5r6m8qzvR+atqyy5ZqtQ MDCMd4YmWWIxbx2Mh/xy0WVlr6SIHeh0kJj00CPjgktBLICb23rioHaeawAEXgKYJgsV A6uO+KD5aM6DhZUMUly8kUkNfYcOhCfaPludem1dliKVlany56U5g9fbu233pK0qxaMt 0xjshNKWlvPCEDTRpMwDFBXxHBPIMhlOzWoY4UIM/F6wDP7o3lW7JxKTtpzBRa3k7L2j hXr2oTBA/htuyVQiw8hX3vyoEmXZUbr0xn3WfJTinXt/4nkd/B1ktctNE/p2jawSOAEv wTyA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Wv86ha9s; spf=pass (google.com: domain of alizter@gmail.com designates 2607:f8b0:4864:20::430 as permitted sender) smtp.mailfrom=alizter@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-pf1-x430.google.com (mail-pf1-x430.google.com. [2607:f8b0:4864:20::430]) by gmr-mx.google.com with ESMTPS id v4si83648vka.3.2019.10.08.09.36.31 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 08 Oct 2019 09:36:31 -0700 (PDT) Received-SPF: pass (google.com: domain of alizter@gmail.com designates 2607:f8b0:4864:20::430 as permitted sender) client-ip=2607:f8b0:4864:20::430; Received: by mail-pf1-x430.google.com with SMTP id q7so11062068pfh.8 for ; Tue, 08 Oct 2019 09:36:31 -0700 (PDT) X-Received: by 2002:a17:90a:e987:: with SMTP id v7mr6924946pjy.86.1570552589899; Tue, 08 Oct 2019 09:36:29 -0700 (PDT) MIME-Version: 1.0 References: <1b613bab-505c-4880-9778-4e3206872294@googlegroups.com> In-Reply-To: <1b613bab-505c-4880-9778-4e3206872294@googlegroups.com> From: Ali Caglayan Date: Tue, 8 Oct 2019 17:36:23 +0100 Message-ID: Subject: Re: [HoTT] Kripke-Joyal Semantics and HoTT To: Alexander Gietelink Oldenziel Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000038da2f059468c5ff" X-Original-Sender: alizter@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=Wv86ha9s; spf=pass (google.com: domain of alizter@gmail.com designates 2607:f8b0:4864:20::430 as permitted sender) smtp.mailfrom=alizter@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --00000000000038da2f059468c5ff Content-Type: text/plain; charset="UTF-8" Hi Alexander, I think what you are asking is "what is the internal language of an oo-topos". 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 once 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 direction with Mike Shulman's work . The Kripke-Joyal semantics of a topos of sheaves is essentially a dictionary between the "internal language" of this 1-topos and what it means externally. 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 care 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 consider. The thing to note with Mike's work is theorem 11.1, which shows that every 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 internal 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 formally 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 that 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 people using Kripke-Joyal semantics to actually do algebraic geometry. It's true that Ingo discovered some new arguments (generic freeness) but these have yet to catch on with "regular" algebraic geometers. This is because even though it is a 200 page thesis, it only covers foundational aspects of the subject, i.e. the basics of scheme theory. There is much more work to be done 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 examples of these almost being done. These are just my thoughts on your question and is no means the word of an expert. Best, Ali Caglayan On Tue, Oct 8, 2019 at 4:07 PM Alexander Gietelink Oldenziel < a.f.d.a.gietelinkoldenziel@gmail.com> wrote: > Dear all, > > It is my understanding that the interpretation of HoTT inside higher topoi > is an ongoing field of research. Much of this business involves subtle > strictness properties and things like contextual and syntactic categories. > In the 1-topos case there is the Kripke-Joyal/Stack - semantics. These > semantics 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 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/msgid/HomotopyTypeTheory/1b613bab-505c-4880-9778-4e3206872294%40googlegroups.com > > . > -- 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/msgid/HomotopyTypeTheory/CAB17i%3DjTaw4CD3Lha4fkKFgcYLpypzzDa0J8pPT1eYnZV1qUaQ%40mail.gmail.com. --00000000000038da2f059468c5ff Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Alexander,

I think what y= ou are asking is "what is the internal language of an oo-topos". = This is doesn't really make much sense as stated since we don't hav= e a definition for "internal language" in an oo-topos. But we exp= ect that once we can define such a notion, then it ought to be HoTT. This w= ill require further work, but recently there have been some big strides tow= ards this direction with Mike = Shulman's work.

The Kripke-Joyal semantics= of a topos of sheaves is essentially a dictionary between the "intern= al language" of this 1-topos and what it means externally. I have quot= ation marks here because I am not being very precise and phrases like "= ;internal language" do have precise meanings which I don't care to= look up right now.

You are correct that these hav= e been used in practice. Just look at Ingo Blechschmidt's work. He dis= cusses on pg. 199 briefly the thing that you consider.

=
The thing to note with Mike's work is theorem 11.1, which shows th= at every oo-topos can be presented by a "type-theoretic model topos&qu= ot;. Now you can think of Kripke-Joyal semantics as a "machine" t= hat can translate between internal and external statements. Here is a pa= ge 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" o= f a HoTT proof of Blakers-Massey into higher topos theory. The key point he= re 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 formally written down these semantics that I kn= ow of. Kripke-Joyal semantics are fairly technical already, just look at In= go's thesis. And you are correct that with HoTT there are lot's of = subtleties involved.

So to answer you final qu= estion: yes it is being investigated and yes it seems to be fruitful.
=

I will add however that apart from Ingo's work, I d= on't know of many people using Kripke-Joyal semantics to actually do al= gebraic geometry. It's true that Ingo discovered some new arguments (ge= neric freeness) but these have yet to catch on with "regular" alg= ebraic geometers. This is because even though it is a 200 page thesis, it o= nly covers foundational aspects of the subject, i.e. the basics of scheme t= heory. There is much more work to be done before it gets mainstream.

We will probably see algebraic topologists using the= internal language of (oo-)toposes well before algebraic geometers do. Sinc= e we already have examples of these almost being done.

=
These are just my thoughts on your question and is no means the word o= f an expert.

Best,
Ali Caglayan<= br>


On Tue, Oct 8, 2019 at 4:07 PM Alexander Gietelink= Oldenziel <a.f.= d.a.gietelinkoldenziel@gmail.com> wrote:
Dear all,

<= div>It is my understanding that the interpretation of HoTT inside higher to= poi is an ongoing field of research. Much of this business involves subtle = strictness properties and things like contextual and syntactic categories.= =C2=A0
In the 1-topos case there is the Kripke-Joyal/Stack - sema= ntics. These semantics are easy to use in practice.=C2=A0 Naively, it seems= one could lift the Kripke-Joyal semantics by not asking for truth but simp= ly an inhabitant of a type.=C2=A0

Has this been in= vestigated at all? Is it ultimately fruitless?

--
You received this message because you are subscribed to the Google Groups &= quot;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 ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/1b613bab-505c-4880-9778-= 4e3206872294%40googlegroups.com.

--
You received this message because you are subscribed to the Google Groups &= quot;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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DjTaw4CD3Lha4fkKFgcYLpy= pzzDa0J8pPT1eYnZV1qUaQ%40mail.gmail.com.
--00000000000038da2f059468c5ff--