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.2 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 6298409a for ; Wed, 13 Feb 2019 06:37:53 +0000 (UTC) Received: by mail-ot1-x33b.google.com with SMTP id l8sf1178617otp.11 for ; Tue, 12 Feb 2019 22:37:52 -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=8vefHYm/1Z4tO06ADAu25wSINJy54Zpq3QHvDrkBr24=; b=TxwLjj/pR6EAI4WOCeNpTwF8xujcaH/9uzBT9h+w0XhEYAhgu771b7y5XKh69VGk2O SdOoSeTA95kGIl52KDIVjzidKE6cIYDNvlswS72zmOmghjRNLjtRFJ1iCyl4/s4URvt8 CjBNNf4kobW4xJL3+2+VDnYBjc1nQmR9fMjwBNOYeGWcMLxaUhTj1J4t7kmBcsouxann 44AWnmYUC6TRK9BL9OzsN8YoMsNMCNxVWDS1C74u7GMT1rvAdJkb2DPqRrj/OfERMiT6 otYgcXso+iiN1aaGCjiYWmCAlwEo5KWi4+bEMcFYTF/YMcfM0rq8T17fIC7LmRnM0IeP yEnw== 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=8vefHYm/1Z4tO06ADAu25wSINJy54Zpq3QHvDrkBr24=; b=r+dED/0aMWM4lW+o7UBuTUtw6KbDDpvzLYbrJ1hTMvN9Xa/hLRXDUFCe2TQD+1yHB+ fry8Y6h3fjs0aUQFLyFCZvmGdfqVLGzzX3KwYie7/3WDXBvJ96NktEqQEFj/dqZSlfew j6Mh73NOtQDUWyKCPFPG+YHRYQqkzdAfctGaTYfd0Lv8W4hrxwsbsqeadU8mPwGiH4eo Bk3017rGInYHwMBhE8c1j74kB4EaeBjBAx1dELKY0j3O4FpSM2o6sfMG/TjaUtX/mlvB yNpyBZVzhiu6o5kxcdWQRkSho7tl51Pc/5yley4bUqwE54qFI7outBnMs3a2lERnT4td fj/w== 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=8vefHYm/1Z4tO06ADAu25wSINJy54Zpq3QHvDrkBr24=; b=QSK59A4WAwY0sij3cznesfsvwZLD+hUZw4j7o3/Q59ANspCkBf+rL3B69F4mSIwILq 75ipuL8SrCCZm7YDqYDwBxElGia/drq7m1i52zlBKZ8VAuiLezCnQo7jSWriigCWHMXh RkDki3K0eU9/AuwIOl3fD4i5ielQdhxutFk2w8Sny/8D8x1shSTlzMbJgm1uDYyP+YcW xw6tfQjz/9NlM5zQ2keDuc5nyko+5RHhotYZiKkKiL6LLnW8LP0Z5n4lC1GLBaR7ZbIn 6vlWhu+5oKGZw9n+R9IfXvJkZaAbpCIvFCsnMebg5yEPJJySBHFunxM+8X4sX3RoJh58 yuYw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAublD+Uey3+RgT9jwZYsF5lxrd8iGUQ1Ox2DUgSClqfDBI9Kslko 7T8PR3GjzPwy8G8+Lez3GvI= X-Google-Smtp-Source: AHgI3IY7/ahwH1wdyOIgjlxc5jwZ/2AFskPxqn74+swpDkYvDg6DaaNj32zjRmbr/t+1ccEokx4d3w== X-Received: by 2002:a9d:19a4:: with SMTP id k33mr165602otk.5.1550039871962; Tue, 12 Feb 2019 22:37:51 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6808:28f:: with SMTP id z15ls6172899oic.4.gmail; Tue, 12 Feb 2019 22:37:51 -0800 (PST) X-Received: by 2002:aca:8c7:: with SMTP id 190mr14165oii.1.1550039871630; Tue, 12 Feb 2019 22:37:51 -0800 (PST) Date: Tue, 12 Feb 2019 22:37:50 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: In-Reply-To: References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> <3d0f6986-0136-480f-8c01-b593cbe3fff9@googlegroups.com> <84a7fbdf-aa40-4d4e-a3f7-1285f1171625@googlegroups.com> <7b35e7cb-3021-44cd-8c97-a7cc1159f999@googlegroups.com> <58de3e94-fee9-405c-ab18-5a35cb90eb68@googlegroups.com> Subject: Re: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2384_826365739.1550039870932" X-Original-Sender: atmacen@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_2384_826365739.1550039870932 Content-Type: multipart/alternative; boundary="----=_Part_2385_1434063516.1550039870932" ------=_Part_2385_1434063516.1550039870932 Content-Type: text/plain; charset="UTF-8" OK. So it sounds like definitional equality is another way of thinking about equality of sense, and is generally not the same as strict equality. That's a relief. But the use of judgmental equality for capturing a system of paths that's fully coherent is actually about strict equality, in general; not necessarily judgmental or definitional equality. So to bring things back to HoTT, what are people's opinions about the best use of these three equalities? My opinion is that strict equality should be implemented as judgmental equality, which should be richer than definitional equality, by using a 2-level system with reflective equality. This is the case in HTS and computational higher dimensional type theory. We would still probably want to consider different theories of strict equality, but there would be no obligation to implement them as equality algorithms. Definitional equality would be a quite separate issue, pertaining to proof automation. On Tuesday, February 12, 2019 at 12:54:24 PM UTC-5, Michael Shulman wrote: > > For sure definitional equality doesn't have to do with models. Like > all the kinds of equality we are discussing, it is a syntactic notion. > Actually I would say it is a *philosophical* notion, and as such is > imprecisely specified; syntactic notions like judgmental equality can > do a better or worse job of capturing it in different theories (and in > some cases may not even be intended to capture it at all). > > > what's the difference between "denoting by definition" and regular > denoting? > > x+(y+z) and (x+y)+z denote the same natural number for any natural > numbers x,y,z, because we can prove that they are equal. But they > don't denote the same natural number *by definition*, because this > proof is not just unfolding the meanings of definitions; it involves > at least a little thought and a pair of inductions. > > For a more radical example, "1+1=2" and "there do not exist positive > integers x,y,z,n with n>2 and x^n+y^n=z^n" denote the same > proposition, namely "true". But that's certainly not the case by > definition! Same reference; different senses. > -- 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_2385_1434063516.1550039870932 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
OK. So it sounds like definitional equality is another way= of thinking about equality of sense, and is generally not the same as stri= ct equality. That's a relief.

