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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qt1-x83b.google.com (mail-qt1-x83b.google.com [IPv6:2607:f8b0:4864:20::83b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3a3824fc for ; Sat, 9 Feb 2019 14:44:40 +0000 (UTC) Received: by mail-qt1-x83b.google.com with SMTP id q33sf6804163qte.23 for ; Sat, 09 Feb 2019 06:44:40 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1549723479; cv=pass; d=google.com; s=arc-20160816; b=Cugeelg/Ags7FEW8P/J2FzP1mRQaayfs5KARSnjVxN22pwQ88GIwsiTPl7qOUCDtsN kHvy6y1iAsdHNXahoqhZe4eiS2d3596eb0TkAzLxnHJMV2LAE9xMPzbCN3z2OuUaevZ6 bWUXaVncFK8Dv7+oLdDfwwtpTVDvRIdx3x4s3FUQdkBZC9oONt5x2XuxA9neL4GbveBO 4rwylw4bBXFu1yOE20uOkfPmlrkUFDqVqEj3CopfVCPcWTCaJdrQ+pSlyQr4ymk/AFrx Rl2ChU1N4i2x8FR1fgaj5+4SWTc4FmFLnUOFOjr+RWJ122HX5ZrzKJmcgDEOucbb5LPA HUpw== 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:content-transfer-encoding:subject:to:from :date:references:in-reply-to:message-id:user-agent:mime-version :sender:dkim-signature; bh=K9ItQQ5PzS8g8DexGqGwNMoKzSgRf6uEHZ+ThOR+w3M=; b=vvBmGEP6y36ei2FH4dLwYCbPPpN/XsHyGcfcWNoVBWulffDqBF8AWDxU+ZROdCtj0E 6SfeLlW7kG1scL6KWZYhk56fYrQ4UVA1gzWlHanv3NmT+6zhsSwd5nIM95MNZHsWZGJq wjjZMqc7eOa7nED5BzoSGNmiHj+6HPDqpCrPPsSHJp9L9ivj/IJTMTIWPVOcjXbMHf8/ LQKXkWpM6xjA1b0hlqntn1OIHGzb/7c/OG3jSV1iwfzL8Y9ulyU+yG0v9U2EeMyalVb2 I6Vq6LOEzbXyRCFnMudOEve+szWjMOWMbbai5s6xSi9gZB39uu2Mm+wa49rByZeUoOJn oQ/Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=q1mEFqas; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:user-agent:message-id:in-reply-to:references :date:from:to:subject:x-original-sender :x-original-authentication-results:content-transfer-encoding :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=K9ItQQ5PzS8g8DexGqGwNMoKzSgRf6uEHZ+ThOR+w3M=; b=HgOMEKq+MuqHVxTRGMeUWPx3rSJwxTkHiulOCaZzb4uZrnAPJ7RzlvwNgVpMhhXAP6 LDZjh78Xq8lFr2kqPNo8rArz2r35TF+jpkipbwplE9y9E7BxLUHXYLZt1WW8I/qtDRe7 zomDyZ2FGPiraym9a5oJIIJc27KTCFSp4Y9khN5jJtNS+C7nj+1eaaFrB+oYNMDW4U8x Z2MmfQBJa5cxGy4si3x3gzmCZn3fgOp4czbITmPByqV8goPMnhaoYWTI0X4tbmTp9cvX UoRxo9Z9BnQL4hysCt4mg6KcceW0fe+AwHoTGst946HPXFSsHw9b1SwC+/RsE2tROuG+ g7Jg== 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:user-agent:message-id :in-reply-to:references:date:from:to:subject:x-original-sender :x-original-authentication-results:content-transfer-encoding :precedence:mailing-list:list-id:x-spam-checked-in-group:list-post :list-help:list-archive:list-unsubscribe; bh=K9ItQQ5PzS8g8DexGqGwNMoKzSgRf6uEHZ+ThOR+w3M=; b=WJRfXTyyzZzi7HZfFbnRp2Ogp5+pB2Ppo1lDcULvW7lyVmjlVjqQfNnRo10nIhjMOr V+3znA7M9ncIzkUbC36gf/Hqt31SgKqvIOEL72cvfttRczNgJs29xxykYxbERnOcM/20 ecvQknqilvtpiqA957/xSUkV9eHmRw2/OQ3ZbaeleqURaamcJzV4oyVUjivSAqT6fxZf evvo6EafpixSDqM0p8/3c9rMfTK3zKhC7E68qy3nsg+S/35rNc6Ywe9o8t5+rdz2N1wV bDcPLoQ/yxty70lgTgpTEJfITSigQunqOrA16hkKwwHoVrfBSxScQc9h+sJCTCU9tSYF 9fQA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AHQUAuaSdppvPRtefeUEKmwciIV9YTkORN07m9kxV2zbaqKlNlVHqXDG 9YXe/gcu4Q4fyTwKmkQDKKg= X-Google-Smtp-Source: AHgI3IaC9pWhaVR9P64IrvsEJax8XvQbHG4nM0llbbalP/Rxmi0zmG0/228223hXOOd5SGKUbaVReA== X-Received: by 2002:a0c:8b4c:: with SMTP id d12mr289301qvc.3.1549723479274; Sat, 09 Feb 2019 06:44:39 -0800 (PST) MIME-Version: 1.0 X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:b043:: with SMTP id l3ls4233483qvc.6.gmail; Sat, 09 Feb 2019 06:44:38 -0800 (PST) X-Received: by 2002:a0c:c288:: with SMTP id b8mr3925067qvi.20.1549723478953; Sat, 09 Feb 2019 06:44:38 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1549723478; cv=none; d=google.com; s=arc-20160816; b=toSQErpz+HHzQJinLcSve2B53Cn3lQcwE3YB1D/4MLhu/M/Dwg693XpXbk1cGL66GY y14UKStOw2icsnMZdRVCwIWL94wCJ7UgmIQKdcvO92RYHeF7SJAewFvy37yPYfGbdYLT UH9fjqzvSZOs7M/8S7XRQFXXY/qJMTPO2QEfLtByuR0UVK1NO7MlQatp/hH95cDHJxzg 2BqtiSLUjIBWvZdsCbkXqKaobM13fdy1N0Mc1qB096Y5gnQPg7KUqInyN+34wCFY5uaX GxJdo5jq3FpF8QW3iM+jPMbPyHEui64pxPQKdFlL9nohfVe9q6ISchsTnKJB4utw6fjc RorQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=subject:to:from:date:references:in-reply-to:message-id:user-agent :dkim-signature; bh=y54KsbbF9fSEOkwvNIic8tUnoBSjMfkO7Z3PBE6w9EQ=; b=H2gUDC5kBod6OjgNCYO6LyOy5OJV16Cowq3im0+rXjt6hGcy6Br/aW4qtlY18zzeZs ZQJs2+yjblzLPgPkdbS1/LFuQ/3xAtt04Tc8zd6yfh4I7yTIAeUFmyjfU7vVVJcbbhqG NjuJxDVxaqXWyqenKfBD4hENwT8ilduP9PNcQBq0KT7191+DTXXII38WOcLvrpKjlY8S Nsir+hT95Pd4r6zl/4Halqibs4UH7a+IfXWjio2c+gNqciJUvKEspwEGwJtma8oKJKAH RL7ZPboG3SoaAjBkQA2cOO4v4zHceqDMIcLKdvzjjT75G76/jKT79Spl/NLw1NMN+MoO FKfg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=q1mEFqas; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com Received: from out2-smtp.messagingengine.com (out2-smtp.messagingengine.com. [66.111.4.26]) by gmr-mx.google.com with ESMTPS id o22si372067qtm.1.2019.02.09.06.44.38 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 09 Feb 2019 06:44:38 -0800 (PST) Received-SPF: neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) client-ip=66.111.4.26; Received: from compute2.internal (compute2.nyi.internal [10.202.2.42]) by mailout.nyi.internal (Postfix) with ESMTP id 9A90B219DA for ; Sat, 9 Feb 2019 09:44:38 -0500 (EST) Received: from imap3 ([10.202.2.53]) by compute2.internal (MEProxy); Sat, 09 Feb 2019 09:44:38 -0500 X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedtledrleeggdeilecutefuodetggdotefrodftvf curfhrohhfihhlvgemucfhrghsthforghilhdpqfhuthenuceurghilhhouhhtmecufedt tdenucesvcftvggtihhpihgvnhhtshculddquddttddmnegoufhushhpvggtthffohhmrg hinhculdegledmnecujfgurhepofgfkfgjfhffhffvufgtsehttdertderredtnecuhfhr ohhmpedflfhonhcuufhtvghrlhhinhhgfdcuoehjohhnsehjohhnmhhsthgvrhhlihhngh drtghomheqnecuffhomhgrihhnpehgohhoghhlvgdrtghomhenucfrrghrrghmpehmrghi lhhfrhhomhepjhhonhesjhhonhhmshhtvghrlhhinhhgrdgtohhmnecuvehluhhsthgvrh fuihiivgeptd X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id 40DCF7C36C; Sat, 9 Feb 2019 09:44:38 -0500 (EST) X-Mailer: MessagingEngine.com Webmail Interface User-Agent: Cyrus-JMAP/3.1.5-832-gba113d7-fmstable-20190201v1 X-Me-Personality: 19972253 Message-Id: <2b86e469-309d-4a7a-8ad0-d7a0cb376c74@www.fastmail.com> In-Reply-To: References: Date: Sat, 09 Feb 2019 09:44:37 -0500 From: "Jon Sterling" To: "'Martin Escardo' via Homotopy Type Theory" Subject: Re: [HoTT] Re: Why do we need judgmental equality? Content-Type: text/plain; charset="UTF-8" X-Original-Sender: jon@jonmsterling.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@messagingengine.com header.s=fm2 header.b=q1mEFqas; spf=neutral (google.com: 66.111.4.26 is neither permitted nor denied by best guess record for domain of jon@jonmsterling.com) smtp.mailfrom=jon@jonmsterling.com Content-Transfer-Encoding: quoted-printable 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: , Hi all, I think there's two different issues being conflated -- there is the questi= on of whether definitional equalities can be removed, in order to obtain mo= re direct interpretation into weaker models, and then there is the question= of whether definitional equalities can be removed as a way to make a proof= assistant more modular, exploiting conservativity results locally to add d= efintional equalities. The first seems more interesting to me, and is indeed the topic of Curien's= famous paper. Many interesting coherence theorems lurk underneath the defi= nitional equalities that we take for granted, and we can only see them if w= e treat definitional equalities as defeasible. The issue about proof assistants seems quite different to me -- the approac= h that seems to be proposed by some of the people in the room, to replace j= udgmental equality with a good enough equality *type* seems perfectly good = for studying algebra and models (for instance, the discipline of QIITs in t= he presence of [semantically] extensional equality types seems like a good = tool for dependently-sorted algebraic theories). But this approach is not l= ikely to yield *proof assistants* that are more usable than existing system= s which have replaced definitional equality with propositional equality. I am referring to Nuprl -- usually Nuprl is characterized as using equality= reflection, but this is not totally accurate (though there is a sense in w= hich it is true). When I say "definitional equality" for a formalism, what = I mean is that if I have a proof object D of a judgment J, if J is definiti= onally equal to J', then D is also already a proof of J'. Definitional equa= lity is the silent equality. In most formalisms, definitional equality incl= udes some combination of alpha/beta/eta/xi, but in Nuprl is included ONLY a= lpha. What I mean is that in a proof object for Nuprl, the biggest relation= by which you can "purturb" a judgment without needing to update the proof = object is alpha equivalence. Proof objects must NOT be confused with realiz= ers, of course -- just like we do not confuse Coq proofs with the OCaml cod= e that they could be extract to. So how does Nuprl work? "Real" equality is captured purely using the equali= ty type, and not using any judgment except membership in the equality type = (a judgment whose derivations are crucially taken only up to alpha, rather = than up to beta/eta/xi). When you want to reason using beta/eta/xi (and the= much richer equations that are also available), you use the equality type = and its elimination rules directly, essentially in the same way that Thorst= en has advocated. Nuprl is in essence what it looks like to remove all definitional equalitie= s and replace them with internal equalities. The main difference between Nu= prl and Thorsten's proposal is that Nuprl's underlying objects are untyped = -- but that is not an essential part of the idea. The reason I bring this up is that the question of whether such an idea can= be made usable, namely using a formalism with only alpha equivalence regar= ded silently/definitionally, and all other equations mediated through the e= quality type, can be essentially reduced to the question of whether Nuprl i= s practical and usable, or whether it is possible to implement a version of= that idea which is practical and usable. As many of the people on this list are aware, in the years past I was very = bullish on this idea, but now after having implemented two separate proof a= ssistants based on this idea, I am not as optimistic about it as I was (but= I don't rule it out). Today, I have changed my methodology and embraced st= rong definitional equality, in order to achieve my actual goals during the = very finite historical period of my PhD -- to build usable proof assistants= for formalizing mathematics. Best, Jon On Sat, Feb 9, 2019, at 9:05 AM, Nicolai Kraus wrote: > On Sat, Feb 9, 2019 at 11:53 AM Felix Rech wrote: > > One of the motivations for my question was that I actually expect usabi= lity benefits if one worked in a dependent type theory without judgmental e= quality that has good support by a proof assistant. >=20 > Yes, me too (but I think *a lot* of work needs to be done before we can= =20 > have a proof assistant based on this idea which provides better=20 > usability than the current ones). > I agree with your points. But I think "x + 0 =3D x versus 0 + x =3D x" is= =20 > an example where I'd expect that one should be able to produce a=20 > conservativity proof and use both at the same time instead of choosing=20 > one. I think it's not necessary that we restrict ourselves to=20 > computation rules that come from actual definitions; anything that is=20 > "constructively conservative" over a weak theory should be allowed. In=20 > Agda, one can have additional computation rules, but it's not a safe=20 > feature. > Nicolai >=20 >=20 > > 1. Judgmental equality cannot be taken as assumptions. If one wants to= use judgmental equalities then one has to give concrete definitions that s= atisfy 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 arbitrar= y than natural. If we define addition of natural numbers for example then w= e 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 behavior. > > Another motivation was of course that it would simplify the implementat= ion of proof checkers and parts of the metatheory. > >=20 > > I would appreciate any comments on this. > > =20 >=20 >=20 > > --=20 > > You received this message because you are subscribed to the Google Grou= ps "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 > =20 >=20 >=20 > --=20 > You received this message because you are subscribed to the Google=20 > Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send= =20 > 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.