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 b4725d9b for ; Sat, 9 Feb 2019 01:30:34 +0000 (UTC) Received: by mail-wm1-x337.google.com with SMTP id g3sf2127267wmf.1 for ; Fri, 08 Feb 2019 17:30:34 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549675833; cv=pass; d=google.com; s=arc-20160816; b=plB9yyU+9qCZDhLvlttdhwHKc6DQdgEWIwpamYZh6cjj7cIBX35NcBQu5WtlVRSz/A aDeUarL3agyaPv0yrp95cglRv7pbnYqIeprgVXvjeeE/mrtFgNfpkXcGKGPpJ3CoxHkw waXlJfUWuK20kAWj2oUNlZW/9C+nlPKGq/oEjJDDLZ/utiphcWMy4eStM6CsgTmQZFKy a2TtbcqgtRanrZa3sKJ8Up7RMD30Mm2NR3g1x1y+KErzx+m1uJI8I8S37X6lAWe7HZ3k u1CLGVNqn17eklNWQAviAFcY33djW13RUQfQVlQUB+XFQ5KN4eYeI3WY5C0kW25eflxw S0JA== 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=LsmXnNr1UzK1wIl8d3Vl+3OwrgYc4VXEAO9UGI9CqvQ=; b=zWHHtdUVU7EQXB8LH2qtxUp1EoaHeRgoCk+hc1rT0tdVpe0KBfiAzfHSDeGUBG17GV E0+POppUCc4lkFrPSZoPNSZU/v3l29hFd7cVdQV+hPIEmFoqlso3NxGkrzHt/EJHQIiK kqzTnFKXrZo2x4FjdeniAJnPcVgW4TPPpQ9bckA+b4cv4oZ9O87zGR/S/8uX+IlPv+nY 9XonK1S7YIJfwMXmvPTwqiavMXqkyN+pHYrvFtx29OCePvDdL3zwFNP5RtGByz8k2PzH u0pvcRA9pF7nM3rvWegy3ABB3LNVJX72rIPbtoakeG3qQaj8DlK7983ggvTmS+UT2O7Z exXw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=WGApsrrk; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::234 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=LsmXnNr1UzK1wIl8d3Vl+3OwrgYc4VXEAO9UGI9CqvQ=; b=IkkFVf7Ngkg3MHAw4RYxndWsCO2QsM7u9tWN3Utq7RgjDEAfPI2aNzXjiWCGefYdsJ 38tF0BhmaXAHzzrIWGt79Hd8r/Qo9xJ+Cqa5LlXVgCqsckUY7olvuj6i2iXuhyrV7k6J y8R26YwZffDxyaj2b/qvYjsxAr6anNnh6dVjZFm8irREY6ifZGgn0+hAu/PKdyTI55Ip SFwiDqRVsmlZetJnglX27xSI1BlzCypAERHn2KF/bEtn1Pbcbu6E3Lkd1Xg/gI35mLgj xcMx4YOojqwwAu2yHJ1uiY08drlF43JhXFIASjOzwHbhwYtv3r/PpXrVkKB6LoVm/rZM RBbQ== 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=LsmXnNr1UzK1wIl8d3Vl+3OwrgYc4VXEAO9UGI9CqvQ=; b=kYL4HCSPq6+QIXDj5vp2oMeoNoNtibhkc4hQPpqUWV2lSjBBoTUcEwNowI0Hq+7HcX XCWpMyXEyIUclEiBipP3MpJKOnaE8hZIxT591Cq4oJNGhFvtf0yrKWdDm5AGRZUPAAe9 Kw/p1ehm9ExYOz20kIVgPPMsmOLya9g8fK6AV0oMux74ID1RUAF1Vi1bit+FRX9V4pj3 7jAkLAHfdb17hWiX9C1gPTH5z9pVRU7WVf+xEIHo/hqyPdUxwsqfT640C+P4KnpUtf3b zh/N2r9lE/88BcJXZl/AJQz6vy3ZEJvRSa6fyAc1QLBDIJ3n9dXajINwoJoKZF45uN1w 6VkQ== 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=LsmXnNr1UzK1wIl8d3Vl+3OwrgYc4VXEAO9UGI9CqvQ=; b=pdqeaaBGWqLstTRs3l/8KotsbPdWp67DV4wdN3fVhLu5pxbnG9E2RmqpEKMt6blMgM p2Ma9OLocfXsJ0rKbGiM/zXvm93bI3uj6g+Dkx9BRIv4Ms07MP0x8a4JvQ0ClT4NDt7A HEGZY/6MbZznp6MHY8fnqNwZYrqeTaKjJV30szJ34JlgDaUNdRusFfC2vnaD3xWn+Yz8 ElbzqVAA/FLSASWUKtAoUrEj4swttCmIKy2hbhkmIMCD+BRd4yDfiGr0ED7cX45CzkpJ dTWRw4na0PQkpnYBmr4c433MGKKtz/1Q9C5DV7FriHrKLDUQufdpfd3rmq5HRtqO7nrd /csw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuY3PmEERgu9OZ4T6hb2VyG45i9NV4AS3F0NXAlE5/csRJ0TBa6Q /L9igNq3AQNZva66r8OGYvg= X-Google-Smtp-Source: AHgI3IazujtiUt4wTcbRBJJEmmnAO47sX8rUmZ+Twiec2mdsfjm/7iHAlQXf/cfZc2Q6YtdJuPq1nA== X-Received: by 2002:a1c:2dca:: with SMTP id t193mr10269wmt.2.1549675833016; Fri, 08 Feb 2019 17:30:33 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:b6d4:: with SMTP id g203ls935550wmf.8.canary-gmail; Fri, 08 Feb 2019 17:30:31 -0800 (PST) X-Received: by 2002:a1c:658a:: with SMTP id z132mr72435wmb.25.1549675831647; Fri, 08 Feb 2019 17:30:31 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549675831; cv=none; d=google.com; s=arc-20160816; b=S9He5YK7hq5b/z9DcvP7GhP6z7dFfNWoOtDaz6yYmDpcfE1+EJCmar7HYitA6on2KQ 0oPz2ZTCEnq2LbKIoIfLIf8cG+gaiKlkyzj9wRWdrLbJu6cLS9RwUyEYTXxvLr2lVPY/ UUX+DzfLLHfTLiRXYrZ0VagZsSvp9C0j6YNbk8qDOS9+2AzTKZ+esUjlKvw8HcZSrTV4 OJ2S//WKh73iupx7mzQtKFc6XGbtfdAqO1s8nyvGWJI2j2KTYYYNvFTiIBibih+i+sg/ LdPmZ9US9+3W1vX3fe7PriOIp+rTp7WnpSRvr5Nso+TD4bRDOhdZzJ28OGGiK/myeibs bsMg== 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=m1sBvkb9OYsF5RJvPCTbIoU/KMP0en5ubA80t78RQyk=; b=NV/ymQYv0zesH3HgiN59p0hBLoCD3HO155gqF8c8upKkkaXjtYjOIun4f9NFsR99I2 RZBkH8q15GfTh1pfoeG3ZMUlqIyCJ/MmsWVCLng82123rNz695idRx6qupi8cHpq0giq GBYFVZmgeYYLDUyksI2j1STK65XgsXuTxPaUFrA04AkVaU3b4tZJj6pGj5QKB9xq1mqy JCWx47/Ry1k4DH4Yc/L6hp2GMOgyQRpyQySxNnJBvHjDivOgfUkDwVZmdikllJx50Qeu 5avYrjoPaZ21deu2FaYz/xYw5TbJXyU/uBueQ3bg0CQJs0mXQCc9tEvnSDC5wf2UpOij dlxQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=WGApsrrk; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::234 as permitted sender) smtp.mailfrom=nicolai.kraus@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lj1-x234.google.com (mail-lj1-x234.google.com. [2a00:1450:4864:20::234]) by gmr-mx.google.com with ESMTPS id 64si187002wma.1.2019.02.08.17.30.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 08 Feb 2019 17:30:31 -0800 (PST) Received-SPF: pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::234 as permitted sender) client-ip=2a00:1450:4864:20::234; Received: by mail-lj1-x234.google.com with SMTP id l15-v6so4518160lja.9 for ; Fri, 08 Feb 2019 17:30:31 -0800 (PST) X-Received: by 2002:a2e:9786:: with SMTP id y6-v6mr3458416lji.53.1549675830809; Fri, 08 Feb 2019 17:30:30 -0800 (PST) MIME-Version: 1.0 References: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> In-Reply-To: <1a3dfba4-816a-42c3-8eea-1a2906cb1cad@googlegroups.com> From: Nicolai Kraus Date: Sat, 9 Feb 2019 01:30:19 +0000 Message-ID: Subject: Re: [HoTT] Re: Why do we need judgmental equality? To: =?UTF-8?B?TWFydMOtbiBIw7Z0emVsIEVzY2FyZMOz?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000069a0ee05816c05ef" 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=WGApsrrk; spf=pass (google.com: domain of nicolai.kraus@gmail.com designates 2a00:1450:4864:20::234 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: , --00000000000069a0ee05816c05ef Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable I agree with everything Martin said below, but I want to go a step further and argue that judgmental equality is potentially holding us back, in terms of meta-theoretical results AND usability of the type theory. I can understand that, for programming, we want built-in computation. However, for a foundational system, I think we should strive for something as minimalistic as possible without arbitrary additional features. It might be a bit controversial to call judgmental equality an "arbitrary additional feature", but there is certainly some arbitrariness involved (why else would Sigma have judgmental eta in some systems and not in others?). It seems to me that the cleanest, most minimalistic, and most canonical choice would be a type theory without judgmental equalities *at all*. This would also be much more in line with the approach of category theory, and I expect that it could make the lives of those of us working with models easier. Is there a deep theoretical reason for the necessity of judgmental equality? Of course, we want convenience and usability. I just fail to see why this means that judgmental equality has to be a built-in thing (one could say: why does it have to be part of the core). It's possible that, if we do *not* insist on built-in judgmental equality, we could even get *more* convenience. What I mean is this: Let's write WTT for a "weak type theory" without any judgmental equalities (since we're doing HoTT, maybe with some axioms such as univalence, but let's not specify this here). Let's say we know that a certain set A of judgmental equalities does not change WTT, i.e. that (WTT+A) is a conservative extension of WTT (conservative in a constructive sense). We could now have a proof assistant which uses WTT as core but which allows us to "load" the conservativity proof of A. Then, at the beginning of a module, a user can tell the proof assistant that in this module, they pretend that the type theory is (WTT+A); i.e. for the user, it looks as if they are working in (WTT+A) but, in the background, the proof assistant translates everything to WTT. In another module, the user can pretend they are working in (WTT+B) instead, if (WTT+B) is conservative over WTT as well. The idea here is that some proofs benefit more from one set of judgmental equalities, while other proofs benefit more from others. Being able to choose which equalities one wants could lead to increased convenience. (I think WTT+A+B is not necessarily conservative over WTT, so we cannot just always assume all equalities for maximum convenience.) For example, let's consider a cubical type theory. I'm aware that we don't really know many conservativity properties of cubical type theories yet, but I would be interested in knowing some. Maybe some cubical type theory gives us a set C which our WTT-based proof assistant can load. In other words, instead of saying "hey, we have found a new cubical type theory with amazing computational behaviour, an implementation is on GitHub", people could say "hey, we have found a new set of judgmental equalities, on GitHub is the conservativity proof that you can load into your proof assistant to use it". I don't think this is something that we will manage to get anytime soon, and I find it very difficult in general to find conservativity results, but is there a theoretical reason which makes this impossible? Nicolai On Fri, Feb 8, 2019 at 9:19 PM Mart=C3=ADn H=C3=B6tzel Escard=C3=B3 < escardo.martin@gmail.com> wrote: > I would also like to know an answer to this question. It is true that > dependent type theories have been designed using definitional equality. > > But why would anybody say that there is a *need* for that? Is it > impossible to define a sensible dependent type theory (say for the purpos= e > of serving as a foundation for univalent mathematics) that doesn't mentio= n > anything like definitional equality? If not, why not? And notice that I a= m > not talking about *usability* of a proof assistant such as the *existing* > ones (say Coq, Agda, Lean) were definitional equalities to be removed. I > don't care if such hypothetical proof assistants would be impossibly > difficult to use for a dependent type theory lacking definitional > equalities (if such a thing exists). > > The question asked by Felix is a very sensible one: why is it claimed tha= t > definitional equalities are essential to dependent type theories? > > (I do understand that they are used to compute, and so if you are > interested in constructive mathematics (like I am) then they are useful. > But, again, in principle we can think of a dependent type theory with no > definitional equalities and instead an existence property like e.g. in > Lambek and Scott's "introduction to higher-order categorical logic". And > like was discussed in a relatively recent message by Thierry Coquand in > this list,) > > Martin > > > On Wednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote: >> >> In section 1.1 of the HoTT book it says "In type theory there is also a >> need for an equality judgment." Currently it seems to me like one could,= in >> principle, replace substitution along judgmental equality with explicit >> transports if one added a few sensible rules to the type theory. Is ther= e a >> fundamental reason why the equality judgment is still necessary? >> >> Thanks, >> Felix Rech >> > -- > 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. > --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --00000000000069a0ee05816c05ef Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
I agree with everything Martin said = below, but I want to go a step further and argue that judgmental equality i= s potentially holding us back, in terms of meta-theoretical results AND usa= bility of the type theory.