But the use of judgmental equality= for capturing a system of paths that's fully coherent is actually abou= t strict equality, in general; not necessarily judgmental or definitional e= quality.

So to bring things back to HoTT, what are people's opin= ions about the best use of these three equalities?

My opinion is tha= t strict equality should be implemented as judgmental equality, which shoul= d be richer than definitional equality, by using a 2-level system with refl= ective equality. This is the case in HTS and computational higher dimension= al type theory. We would still probably want to consider different theories= of strict equality, but there would be no obligation to implement them as = equality algorithms. Definitional equality would be a quite separate issue,= pertaining to proof automation.

On Tuesday, February 12, 2019 at 12= :54:24 PM UTC-5, Michael Shulman wrote:
For sure definitional equality doesn't have to do with models.= =C2=A0Like
all the kinds of equality we are discussing, it is a syntactic notion.
Actually I would say it is a *philosophical* notion, and as such is
imprecisely specified; syntactic notions like judgmental equality can
do a better or worse job of capturing it in different theories (and in
some cases may not even be intended to capture it at all).

> what's the difference between "denoting by definition&quo= t; and regular denoting?

x+(y+z) and (x+y)+z denote the same natural number for any natural
numbers x,y,z, because we can prove that they are equal. =C2=A0But they
don't denote the same natural number *by definition*, because this
proof is not just unfolding the meanings of definitions; it involves
at least a little thought and a pair of inductions.

For a more radical example, "1+1=3D2" and "there do not = exist positive
integers x,y,z,n with n>2 and x^n+y^n=3Dz^n" denote the same
proposition, namely "true". =C2=A0But that's certainly no= t the case by
definition! =C2=A0Same reference; different senses.

--
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_2385_1434063516.1550039870932-- ------=_Part_2384_826365739.1550039870932--