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=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-xa37.google.com (mail-vk1-xa37.google.com [IPv6:2607:f8b0:4864:20::a37]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8671d38f for ; Sat, 9 Feb 2019 08:17:21 +0000 (UTC) Received: by mail-vk1-xa37.google.com with SMTP id x202sf2297484vke.19 for ; Sat, 09 Feb 2019 00:17:21 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549700240; cv=pass; d=google.com; s=arc-20160816; b=RBrLkkDg2GQ6JHyQHDVnS7m0QMalnIrQsYpPvXGerHa1r2yEJ9Cwa9Qjxb7xqOlBDm 0836jbnqRoFWrOuLg9SkRlM87cZtpsJ/HZSmVGALxPVTwIBFcjoL2GAFZ7VqIO8N3hmc nrtxrW9yJb7izHclSFS5HRXR8w1j53UZaUxDKhLJt00lRQfPwzBtv9dL6TrfDtULTwLU 7Ln4rBHiRvs/Nb2//5xUXDYRis6c0/8wuj7OG+ybpjXvVN335J1g6XMWn9CZeooSN7Op 6zL8PXH30FGxHt8QXW2p5Ioi56YSfSRJiBhVJ6GjgpPFm/JCcVP5c1y1Qg8YWC65DLIV cCaQ== 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=zA/8wXoO/p0MqKFPcTGlrPEQ7PEAvgHg7+sb0B/+6HI=; b=JQEYIO+AQR62Ti5/VNXq9+L0QGEK/5Dn/R+c+/y3VmqNBlDNxqiuSiU5U4SaWEqsTl gejdfCFkofabKNpTA1W08SlFKwItm7bwIF6hMtRuHFBhHaDDwXZQzTTXumMtVLiFTPQS eLqDdKORAy645AjyrcCHUYu2/WrJusxlWbW0Toq6POtE4Ughb44syea7TJ5Ijf6tX9Gx dTiUBXQJUpo1GNvhx5qP3jdRehMGmqOaJPX/7sJu/4yoIOdQmCURcxsl44qJ8VswVt0b z6jDGbA30qLnwtqUE/PIlONhaCW6b2WNsBeMoyvPAjoH4a+Cu0/56096RF+X/UDSjVBc iM/A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=QLeX5yfr; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::12b as permitted sender) smtp.mailfrom=valery.isaev@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=zA/8wXoO/p0MqKFPcTGlrPEQ7PEAvgHg7+sb0B/+6HI=; b=Ye6yszkD8zkM9WzgJAWqpgjvQJvy5yTTPrFkJLU8QaDnKurz6OPE6QfrQYLOygXmnt OfqrsyhWUfnpq6k9yjEMxvW3lSWf2u1L2eN83iugIk/7mLKEVvezjmu9R6OcjN5TUOmU jWazAG34//ofj6mC97NHjw9SawhsschuYKLNC/VORcr0Uh1rijZcWpaintVQ/j898a7l jgdjdff1pOV9+uoz/193RMRlCg5/mybiVgCVw9QZ6e0n6MqZtvrZHniLVKfnuRh8NOax naGCOXywpljB5XpPiugyPOjm/AXXFQcxTzzAP+7eE/xHy2bxmQMnRcHFErHaLUuRQqqm fnow== 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=zA/8wXoO/p0MqKFPcTGlrPEQ7PEAvgHg7+sb0B/+6HI=; b=PTuOOxfEN0ogJdFYgc3AA9sNuD0RXZyvUdScwEWpXtOMqv8i4FrbJcbidX8ws22GpI iDjEgLc0aohpQvYNAjYFh/jQWI1MheoR/JtDBDXEavXEhLX3BJzQMnkJ1Wjy2et64yqn myUAi7iS1lq86JABUUWDQ/JOJGwXF7cByh7vpa/qdtshmqVDSLMmgxo+MLDfg5Rul8Ba 1ESWFwuGA6ZJFxiAdWr8O4nHMCmFUljpgyxAXEMqOQYLulzA071jXrSoewKwjUNZvNyD 18XXWQVtAwSNWvbONj381dz+A+vQEg1c+H9Fj1NnhZLtozNBP2s15queJr9b1GK4pOmk hj0w== 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=zA/8wXoO/p0MqKFPcTGlrPEQ7PEAvgHg7+sb0B/+6HI=; b=aK+U9J2H2prLRaEliuSG5J5g6Z3gA6PEK42YlmcQsTr2K5aUpl+gAyxMSpAIhStPBc XxtuAYIuE4n0qsyKh57xUVHRPnd31Q/ITnHJCkXBRne5iYGwsQ1o4ksu+ULkBj44uh69 gXQQ09hNz4xaRjEb7kJqyC5/FoZQGkGhnON8J1zxJOAN949N1FjIxvNwC++jt6Y3N4YK ABF8NFc/Cauqf2YWyXbkGMXZnXS+ih9whx4pR2dGnY3U+LW2K1Y9nlQvXmomidxE9xxt GCeWh+lgFzMkUrjLNv3wxYjf60wFvCYbKxGLh5/3pDR1y8i3Tw+Qf9WHVQQMFS8WdoKN VkdA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZ9DfZAtcz1/HQEnnPWaBz1WiD3uZBdVM8FoZwrb1mpkhrt1SGT sMq0XnvWAC3GIBIgK2pSOdw= X-Google-Smtp-Source: AHgI3IZ2y7pFFPRAgdLa4ms/rN9l8lrle1UAFo4bo8RBEo2wPf/wnZtP5+Ss0VmXUoMtRAeferV4+w== X-Received: by 2002:a1f:a504:: with SMTP id o4mr76336vke.0.1549700240145; Sat, 09 Feb 2019 00:17:20 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:9d0f:: with SMTP id g15ls1392991vke.1.gmail; Sat, 09 Feb 2019 00:17:19 -0800 (PST) X-Received: by 2002:a1f:1a46:: with SMTP id a67mr15173223vka.26.1549700239634; Sat, 09 Feb 2019 00:17:19 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549700239; cv=none; d=google.com; s=arc-20160816; b=TinIs9pAddXS8b7EN68JxeaYmqNkspyPd1fstm+cjK87Yr5bLtJjEyJU0h7ZtQblS5 WQjOO61bszwstcRfm/qf6aKw8YnrN52PEk48jtgDKPMEQoQhW6IeNjyFsVMF832uq/Vs jQMTr+nLXkvKBS3f3e35ytyAEw6oNBQpsUjD+mKHfaf/t1B7QabTsrv4MnT1cVhuVJpC UCE7a/oEQs/CfpYraRUxOcflidTY8pnl27yPXy5VFVwwKa1mhRMigN/eY9LEfU53duN9 M/p3QExxNQGGCiz0+wEa8duneWYRjRe/XUU8wE4FewMEluRZ70XMhAGMRwcXtySRonI1 hDCQ== 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=VnKSnML9UGnQDd1CQ3SlTvAb2PAnftoqyaDaIMLLtpw=; b=jKUPTh7UekUVCJl2cPceMrETbVVzOpN8RsYR9AUNhK5y2TsnWt8WggNzfINVDnCIYL 9VUbfRQiSNDHnAROe0Z5gt6IAhTlw7xcoqJrnp0jFLiAYmnJradCq5r6hopbH00hJ60J YM7bj9p+TiN42hG+ag1pxEWVaguaKhvPTBRcLruUi376rWS3Ky7p0Cji7FXJq+0pqP9a TyDFXM1RKegNcpBMQUqrNwzVdk1HXxC5VJJYxyy+vzecuicDNU8w3qNI2JkXvlQaAhnt r0ejL/pQ4PsOk1UjsIzCWnHqsXI4ivL+GELojC3mBxMhLhTaba7g2AqbD2tTki/S8R+A jzeQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=QLeX5yfr; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::12b as permitted sender) smtp.mailfrom=valery.isaev@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it1-x12b.google.com (mail-it1-x12b.google.com. [2607:f8b0:4864:20::12b]) by gmr-mx.google.com with ESMTPS id j26si184020uag.1.2019.02.09.00.17.19 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 09 Feb 2019 00:17:19 -0800 (PST) Received-SPF: pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::12b as permitted sender) client-ip=2607:f8b0:4864:20::12b; Received: by mail-it1-x12b.google.com with SMTP id r11so9436857itc.2 for ; Sat, 09 Feb 2019 00:17:19 -0800 (PST) X-Received: by 2002:a02:187:: with SMTP id 7mr78693jak.115.1549700239206; Sat, 09 Feb 2019 00:17:19 -0800 (PST) MIME-Version: 1.0 References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> <431cad6d-062a-4ed8-8c01-c6caf884ffa8@www.fastmail.com> In-Reply-To: <431cad6d-062a-4ed8-8c01-c6caf884ffa8@www.fastmail.com> From: Valery Isaev Date: Sat, 9 Feb 2019 11:16:43 +0300 Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: Jon Sterling Cc: "'Martin Escardo' via Homotopy Type Theory" Content-Type: multipart/alternative; boundary="000000000000443148058171b466" X-Original-Sender: valery.isaev@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=QLeX5yfr; spf=pass (google.com: domain of valery.isaev@gmail.com designates 2607:f8b0:4864:20::12b as permitted sender) smtp.mailfrom=valery.isaev@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: , --000000000000443148058171b466 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Jon, It is not true that Q(T) can be obtained from T simply by replacing judgmental equalities with propositional ones (I think this should be true for some theories, but certainly not for all). So, if we denote the theory with an interval and judgmental rules by T_I and the theory with propsoitional axioms by T_a, then Q(T_I) is equivalent to T_I and Q(T_a) is equivalent to T_a, but Q(T_I) is not equivalent to T_a. Theories T_a and Q(T_a) are actually equivalent to the ordinary MLTT (since we simply add another contractible type to it). Functional extensionality is provable in both T_I and Q(T_I). It follows from the existence of the interval type in T_I and it can be added as an axiom to Q(T_I). I believe that theories T_I and Q(T_I) are equivalent to MLTT + functional extensionality, but I don't know how to prove this yet. Regards, Valery Isaev =D1=81=D0=B1, 9 =D1=84=D0=B5=D0=B2=D1=80. 2019 =D0=B3. =D0=B2 05:01, Jon St= erling : > Hi Valery, > > I'm trying to square what you said with what Anders said. Consider > extending MLTT with an interval in two different ways: > > 1. With judgmental computation rules for the recursor > 2. With propositional computation axioms for the recursor > > I do not expect to obtain a conservativity result for the second version > over the first version, since the first one derives function > extensionality, and the second one does not (afaict). > > Can you give a bit more detail about how this algebraic power move that > you are describing works, and whether it applies in this case? > > Thanks! > Jon > > On Fri, Feb 8, 2019, at 6:32 PM, Valery Isaev wrote: > > If you are not interested in computations and convenience of your type > > theory, then the definitional equality is not essential in the sense > > that every type theory T is equivalent to a type theory Q(T) with no > > computational rules. Now, what do I mean when I say that type theories > > T and Q(T) are equivalent? I won't give here the formal definition, but > > the idea is that Q(T) can be interpreted in T and, for every type A of > > T, there is a type in Q(T) equivalent to A in T and the same is true > > for terms. This implies that every statement (i.e., type) of Q(T) is > > provable in Q(T) if and only if it is provable in T and every statement > > of T has an equivalent statement in Q(T), so the theories are > > "logically equivalent". Moreover, equivalent theories have equivalent > > (in an appropriate homotopical sense) categories of models. > > > > Regards, > > Valery Isaev > > > > > > =D1=81=D0=B1, 9 =D1=84=D0=B5=D0=B2=D1=80. 2019 =D0=B3. =D0=B2 00:19, Ma= rt=C3=ADn H=C3=B6tzel Escard=C3=B3 < > escardo.martin@gmail.com>: > > > I would also like to know an answer to this question. It is true that > dependent type theories have been designed using definitional equality. > > > > > > But why would anybody say that there is a *need* for that? Is it > impossible to define a sensible dependent type theory (say for the purpos= e > of serving as a foundation for univalent mathematics) that doesn't mentio= n > anything like definitional equality? If not, why not? And notice that I a= m > not talking about *usability* of a proof assistant such as the *existing* > ones (say Coq, Agda, Lean) were definitional equalities to be removed. I > don't care if such hypothetical proof assistants would be impossibly > difficult to use for a dependent type theory lacking definitional > equalities (if such a thing exists). > > > > > > The question asked by Felix is a very sensible one: why is it claimed > that definitional equalities are essential to dependent type theories? > > > > > > (I do understand that they are used to compute, and so if you are > interested in constructive mathematics (like I am) then they are useful. > But, again, in principle we can think of a dependent type theory with no > definitional equalities and instead an existence property like e.g. in > Lambek and Scott's "introduction to higher-order categorical logic". And > like was discussed in a relatively recent message by Thierry Coquand in > this list,) > > > > > > Martin > > > > > > > > > On Wednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote: > > >> In section 1.1 of the HoTT book it says "In type theory there is als= o > a need for an equality judgment." Currently it seems to me like one could= , > in principle, replace substitution along judgmental equality with explici= t > transports if one added a few sensible rules to the type theory. Is there= a > fundamental reason why the equality judgment is still necessary? > > >> > > >> Thanks, > > >> Felix Rech > > > > > > > > > > -- > > > 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. > > > > > > > > > > > -- > > 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. > > > > -- > 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. --000000000000443148058171b466 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Jon,

<= div>It is not true that Q(T) can be obtained from T simply by replacing jud= gmental equalities with propositional ones (I think this should be true for= some theories, but certainly not for all).

So, if= we denote the theory with an interval and judgmental rules by T_I and the = theory with propsoitional axioms by T_a, then Q(T_I) is equivalent to T_I a= nd Q(T_a) is equivalent to T_a, but Q(T_I) is not equivalent to T_a. Theori= es T_a and Q(T_a) are actually equivalent to the ordinary MLTT (since we si= mply add another contractible type to it).

Functio= nal extensionality is provable in both T_I and Q(T_I). It follows from the = existence of the interval type in T_I and it can be added as an axiom to Q(= T_I). I believe that theories T_I and Q(T_I) are equivalent to MLTT=C2=A0+ = functional extensionality, but I don't know how to prove this yet.

Rega= rds,
Valery Isaev

=D1=81=D0=B1, 9 =D1=84=D0=B5=D0=B2=D1=80. 2019 =D0=B3. =D0=B2 05:01, Jon = Sterling <jon@jonmsterling.com>:
Hi Valer= y,

I'm trying to square what you said with what Anders said. Consider exte= nding MLTT with an interval in two different ways:

1. With judgmental computation rules for the recursor
2. With propositional computation axioms for the recursor

I do not expect to obtain a conservativity result for the second version ov= er the first version, since the first one derives function extensionality, = and the second one does not (afaict).

Can you give a bit more detail about how this algebraic power move that you= are describing works, and whether it applies in this case?

Thanks!
Jon

On Fri, Feb 8, 2019, at 6:32 PM, Valery Isaev wrote:
> If you are not interested in computations and convenience of your type=
> theory, then the definitional equality is not essential in the sense <= br> > that every type theory T is equivalent to a type theory Q(T) with no <= br> > computational rules. Now, what do I mean when I say that type theories=
> T and Q(T) are equivalent? I won't give here the formal definition= , but
> the idea is that Q(T) can be interpreted in T and, for every type A of=
> T, there is a type in Q(T) equivalent to A in T and the same is true <= br> > for terms. This implies that every statement (i.e., type) of Q(T) is <= br> > provable in Q(T) if and only if it is provable in T and every statemen= t
> of T has an equivalent statement in Q(T), so the theories are
> "logically equivalent". Moreover, equivalent theories have e= quivalent
> (in an appropriate homotopical sense) categories of models.
>
> Regards,
> Valery Isaev
>
>
> =D1=81=D0=B1, 9 =D1=84=D0=B5=D0=B2=D1=80. 2019 =D0=B3. =D0=B2 00:19, M= art=C3=ADn H=C3=B6tzel Escard=C3=B3 <
escardo.martin@gmail.com>:
> > I would also like to know an answer to this question. It is true = that dependent type theories have been designed using definitional equality= .
> >
> > But why would anybody say that there is a *need* for that? Is it = impossible to define a sensible dependent type theory (say for the purpose = of serving as a foundation for univalent mathematics) that doesn't ment= ion anything like definitional equality? If not, why not? And notice that I= am not talking about *usability* of a proof assistant such as the *existin= g* ones (say Coq, Agda, Lean) were definitional equalities to be removed. I= don't care if such hypothetical proof assistants would be impossibly d= ifficult to use for a dependent type theory lacking definitional equalities= (if such a thing exists).
> >
> > The question asked by Felix is a very sensible one: why is it cla= imed that definitional equalities are essential to dependent type theories?=
> >
> > (I do understand that they are used to compute, and so if you are= interested in constructive mathematics (like I am) then they are useful. B= ut, again, in principle we can think of a dependent type theory with no def= initional equalities and instead an existence property like e.g. in Lambek = and Scott's "introduction to higher-order categorical logic".= And like was discussed in a relatively recent message by Thierry Coquand i= n this list,)
> >
> > Martin
> >
> >
> > On Wednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote:
> >> In section 1.1 of the HoTT book it says "In type theory = there is also a need for an equality judgment." Currently it seems to = me like one could, in principle, replace substitution along judgmental equa= lity with explicit transports if one added a few sensible rules to the type= theory. Is there a fundamental reason why the equality judgment is still n= ecessary?
> >>
> >> Thanks,
> >> Felix Rech
> >=C2=A0
>
>
> >=C2=A0 --
> >=C2=A0 You received this message because you are subscribed to the= Google Groups "Homotopy Type Theory" group.
> >=C2=A0 To unsubscribe from this group and stop receiving emails fr= om it, send an email to HomotopyTypeTheory+unsubscribe@googlegr= oups.com.
> >=C2=A0 For more options, visit https://groups.google.com/= d/optout.
> >=C2=A0
>=C2=A0
>
>
>=C2=A0 --
>=C2=A0 You received this message because you are subscribed to the Goog= le
> Groups "Homotopy Type Theory" group.
>=C2=A0 To unsubscribe from this group and stop receiving emails from it= , send
> an email to HomotopyTypeTheory+unsubscribe@googlegroups.co= m.
>=C2=A0 For more options, visit https://groups.google.com/d/opt= out.
>

--
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. For more options, visit https://groups.google.com/d/optout.

--
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.
For more options, visit http= s://groups.google.com/d/optout.
--000000000000443148058171b466--