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-xa3c.google.com (mail-vk1-xa3c.google.com [IPv6:2607:f8b0:4864:20::a3c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3b1101f5 for ; Sat, 9 Feb 2019 14:16:15 +0000 (UTC) Received: by mail-vk1-xa3c.google.com with SMTP id d123sf2595364vkf.23 for ; Sat, 09 Feb 2019 06:16:15 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549721774; cv=pass; d=google.com; s=arc-20160816; b=SqLDFzM2Kngapl7sa8dkpBpm6gQJbI3A3XH2fxO0XLZqf5YMxy8fUXB/ePymcsfumG AZu/Z9uLrLibr6O5uQoLdehHsbr6qcpKJInK3TbZ7jM8lauXZKleY12IKJUF7UK5rbdE 322UEtosW3AAaxULOXx8e3oqCr2kf/d9Qzvtb3YYHrKpZ75SozWRJoWXnejC9KTAEQK+ ZIjNF3+qpiPLZ6B22/TmIphsF/S59wHC8Bagq9A1AQcf8QFfg6bRSBW6FCbMaxlQnsgC uc2S86oJElFD6pMtYwzZJD2v0GHRJX2GozzGk5PLS3LT+TsF26znLR1XeyAwhd4Tq26l G/Sw== 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=hG4z7gk87E8d6pEqTPLSThwMeEUgN13LZgtxnnX5TeM=; b=QpfpKs4u0W0N37EAYn89uElyiHkG0XZSGLEhqK3bElFQRqKQvgsjBXE5MDZUuu9EME O4w4UrxiO09DPc8sbcuLfFczsVQ8zGQRh9/ZNc0AMq7OjwgP2B/WHZykZfpNwIAXF0Lb ZRim3jmb1aOEDxlwczAnf8tvHdx03ptg/a+7iBii10yx9qC84AASwFBPBszr8TElcN3z DCYZs5XAHrY3TA/3skyS50W3Arz/lYAbxUNlg8yu+CynLSbrWBGQFMcoyLoffCog55by lEGq/VqfNp2GhiK2mnBQAQ8NRBaByR9JQhh2vUS+Eo+grFjHTkTqhBIzYbvohG0F76mi v6Uw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=E8gmAVNi; spf=pass (google.com: domain of gabriel.scherer@gmail.com designates 2607:f8b0:4864:20::730 as permitted sender) smtp.mailfrom=gabriel.scherer@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=hG4z7gk87E8d6pEqTPLSThwMeEUgN13LZgtxnnX5TeM=; b=cJZVybDbdx1d1XWij+E7Eg14PIG2/AWl1+0nPPRI8rYkidPCwh2aZT/gDvHiEiUTBb R5v4M7/ilMHcnhunyGFSy2ozmv+Tq+Hovh2ZFZ5TXtErXv3MqkNtBBhvjpxHeRF9xc7E clleChZPnnheCt9gc/EowJrs0il4sayEEFZFL2DM6Sg4N5MDHx7e8X5+a0FgkB0YqJva RCmgfoULrYpkx+gYwWreNWSKbHV10iUSsF33JKckgTlnh2rv4jQL76aPk0LdwFfuBUyf OvjDTScDWB1Dp4RgV9IwV+Qr9jWUBXWH6qdcgpvtRN49TS+3HIrFnlBpH9nwrsU1gKco GX0Q== 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=hG4z7gk87E8d6pEqTPLSThwMeEUgN13LZgtxnnX5TeM=; b=h9OtbsMohuGaQaV/HThPTxswbGu4SnYQIAhBSpG+JKTEsHvCd8Ex65uZ0gtmDg7G0Q J58TOaPT9toyxwhqlF/T1xYkCuUhE/f9X7hBTfRdTQsljV5QIcOmBYfiX0IYi+BESVpl QqTKEJLzjuOCuy/4fxmSCNtT7BEhtZU21pZDbvohzM1h2/1vrvK4L7n1za3MPwL2Q+kh 00kzZUeC1R6zoD2jje6Mz2IdXtZQvU6xDz83WFpqjC6VbIajyvZrzhZxLp5G+h2RXiM0 x3cUvD24hYUDQUy8owVfT7zrj33S/jA/o1iNhWEYFumituZSMeVg1tBlDJe+txv4uahP SVjg== 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=hG4z7gk87E8d6pEqTPLSThwMeEUgN13LZgtxnnX5TeM=; b=ryE25LB/P8idNzpqckVo8K+x4Cl+Wm1ptfMVbSQpBvfbKaXYsRIxan+5l/Bh8q2BMW arj4tcELISl1G2lqlrHezsnb3DBCVZFk1HYpXmW2FiHA2vuHs/+X55cu5kjag3Zuzifd oxNiCtum6qevr5eGYJMKJf5YHq2g7hccEPTs3RJQvr4AGeQAXrGE8IjQ9+zp2CBxF9cQ 6VCTIdezbSpx3Fa+eFldGNxvzJ7tucTFJODnEfhPVzvTjbOuSP9sl5XS7PsQzGMmucVH GFlCkUZQEX71kx0urijMdwQaQoAn0TD+07/x5NbyihpZGnwvk8YiRTv8XixdywSd1a4u 9gwA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAua8G6c5XjofJVMIDDm4a2S39/B4fv0NcMPEGfeajOYSVqiSWaz0 bKPJET1BBtKM/wU6hG878ZU= X-Google-Smtp-Source: AHgI3IYwLA/VF6LU0pI/izo7jYYFoCTN3WQFmXTP6woHaRD9v3qjJU1rVd52uJvqt20GMZsj4bCcaw== X-Received: by 2002:a1f:8204:: with SMTP id e4mr78208vkd.5.1549721774016; Sat, 09 Feb 2019 06:16:14 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:9d0f:: with SMTP id g15ls1484917vke.1.gmail; Sat, 09 Feb 2019 06:16:13 -0800 (PST) X-Received: by 2002:a1f:a78c:: with SMTP id q134mr17707284vke.6.1549721773649; Sat, 09 Feb 2019 06:16:13 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549721773; cv=none; d=google.com; s=arc-20160816; b=Mr0j2Ui/BqwLR2w14Nc6XbCAc76Yc8W2SGsSmAX0cdPJNIn2VwciAQz3mFxsLtFPku 7GJHcu7ke0jS3HJIpOqLzRz+AiHIsgbNqh6xEKvMqVlFwqm3gNrBT1UgHKTIcu6kn1GN vFZGtTd1keirauTCqz8p2lenvBjkSI3jilgFxLsGGIg7/DvGL6TyI45lAmxI2RDCK6mf SEByiJu31UhEmopOKD+qQ28mIJRXwno91Idszmi8s0Px3IYVQqscsjb5iLUKWJTLH+eB RN3FhkoLRz7c5ZNYvr0yDbJeEi0IVMEgUxbbkfW2y4+b2HrMq2Ue8fuPHe2QeJpKRm0F k69g== 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=7aM9S2GVJgqdAqkowMHGQi5kDe9+hURFRl3EaU3n1tc=; b=hB74WSY3vCKOkNlAQCdNO4kV5cbaabuMQQjqQb4wFFHo/Ygdfo48OSevTRYiuxh/l3 7vGvlQKMCho7qyP1wnJuos8LjSWukkCwwlDHXPv5T5uXzLgmEnn5ar7Xemg7a0usQNUm AuvjPOSPNBorN6Q9jbygS0j+cM3ayhj0rLVMjtdFT0KdcJVvqQ4IV9+UsKW6bT6Xh/o3 nSHEzivnEMX+E2vmrvpycChjqlwnxicKTAfMebCArxGsnW6OzZYdGpQbza/r1JDvlxTb ilsCGpSwzW5oyUvzzPW5YlECGojHSAA0O/R/mc2r91XsVDd1EgI3+SjaYc08sAWRYIbJ hb8Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=E8gmAVNi; spf=pass (google.com: domain of gabriel.scherer@gmail.com designates 2607:f8b0:4864:20::730 as permitted sender) smtp.mailfrom=gabriel.scherer@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-qk1-x730.google.com (mail-qk1-x730.google.com. [2607:f8b0:4864:20::730]) by gmr-mx.google.com with ESMTPS id x65si413157vkg.2.2019.02.09.06.16.13 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 09 Feb 2019 06:16:13 -0800 (PST) Received-SPF: pass (google.com: domain of gabriel.scherer@gmail.com designates 2607:f8b0:4864:20::730 as permitted sender) client-ip=2607:f8b0:4864:20::730; Received: by mail-qk1-x730.google.com with SMTP id q1so3817818qkf.13 for ; Sat, 09 Feb 2019 06:16:13 -0800 (PST) X-Received: by 2002:a37:b046:: with SMTP id z67mr19190806qke.350.1549721773325; Sat, 09 Feb 2019 06:16:13 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Gabriel Scherer Date: Sat, 9 Feb 2019 15:26:54 +0100 Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: Nicolai Kraus Cc: Felix Rech , Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000ccc24c058176b794" X-Original-Sender: gabriel.scherer@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=E8gmAVNi; spf=pass (google.com: domain of gabriel.scherer@gmail.com designates 2607:f8b0:4864:20::730 as permitted sender) smtp.mailfrom=gabriel.scherer@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: , --000000000000ccc24c058176b794 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable A relevant citation for this line of thinking (if we reduce implicit computation, can we gain usability some other way?) is the work on the Zombie programming language, which tried to weaken beta-reduction in a dependent language (restricting it to values only, as in F*) to obtain a more automatic form of reasoning upto congruence (definitional equalities can be put in the context and used from there). Programming up to Congruence Vilhelm Sj=C3=B6berg and Stephanie Weirich, 2015 http://www.cs.yale.edu/homes/vilhelm/papers/popl15congruence.pdf On Sat, Feb 9, 2019 at 3:05 PM Nicolai Kraus wrote: > On Sat, Feb 9, 2019 at 11:53 AM Felix Rech wrote: > >> One of the motivations for my question was that I actually expect >> usability benefits if one worked in a dependent type theory without >> judgmental equality that has good support by a proof assistant. >> > > Yes, me too (but I think *a lot* of work needs to be done before we can > have a proof assistant based on this idea which provides better usability > than the current ones). > I agree with your points. But I think "x + 0 =3D x versus 0 + x =3D x" is= an > example where I'd expect that one should be able to produce a > conservativity proof and use both at the same time instead of choosing on= e. > I think it's not necessary that we restrict ourselves to computation rule= s > that come from actual definitions; anything that is "constructively > conservative" over a weak theory should be allowed. In Agda, one can have > additional computation rules, but it's not a safe feature. > Nicolai > > > >> 1. Judgmental equality cannot be taken as assumptions. If one wants >> to use judgmental equalities then one has to give concrete definition= s that >> satisfy those equalities and cannot hide the definition details. This= makes >> it impossible to change definitions later on without breaking constru= ctions >> that depend on them. >> 2. In nontrivial definitions, judgmental equalities seem more >> arbitrary than natural. If we define addition of natural numbers for >> example then we can choose between x + 0 =3D x and 0 + x =3D x as jud= gmental >> equality but we cannot have both. This makes it hard to find the righ= t >> definitions and to predict their behavior. >> >> Another motivation was of course that it would simplify the >> implementation of proof checkers and parts of the metatheory. >> >> I would appreciate any comments on this. >> >> -- >> 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. >> 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. --000000000000ccc24c058176b794 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
A relevant citation= for this line of thinking (if we reduce implicit computation, can we gain = usability some other way?) is the work on the Zombie programming language, = which tried to weaken beta-reduction in a dependent language (restricting i= t to values only, as in F*) to obtain a more automatic form of reasoning up= to congruence (definitional equalities can be put in the context and used f= rom there).

=C2=A0 Programming up to Congruence
=C2=A0 Vilhelm Sj=C3=B6berg and Stephanie Weirich, 2015


On Sat, Feb 9, 2019 at 3:05= PM Nicolai Kraus <nicolai.kr= aus@gmail.com> wrote:
On Sat, Feb 9, 2019 at 11:53= AM Felix Rech <= s9ferech@gmail.com> wrote:
One of t= he motivations for my question was that I actually expect usability benefit= s if one worked in a dependent type theory without judgmental equality that= has good support by a proof assistant.

Yes, me too (but I think *a lot* of work needs to be done before w= e can have a proof assistant based on this idea which provides better usabi= lity than the current ones).
I agree with your points. But I thin= k "x=C2=A0+ 0 =3D x versus 0=C2=A0+ x =3D x" is an example where = I'd expect that one should be able to produce a conservativity proof an= d use both at the same time instead of choosing one. I think it's not n= ecessary that we restrict ourselves to computation rules that come from act= ual definitions; anything that is "constructively conservative" o= ver a weak theory should be allowed. In Agda, one can have additional compu= tation rules, but=C2=A0it's not a safe feature.
Nicolai
=


  1. Judgmental equality cannot be taken as a= ssumptions. If one wants to use judgmental equalities then one has to give = concrete definitions that satisfy those equalities and cannot hide the defi= nition details. This makes it impossible to change definitions later on wit= hout breaking constructions that depend on them.
  2. In nontrivial defi= nitions, judgmental equalities seem more arbitrary than natural. If we defi= ne addition of natural numbers for example then we can choose between x + 0= =3D x and 0 + x =3D x as judgmental equality but we cannot have both. This= makes it hard to find the right definitions and to predict their behavior.=
Another motivation was of course that it would simplif= y the implementation of proof checkers and parts of the metatheory.

I would appreciate any comments on this.

--
You received this message because you are subscribed to the G= oogle Groups "Homotopy Type Theory" group.
To unsubscribe from= this group and stop receiving emails from it, send an email to H= omotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, vi= sit 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 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.
--000000000000ccc24c058176b794--