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-ot1-x33b.google.com (mail-ot1-x33b.google.com [IPv6:2607:f8b0:4864:20::33b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 674cf025 for ; Sat, 9 Feb 2019 11:53:17 +0000 (UTC) Received: by mail-ot1-x33b.google.com with SMTP id o8sf5700886otp.16 for ; Sat, 09 Feb 2019 03:53:16 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Afr71vIodp3Wmsr6T4XQqtHfZSWbOWeKAsPPU7p40lQ=; b=BzXeXW1+JSFOxFjWfhwxe3i2RKDvgQ63tBXV0z3rzI23jA2jVyj5rET1/VVnSnV9bd rpjkw2Q2YswWA2igsCaZaP/PwEEWVAT7zGIppLEoWuO4aX11QYEbOfBqR9WvGsvbT+83 QDYEGKhgW2k2Ou8slKxZl5o1R0EQKzQCpTNUUoH9sSxxnyG3xvfHY2h4QyCP6y1CCrjH CklKHpt3+D0p8Uso7cDekaikiZOEnsCy10wa3uDsYDYqXvcc7W+HYB4o/lS6lt6U+vEm 46auwUQh0qhI2Co2IJMZnYOra6FYfSSZqy1Yjw/x10mHskDdpIpDjGSP8FueQ9qzf+bT gvrw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=Afr71vIodp3Wmsr6T4XQqtHfZSWbOWeKAsPPU7p40lQ=; b=Dpxbbxmwa3aKiMemO6WXokc6+ZTp5gKcZ/SQhzhnNLTNnD2qXipNNGIXlev44oj4sI JjKDwXoMfPVqpTwo5wCFq9la7VA7FNmZjybR2+OstvLFKMcrboOvvG9WDCYDkP5JJqBg tNd8koshu3YHwarI21yGfCFTRR9Q27lrSornodD0h+CSvG1f7l/mrpJuOdXYu6ExxP30 ekuy6gtXvMg//ySSrUDE4vCxkhp0kZ3fBUUh8QG5OwjmZzOOf9djC1n/HQmQgBuso5xs JVyn0eOmTvsMNZxu7hU7LDsxLVU10lddIut3xAE1l6p+sTTHfpP1X5ngSKJ17B2n26r9 zc4A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=Afr71vIodp3Wmsr6T4XQqtHfZSWbOWeKAsPPU7p40lQ=; b=ZW+i9VgmXi9oJr3JVpuWS/RK49HWQPVS1PVXcbK7QuMVLgJZ2N/J4WlAz5wuYxBhyI o8rHltKORhPf2cdQwKbNR8xXVZdLLBJbk4JoBFaar252CQ3aS4QaxzSQ/nAe8xoXRIeE x5kDy5EYZMkae5WynJZsOxvDnFKX4YwHa7MLBFRLIlZF2WMSRUq1AYDmEuZbj+PGUaLP 0XIBhWSXDfkTfzuLnDa/fpqZavCGr1/mnv0zV0ALZlU0BSxda40AtqCF+ipZ4rrSibcx yNl1mMEjXPoYU04A8QBXDNi6DRIZTO+nDrEfcfMbHqJ3gb84roCrX//5SSoVX3MyVfdD zpbw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuYd9+hj0H/cv6i3teYc8rgJFT/wH+/uOOlc6pjmLyJny/Y44mRa jy9QH54rA2cnOpRBwzy3cZI= X-Google-Smtp-Source: AHgI3IZMFfL/Y4HU5C38/t17muAUdBm/jk40G6wyCiNHfsdbD5uwhYS/UPhwjngXaVrAt9NI/fOlSA== X-Received: by 2002:aca:47c9:: with SMTP id u192mr28550oia.7.1549713196055; Sat, 09 Feb 2019 03:53:16 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a54:4605:: with SMTP id p5ls3243167oip.0.gmail; Sat, 09 Feb 2019 03:53:15 -0800 (PST) X-Received: by 2002:a54:4d86:: with SMTP id y6mr21247oix.0.1549713195553; Sat, 09 Feb 2019 03:53:15 -0800 (PST) Date: Sat, 9 Feb 2019 03:53:14 -0800 (PST) From: Felix Rech To: Homotopy Type Theory Message-Id: In-Reply-To: References: Subject: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_735_1183488318.1549713194877" X-Original-Sender: s9ferech@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: , ------=_Part_735_1183488318.1549713194877 Content-Type: multipart/alternative; boundary="----=_Part_736_503094476.1549713194877" ------=_Part_736_503094476.1549713194877 Content-Type: text/plain; charset="UTF-8" Thank you all for the discussion! 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. There are primarily two reasons for this: 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. ------=_Part_736_503094476.1549713194877 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thank you all for the discussion!

One of the motivations for my question was that I actually expect usa= bility benefits if one worked in a dependent type theory without judgmental= equality that has good support by a proof assistant. There are primarily t= wo reasons for this:
  1. Judgmental equality cannot be taken = as assumptions. If one wants to use judgmental equalities then one has to g= ive 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 =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 behav= ior.
Another motivation was of course that it would sim= plify 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 &= 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.
------=_Part_736_503094476.1549713194877-- ------=_Part_735_1183488318.1549713194877--