I can understand that, = for programming, we want built-in computation. However, for a foundational = system, I think we should strive for something as minimalistic as possible = without arbitrary additional features.=C2=A0

It mi= ght be a bit controversial to call judgmental equality an "arbitrary a= dditional feature", but there is certainly some arbitrariness involved= (why else would Sigma have judgmental eta in some systems and not in other= s?). It seems to me that the cleanest, most minimalistic, and most canonica= l choice would be a type theory without judgmental equalities *at all*. Thi= s would also be much more in line with the approach of category theory, and= I expect that it could make the lives of those of us working with models e= asier. Is there a deep theoretical reason for the necessity of judgmental e= quality?

Of course, we want convenience and usabil= ity. I just fail to see why this means that judgmental equality has to be a= built-in thing (one could say: why does it have to be part of the core). I= t's possible that, if we do *not* insist on built-in judgmental equalit= y, we could even get *more* convenience. What I mean is this: Let's wri= te WTT for a "weak type theory" without any judgmental equalities= (since we're doing HoTT, maybe with some axioms such as univalence, bu= t let's not specify this here). Let's say we know that a certain se= t A of judgmental equalities does not change WTT, i.e. that (WTT+A) is a co= nservative extension of WTT (conservative in a constructive sense). We coul= d now have a proof assistant which uses WTT as core but which allows us to = "load" the conservativity proof of A. Then, at the beginning of a= module, a user can tell the proof assistant that in this module, they pret= end that the type theory is (WTT+A); i.e. for the user, it looks as if they= are working in (WTT+A) but, in the background, the proof assistant transla= tes everything to WTT. In another module, the user can pretend they are wor= king in (WTT+B) instead, if (WTT+B) is conservative over WTT as well. The i= dea here is that some proofs benefit more from one set of judgmental equali= ties, while other proofs benefit more from others. Being able to choose whi= ch equalities one wants could lead to increased convenience. (I think WTT+A= +B is not necessarily conservative over WTT, so we cannot just always assum= e all equalities for maximum convenience.)

