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-x339.google.com (mail-ot1-x339.google.com [IPv6:2607:f8b0:4864:20::339]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 7e584f36 for ; Mon, 11 Feb 2019 12:17:53 +0000 (UTC) Received: by mail-ot1-x339.google.com with SMTP id q11sf10679202otl.23 for ; Mon, 11 Feb 2019 04:17:53 -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=RzMeeqeIIYd6yIoodQC78LqGFvc4zs2WUbyRAVsEG+w=; b=W7h7pO9v8xZ1ww2T8zwiG0Tvsp6iGPtF8SAHVmXj33vs+dDGNvTWbjqY0HdelVhpfc A3fbYLMcxQU6g4r3sgpDuPeBTz0MaoVZV8YEHjHtFzIxcTStoaEHQn/vivzrQ1OUGiWA zJqD5QdfqJX7dgLSO5mZ7eGyeP4UfBbrLAqufm14aDeR9pqBmxabzw7WVZ5EcEnwdl18 12q8b8Ejuu+RR0jtFgbBHH+WwNHoJhPGabOh8vWhWOBwSihYkY1Cp+7aMc1FCtrRcwaF uDjTzPlOzkzbf4EsqBXVS31WNi3C4o9Kt7oQ7+OO6RwV1H2tKIYvMsrZRs3r1uxgaHVh 55Bw== 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=RzMeeqeIIYd6yIoodQC78LqGFvc4zs2WUbyRAVsEG+w=; b=Aex38QJPsY1wTzrDKN7cdkfB9Z/N+xqUFsBXsHup+RvbwySqAhRPUB0ZGCd0K8BcQe /EN5s/zEddCBWMCJRdffI1RJTskcdV6nuO9WUCqYdincYIMrRvCA4saocNFKJUiZEI4Z BTm7NwRkJ98M/+HgwZ6wio1t9rt94I/s428XA6tOMusYVt/9v0KaXzFerqX/JGksheoW icC3bOYb3uDBrfkmODuUzsNX3WBXGeMBFmmmcQqavqljjCOXopL22j8/Hj10o5bv2ayQ 5DU7O5VJBmWl+C9AEOSC0+mZKTpYjwjarxy5+hlif5NALhxYT2AFh1CX9+i1YhluGcob MZwg== 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=RzMeeqeIIYd6yIoodQC78LqGFvc4zs2WUbyRAVsEG+w=; b=RGsdEQ4Epb2b5ZHjiz4bgNfTJdE/qCrk3hrtGrpVJRHNz6hvA9E9BbjIhv6RdfTyLO aO/N22d+bNL43HVzcIvZSuQo76vqwnO3s5m4Y+94lnjcq37OFMMb7904NHv/7e3B0HRB de8iMGqPRn2IBqcIVoHPuZvKX/Ow7N4YmiNiZqeBwEYn3LGBvG/yPjqYFFXzQ231y9+Y KdYPF5m3pXNoT5cme4ABFGCPoXgJEkkMZBFHoYQMwr4HaYugtN1oRr+vsydkR5YTi4F3 KKaCrENuyE3i83ZI3y0QtEpXy7GNqbF0Jf4YDXEtAfIVlkCmJAu7SUllnKvcXlRUiVo6 1Lcg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuan/q7voaaKvcKSWl7hfzt5B6N66LISShw1UxfqFVNild3ssvlP 6dXF0FtN/T4oqCBvUCskXvc= X-Google-Smtp-Source: AHgI3IZuSBkmRaKJlhsQuF4HEBuziQS/GgGP0ZeMBNqrn/KQNsfsrSuIyGjS6E/9RhgayF+EZlQQ7w== X-Received: by 2002:aca:4b89:: with SMTP id y131mr24307oia.3.1549887472394; Mon, 11 Feb 2019 04:17:52 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6830:164a:: with SMTP id h10ls1756049otr.7.gmail; Mon, 11 Feb 2019 04:17:52 -0800 (PST) X-Received: by 2002:a9d:654f:: with SMTP id q15mr399269otl.6.1549887471835; Mon, 11 Feb 2019 04:17:51 -0800 (PST) Date: Mon, 11 Feb 2019 04:17:51 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <3d0f6986-0136-480f-8c01-b593cbe3fff9@googlegroups.com> In-Reply-To: References: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> Subject: Re: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1240_691413597.1549887471275" 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_1240_691413597.1549887471275 Content-Type: multipart/alternative; boundary="----=_Part_1241_1086510789.1549887471275" ------=_Part_1241_1086510789.1549887471275 Content-Type: text/plain; charset="UTF-8" On Saturday, February 9, 2019 at 3:34:22 PM UTC-5, Michael Shulman wrote: > > From an implementation point of view, I agree that in the long run we > should have proof assistants that don't hardcode a fixed set of > judgmental equalities. But I don't think that means eliminating all > judgmental equalities; it just means making the logical framework more > flexible, such as Agda's ability to postulate new reductions or > Andromeda's framework with equality reflection. In particular, the > new equalities that we postulate should still be *substitutive* (as > Jon says, allowing to perturb a judgment without altering the proof > object) rather than *transportive* (requiring the proof object to be > altered) -- I think Vladimir was the one who suggested words like > those. I first heard those terms was on this list: https://groups.google.com/forum/#!topic/homotopytypetheory/1bUtH8CLGQg It seems from that discussion that they were associated with Vladimir Voevodsky's proposal for HTS. As a form of extensional type theory without any "built-in" implementation proposal, it seems like HTS has no notion of "proof object" in Jon's sense, which seems to be formal, checkable proofs. It's not that you couldn't come up with one, it just isn't specified. So I don't think HTS has any "definitional equality", in Jon's sense. But it seems like HTS' exact equality was considered substitutive nonetheless. In fact, it seems to me like what Vladimir meant by "substitutional" was that it doesn't cause coercions. Either because it's definitional, or because it's subsumptive (my term, from another message in this thread). So I think you're misusing those terms. Judgmental, definitional, substitutive, and computational equalities > are not exactly the same thing. But the fact that there are so many > different but related points of view on similar and overlapping > concepts, and so many different but related uses and applications for > them, suggests to me that there is an important underlying > mathematical concept that should not lightly be discarded. > This is too vague. I wouldn't know whether I'm discarding it or not. You seem to be downplaying the differences between these notions. Why? If you don't care about the difference, why don't you just deal with strict or exact equality, and leave the implementation details to someone else? Coherence issues don't penetrate to a lower level than strict equality. Judgmental, definitional, and substitutive equality are special cases of strict equality that differ in their implementation properties. -- 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_1241_1086510789.1549887471275 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Saturday, February 9, 2019 at 3:34:22 PM UTC-5, Michael= Shulman wrote:
From an impleme= ntation point of view, I agree that in the long run we
should have proof assistants that don't hardcode a fixed set of
judgmental equalities. =C2=A0But I don't think that means eliminati= ng all
judgmental equalities; it just means making the logical framework more
flexible, such as Agda's ability to postulate new reductions or
Andromeda's framework with equality reflection. =C2=A0In particular= , the
new equalities that we postulate should still be *substitutive* (as
Jon says, allowing to perturb a judgment without altering the proof
object) rather than *transportive* (requiring the proof object to be
altered) -- I think Vladimir was the one who suggested words like
those.

I first heard those terms was on this list:=
https://groups.google.com/forum/#!topic/homotopytypetheory/1bUtH8CLGQg<= br>
It seems from that discussion that they were associated with Vladimi= r Voevodsky's proposal for HTS. As a form of extensional type theory wi= thout any "built-in" implementation proposal, it seems like HTS h= as no notion of "proof object" in Jon's sense, which seems to= be formal, checkable proofs. It's not that you couldn't come up wi= th one, it just isn't specified. So I don't think HTS has any "= ;definitional equality", in Jon's sense. But it seems like HTS'= ; exact equality was considered substitutive nonetheless. In fact, it seems= to me like what Vladimir meant by "substitutional" was that it d= oesn't cause coercions. Either because it's definitional, or becaus= e it's subsumptive (my term, from another message in this thread).
<= br>So I think you're misusing those terms.

Judgmental, definitional, substitutive, and c= omputational equalities
are not exactly the same thing. =C2=A0But the fact that there are so ma= ny
different but related points of view on similar and overlapping
concepts, and so many different but related uses and applications for
them, suggests to me that there is an important underlying
mathematical concept that should not lightly be discarded.

This is too vague. I wouldn't know whether I'm discard= ing it or not. You seem to be downplaying the differences between these not= ions. Why? If you don't care about the difference, why don't you ju= st deal with strict or exact equality, and leave the implementation details= to someone else? Coherence issues don't penetrate to a lower level tha= n strict equality. Judgmental, definitional, and substitutive equality are = special cases of strict equality that differ in their implementation proper= ties.

--
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_1241_1086510789.1549887471275-- ------=_Part_1240_691413597.1549887471275--