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-wm1-x337.google.com (mail-wm1-x337.google.com [IPv6:2a00:1450:4864:20::337]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 09bc87d1 for ; Sat, 9 Feb 2019 14:05:11 +0000 (UTC) Received: by mail-wm1-x337.google.com with SMTP id f202sf2661812wme.2 for ; Sat, 09 Feb 2019 06:05:11 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549721111; cv=pass; d=google.com; s=arc-20160816; b=NuXWgrIZ/BUF4+XfFsLWuBIgw68vkrMXO/Uqtmp12PgEzy2LFrbyuj435u4Y//9uS7 MufAMETHgdoHqrgTGmjkHCr9DA2hMJIqts3In18OiH8UicGzgq1vZebih5z9fXKGUplO TkvGBL72bhBGrOZMhy3wdPVy0aJz5lg5wxjw9F9rcjLwjVCNPnUdfz8SD+0p7LhfONHW zJgurAMz5SgKSGuPSnSbZAVsCMhqv+XQyOtxic8v2PCs7Zyldaw1evrVYCb5YD8HvZSU EVld3oddoGSvOPVAE4jW9Ty0XPUDwmO5sqpaBORjaLO2XCU/VKQl6xRXWIy+uyDMfmPp n+mg== 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=wIblSsubkVvRXMysELJn3VNeDtdlx3sqHmIH4mrHfdg=; b=duOVmw9iYlVz4/Eh+GyDosX3Lfzwd5weFLfMagsdoCeji2dU3JKzV6QsKBwheRfRvp 3lMVzLtTInFHP8kIVmaFLF6aojouqbVnCWhkZscA4hL5x7AQQrETFUNYpmtJznBsrcHw 4buXgS4lpXR9d0R9gRceYvkSUDaJcpJKMk8QIyph+kkclvH0P6g94xd0994S3oBV3djC N/shImPQMZTJKrKJ5Hwih06ZFEAgb5j1DkK9DbraCp6yD7HF/6DOAwE9gDr1PeXTxp0x azTeOsoRd4EwUMda2tiKbWUhDjEhnIfxAooV6Q3ck4XvA7HkxpWx/EZBujbeopXG+V+d E1UQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=dX0WjD1i; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::12a as permitted sender) smtp.mailfrom=nicolai.kraus@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=wIblSsubkVvRXMysELJn3VNeDtdlx3sqHmIH4mrHfdg=; b=n+qeiqoTEbezK0e5b/ySbeNXsXN+jbKE7DWXWh3PTaYIaeRu64KcAaMpBFe0K/wr4t NcqTJOQQbTG/NLp3IXjXFRsK8PSkJzeDwaL8YhnO73yUPd6b+MTjvGFTiZOqMoKBAOQf wqg4QyVglm5FHvixgYh4ghMtKD/JM2JM70/Y55OQS2AwXsWAGWL0Z0aGQjI6MJYKKm+G 6nt/xEU0mpeUq//Y/KxhMuoYnkXOBKwqs/cdlWKGVazCStfuOPARUwfkvnNC0uj2IXJD eHjaDoaoZaFGalkGYCfy4+o9quqx2C2tt4R0rZ6b9NBC0lVmsGniaZHkXnBxIL5KmeNA dALA== 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=wIblSsubkVvRXMysELJn3VNeDtdlx3sqHmIH4mrHfdg=; b=tdowPDt3olBIQ5K9YfE/gJcSS8Mi3mqrOQDbd/qzRXhRZvfi7jiWI7iBkj6cwCw3bz jHEQHE3rB1W3QnwJkihYfEOQwUCfeMKUBeTvtSr8I1kJt7TJOFjKBh1CVGAFluG56kR6 0agty5exw7WL5/FUro0sbd7k0beD//R16nDmUbV5qxllF4r/ujnk9/CtYjYMXIYX3vn1 oLIsnfCf3G6KKrBT7c0+O60vHA3jdzkWEX8pFwJYywKkO/5T0IoV0jl1111XcmQ4cDvI cBMe+vDQWwr/QZfX5mMfMOW3mUkhbE7RF9zlMiNlofGQmzNtILFj/+Yfhxj48AtOGU7E P8xw== 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=wIblSsubkVvRXMysELJn3VNeDtdlx3sqHmIH4mrHfdg=; b=VCXIHJperFBxzEHn6QlI7pjQRg2nbFRqK3a4uQYIJ0UG7mHGy5dFk+Lr2EfOBJMU7D aFLfsocKks7xNSc2zVRVh1Kqb5AX9RzJEEbg2Lt3o+iji6UneI2wPSUo5vDP07Ve2Hwa kue6oAlW2PQ7MG3HfL8zGdH8Qyyvby0tAgmxIhgOyjDy3h5/4m/ZZ0AyC7uZrqDhXYhs ey/gpfaToYXJHX2xUh+uoKSGhDS90cCEtmjJTNjQW5iPOa5WUe4bZ+HLDBwPc1VRHs7K jaxqPatovxXtUvU1tjHfmWmMsfsQA7bOWhosDkNH+IJsViqPwf2os5d/oyUWPLCzjSfF aIZQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuacXU+Z2UVhptK6fazjrmDDxM4gcPQkOpGu3kPkbzP3Oebo1TQ2 S2xDNyzZfBvNFDKeauWmuZM= X-Google-Smtp-Source: AHgI3IYW3SY2MXS7LH/bKgQRLX5qWJwqdwJVKGV0tVE66kHoROblcjySubXLWOOvZzqzBM5rPYbt1Q== X-Received: by 2002:a1c:9cc7:: with SMTP id f190mr31509wme.0.1549721111088; Sat, 09 Feb 2019 06:05:11 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:35c6:: with SMTP id c189ls1098887wma.13.canary-gmail; Sat, 09 Feb 2019 06:05:10 -0800 (PST) X-Received: by 2002:a1c:f613:: with SMTP id w19mr215284wmc.18.1549721110490; Sat, 09 Feb 2019 06:05:10 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549721110; cv=none; d=google.com; s=arc-20160816; b=yA6rHUYAZac2G0cGNGSclHkkQt7M3Q3A9ttOeQc+B30tJzTdMToedTKP85z8tHDTEg J0avX1a0oWhFqz4rCKn3+atEERWJE7AXokAm62CZNWu7RsIF7TKtQs8t1jfcoaZGvRkX k60eM754nr1NYds245eLHNo1NYh0466lBJvitk96UGY+hQ9KmmGLLujW1jOM7BI32Ecn ijvDAee60k5l1AK5WYg/HfV2iNr585uUv2PkjkZKsh6FGqFu1T57TwdRnD4XIHkZxo/g IgQtfkvFYNJVCvgf7GAG1VSTsM7zgV9yTvRkySfMpeJXiDLrPOJp+B5zCBv1OWrdJriE HQ7A== 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=BIb9uWxl/rod5KNxu0UHMl/ndboimk9ZPAQ/KERb7tw=; b=OQdOmcZp/4bFdkBo7dHpj8INxLtQrC/Tai7K1U9+UaVyWJNTn9o5GUUVgdhiDF0uyk WRYljvtx2XZkpuYoOF/aDHeN6qANNZyNKs11OpWnjkok3KbyqclKvmH99qdMefBCJMDo 6VXXKWDznDruP+1m7C0s5SKEfQg0evKbr2O3yzQ8yzDku/FO5lAugypndNYg3GK6yD+P EWDrH8J0uuaKOmSsnWckwpDp6yTPjt55fVi6ROaqntm5zC/uUFGocivsweONntKZ+4L8 Td80Ma2+vA40LWyC8TlaAQWw7ASa2uoSDav+XTK6MfNp1d+r55chAz4xzeDQCUsiDcml E98Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=dX0WjD1i; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::12a as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lf1-x12a.google.com (mail-lf1-x12a.google.com. [2a00:1450:4864:20::12a]) by gmr-mx.google.com with ESMTPS id q5si213822wrn.0.2019.02.09.06.05.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 09 Feb 2019 06:05:10 -0800 (PST) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::12a as permitted sender) client-ip=2a00:1450:4864:20::12a; Received: by mail-lf1-x12a.google.com with SMTP id q11so4627782lfd.3 for ; Sat, 09 Feb 2019 06:05:10 -0800 (PST) X-Received: by 2002:ac2:51af:: with SMTP id f15mr16660370lfk.44.1549721109761; Sat, 09 Feb 2019 06:05:09 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Nicolai Kraus Date: Sat, 9 Feb 2019 14:04:58 +0000 Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: Felix Rech Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000003f95f20581769094" X-Original-Sender: nicolai.kraus@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=dX0WjD1i; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::12a as permitted sender) smtp.mailfrom=nicolai.kraus@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: , --0000000000003f95f20581769094 Content-Type: text/plain; charset="UTF-8" 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 = x versus 0 + x = 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 one. I think it's not necessary that we restrict ourselves to computation rules 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 definitions that > satisfy those equalities and cannot hide the definition details. This makes > it impossible to change definitions later on without breaking constructions > 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 = x and 0 + x = 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 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 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. --0000000000003f95f20581769094 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Sat, Feb 9, 2019 at 11:53 AM Felix Rec= h <s9ferech@gmail.com> wrot= e:
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 as= sistant.

Yes, me too (but I thi= nk *a lot* of work needs to be done before we can have a proof assistant ba= sed on this idea which provides better usability than the current ones).
I agree with your points. But I think "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 and use both at the same time ins= tead of choosing one. I think it's not necessary that we restrict ourse= lves to computation rules that come from actual definitions; anything that = is "constructively conservative" over a weak theory should be all= owed. In Agda, one can have additional computation rules, but=C2=A0it's= not a safe feature.
Nicolai


<= blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-l= eft:1px solid rgb(204,204,204);padding-left:1ex">
    =
  1. Judgmental equality cannot be taken as assumptions. If one wants to use= judgmental equalities then one has to give concrete definitions that satis= fy those equalities and cannot hide the definition details. This makes it i= mpossible to change definitions later on without breaking constructions tha= t 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 judgm= ental equality but we cannot have both. This makes it hard to find the righ= t definitions and to predict their behavior.
Another mo= tivation was of course that it would simplify the implementation of proof c= heckers and parts of the metatheory.

I would appre= ciate 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 http= s://groups.google.com/d/optout.
--0000000000003f95f20581769094--