For exa= mple, let's consider a cubical type theory. I'm aware that we don&#= 39;t really know many conservativity properties of cubical type theories ye= t, but I would be interested in knowing some. Maybe some cubical type theor= y gives us a set C which our WTT-based proof assistant can load. In other w= ords, instead of saying "hey, we have found a new cubical type theory = with amazing computational behaviour, an implementation is on GitHub",= people could say "hey, we have found a new set of judgmental equaliti= es, on GitHub is the conservativity proof that you can load into your proof= assistant to use it".

I don't think this= is something that we will manage to get anytime soon, and I find it very d= ifficult in general to find conservativity results, but is there a theoreti= cal reason which makes this impossible?

Nicolai


On Fri, Feb 8, 2019 at 9:19 PM Mart=C3=ADn H=C3=B6t= zel Escard=C3=B3 <escardo.ma= rtin@gmail.com> wrote:
I would also like to know an answer to this = question. It is true that dependent type theories have been designed using = definitional equality.

But why would anybody say that th= ere is a *need* for that? Is it impossible to define a sensible dependent t= ype theory (say for the purpose of serving as a foundation for univalent ma= thematics) that doesn't mention anything like definitional equality? If= not, why not? And notice that I am not talking about *usability* of a proo= f assistant such as the *existing* ones (say Coq, Agda, Lean) were definiti= onal equalities to be removed. I don't care if such hypothetical proof = assistants would be impossibly difficult to use for a dependent type theory= lacking definitional equalities (if such a thing exists).

The question asked by Felix is a very sensible one: why is it clai= med that definitional equalities are essential to dependent type theories?<= /div>

(I do understand that they are used to compute, an= d so if you are interested in constructive mathematics (like I am) then the= y are useful. But, again, in principle we can think of a dependent type the= ory with no definitional equalities and instead an existence property like = e.g. in Lambek and Scott's "introduction to higher-order categoric= al logic". And like was discussed in a relatively recent message by Th= ierry Coquand in this list,)

Martin=C2=A0


On Wednesday, 30 January 2019 11:54:07 UTC, Felix Rech wrote:
In sec= tion 1.1 of the HoTT book it says "In type theory there is also a need= for an equality judgment." Currently it seems to me like one could, i= n principle, replace substitution along judgmental equality with explicit t= ransports if one added a few sensible rules to the type theory. Is there a = fundamental reason why the equality judgment is still necessary?
<= div>
Thanks,
Felix Rech

--
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 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.
--00000000000069a0ee05816c05ef--