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-x33a.google.com (mail-ot1-x33a.google.com [IPv6:2607:f8b0:4864:20::33a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2a507a5d for ; Mon, 11 Feb 2019 06:51:32 +0000 (UTC) Received: by mail-ot1-x33a.google.com with SMTP id j23sf10239752otl.6 for ; Sun, 10 Feb 2019 22:51:32 -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=zhqsxgph9jg77TOClGEZsBLMfaMVusML2E1mDV0Z8Z8=; b=bwg+YwWjKOuLnit5YQorOUk9OLfut38l7Y09kTrEogw/Vc5rHqef3TZgJda/PxiGV5 8/454/OrvmROWqSjUFKq8hD5aQOLDFZIPjxn/nIcENcApErI6PhDQtJGifxkMbehY8rM Cswo5PIkgtCG590yU9+Y5lRI3XitJzgN+qlS8SOdncnXGr+WbLd3qk+evNj3n4mLtsxS WjBj5LmQGaXXPNEpwkCOTYaPuodqLO58HeQ2h8trToK0spWfc0OsfUp5xWcvWJauuTBx bbQtaXXpUR0r6Aloy9td47B8wYqWp/VTMmpcupfdfQ2AIAiEMAo0PR043oqi33DZKekj zhQg== 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=zhqsxgph9jg77TOClGEZsBLMfaMVusML2E1mDV0Z8Z8=; b=hsufihiTMtmnZdcgBypKXucKKJ9TTvKYQ12+aY2Ou1QE8NXI83I03mp+C1mmA4wod8 8jhoEGRnA0PKMFAhXQeIyWFqVTFcBadsr34Vc3apBm1oS1EJ4rixYFcCi0QZS8yNeZhD TdzQSlDERls6J/cud3lBsDMxesI6gSJQAEkvMUz8Nf/+x6F3aah7rHDQEcExiFthKYgN ZqQe0p6zjpDLFIoD73/G9dWCz4AQ7xJEwaiNiMeYDF7p5BTu3DPiGIVOK7XcKP1N24T9 kZdo+MyuyJhoB/KZw0qeAMxQmWtPeRTNT63+xfUdPwA9LH1gusnCTsfKXNj9mTmBZ4wk gxAw== 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=zhqsxgph9jg77TOClGEZsBLMfaMVusML2E1mDV0Z8Z8=; b=Fox49GZKQcFDzHAygFpagOck9P+en6TObMrBa6wBB94qMsmmgzcZTE3yuGeRjtMMSi GZPblXPoAho0twV00OaF4oslRhIDUEh6PFKM7AYfhN75tOxSq+hEtHcpsCJh4GtYN5pE gxGEs5FtTB75mL8SNVh6N1EQiYWL+0q6mB3ydGsnTVVnocr68bqlSEY/Ul/sajihYrcD cqfesvrlWdqUuwqohlJpMYmhBBgRsFApqgqyWGYOKbO3/NLRQ6s/YJpG+GurMsNEmKd9 YwmXpFruuGwCu+CKbhGCUuuQ3K9UMiAvMj8Q75hiEuXBmC4LOyTkuhxY1fGQWyXC3Nzg kjJQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuZ+L9pP3ZAimMCxJAm6dBcG4d98xVg4EnqemAP0LRL89E9Zg0d/ 1rlixRhZ6I83MinM/1iYwNQ= X-Google-Smtp-Source: AHgI3IbcsbfvhYwCzlw+Rg8Kl9WJp6Z5WmKLXlQhWbRFL8iU4K/WmzmO/DsqDienzYGdGosRpo73NQ== X-Received: by 2002:a05:6830:1212:: with SMTP id r18mr283498otp.0.1549867890588; Sun, 10 Feb 2019 22:51:30 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:64f:: with SMTP id 73ls1795089otn.10.gmail; Sun, 10 Feb 2019 22:51:30 -0800 (PST) X-Received: by 2002:a05:6830:130d:: with SMTP id p13mr195443otq.2.1549867890240; Sun, 10 Feb 2019 22:51:30 -0800 (PST) Date: Sun, 10 Feb 2019 22:51:29 -0800 (PST) From: Matt Oliveri To: Homotopy Type Theory Message-Id: <0a575642-04bb-4b8a-b0d9-c609f7f125dc@googlegroups.com> In-Reply-To: References: Subject: [HoTT] Re: Why do we need judgmental equality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_244_657912461.1549867889405" 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_244_657912461.1549867889405 Content-Type: multipart/alternative; boundary="----=_Part_245_1707438748.1549867889405" ------=_Part_245_1707438748.1549867889405 Content-Type: text/plain; charset="UTF-8" On Saturday, February 9, 2019 at 6:53:15 AM UTC-5, Felix Rech wrote: > > 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. > I worry that this will indeed be a modularity problem in practice. You generally can't specify behavior strictly at the interface between subsystems. Semantic purists would point out that such an interface wouldn't make sense anyway, unless the subsystem's type is an hset, and you use paths. In general, you should specify a bunch of coherences. Aside from being way harder though, we don't know how to do it in general, because of the infinite object problem. With a 2-level theory, you could at least have second-class module signatures with strict equality. 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. > This problem is solved by the special case of 2-level theories where strict equality is reflective (like extensional type theory (ETT)). What this does for you in practice is that you never have to see coercions between e.g. types (F (x + 0)) and (F (0 + x)), since they can be proven judgmentally equal by induction. (What I mean is that there's no record in terms of rewriting with nat equality. Not that all such reasoning can be done automatically. (It presumably is easy to automate both plus-zero rewrites though.)) Without reflective equality, strict equality doesn't seem to provide any benefit over paths in this case, because you need a coercion, and paths between nats are already unique. -- 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_245_1707438748.1549867889405 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Saturday, February 9, 2019 at 6:53:15 AM UTC-5, Felix R= ech wrote:
Jud= gmental equality cannot be taken as assumptions. If one wants to use judgme= ntal equalities then one has to give concrete definitions that satisfy thos= e equalities and cannot hide the definition details. This makes it impossib= le to change definitions later on without breaking constructions that depen= d on them.

I worry that this will indeed be a mo= dularity problem in practice. You generally can't specify behavior stri= ctly at the interface between subsystems. Semantic purists would point out = that such an interface wouldn't make sense anyway, unless the subsystem= 's type is an hset, and you use paths. In general, you should specify a= bunch of coherences. Aside from being way harder though, we don't know= how to do it in general, because of the infinite object problem.

Wi= th a 2-level theory, you could at least have second-class module signatures= with strict equality.

In nontrivial definitions, judgmental equalities see= m 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 judgment= al equality but we cannot have both. This makes it hard to find the right d= efinitions and to predict their behavior.
Another motivation was of cou= rse that it would simplify the implementation of proof checkers and parts o= f the metatheory.

This problem is solved b= y the special case of 2-level theories where strict equality is reflective = (like extensional type theory (ETT)). What this does for you in practice is= that you never have to see coercions between e.g. types (F (x + 0)) and (F= (0 + x)), since they can be proven judgmentally equal by induction. (What = I mean is that there's no record in terms of rewriting with nat equalit= y. Not that all such reasoning can be done automatically. (It presumably is= easy to automate both plus-zero rewrites though.))

Without reflecti= ve equality, strict equality doesn't seem to provide any benefit over p= aths in this case, because you need a coercion, and paths between nats are = already unique.

--
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_245_1707438748.1549867889405-- ------=_Part_244_657912461.1549867889405--