From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.67.3.138 with SMTP id bw10mr34273309pad.16.1468946949038; Tue, 19 Jul 2016 09:49:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.86.202 with SMTP id o193ls3177424itb.19.gmail; Tue, 19 Jul 2016 09:49:08 -0700 (PDT) X-Received: by 10.107.4.69 with SMTP id 66mr7248602ioe.17.1468946947983; Tue, 19 Jul 2016 09:49:07 -0700 (PDT) Return-Path: Received: from out5-smtp.messagingengine.com (out5-smtp.messagingengine.com. [66.111.4.29]) by gmr-mx.google.com with ESMTPS id t206si2061511ywb.3.2016.07.19.09.49.07 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Jul 2016 09:49:07 -0700 (PDT) Received-SPF: neutral (google.com: 66.111.4.29 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) client-ip=66.111.4.29; Authentication-Results: gmr-mx.google.com; dkim=pass head...@messagingengine.com; spf=neutral (google.com: 66.111.4.29 is neither permitted nor denied by best guess record for domain of j...@jonmsterling.com) smtp.mailfrom=j...@jonmsterling.com Received: from compute4.internal (compute4.nyi.internal [10.202.2.44]) by mailout.nyi.internal (Postfix) with ESMTP id 9195220692 for ; Tue, 19 Jul 2016 12:49:07 -0400 (EDT) Received: from web4 ([10.202.2.214]) by compute4.internal (MEProxy); Tue, 19 Jul 2016 12:49:07 -0400 DKIM-Signature: v=1; a=rsa-sha1; c=relaxed/relaxed; d= messagingengine.com; h=content-transfer-encoding:content-type :date:from:in-reply-to:message-id:mime-version:references :subject:to:x-sasl-enc:x-sasl-enc; s=smtpout; bh=RAq+qQGlU4jZU21 L0M23viR4/+A=; b=ZKf2Py5ElqbYtZJfl6EylJ3+XRvfCChf5AThXDl8kOPLYmO yLO1fPzu2Y8oRzGhSTyoUyNYxxfAC6Bun4WyVyQQZtJdKZkH3Qlu744j8Zl+Qv/2 Zd0XT2JO7PScctXPa7fM3ZqIzqd7BRp3h0M9B1CoW1M/IprrEmDlqpZoSSMs= Received: by mailuser.nyi.internal (Postfix, from userid 99) id 5DDFCCC6D4; Tue, 19 Jul 2016 12:49:07 -0400 (EDT) Message-Id: <1468946947.2314129.670766785.49572383@webmail.messagingengine.com> X-Sasl-Enc: 6+BVl/cINR1HHxrwMVNsGOUlisyrl8djXGwHqm4tH9N9 1468946947 From: Jon Sterling To: HomotopyTypeTheory@googlegroups.com MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" X-Mailer: MessagingEngine.com Webmail Interface - ajax-6fae4dd4 Subject: Re: [HoTT] Different notions of equality; terminology Date: Tue, 19 Jul 2016 09:49:07 -0700 In-Reply-To: References: Hi Mike, I liked your message below! I am essentially in agreement with most of your remarks. Let me begin by saying, I think we should call "propositional/typeal" equality "internal equality", since the whole point is that it consists in the internalization of a judgment as a proposition/type=E2=80=94and the evidence of the judgment corresponds to th= e truth of the proposition/type. On Tue, Jul 19, 2016, at 05:53 AM, Michael Shulman wrote: > My apologies to everyone (except Andrew), who saw his replies to my > messages without the originals. The problem was an email issue on my > end. Below I summarize the content of my messages; this will be my > last email on the subject. >=20 > ~~ >=20 > I have been advocating the term "typal equality" for what used to be > called "propositional". It is less awkward than "type-level" or > "type-theoretic", and conveys exactly what is meant, namely that the > statement of equality *is a type*. I prefer it to "logical equality" > because traditionally, "logic" has often referred only to the type > theory of mere propositions, so "logical equality" has something of > the same problem as "propositional equality". In the programming languages field, we use "logical equivalence" to refer to a type directed extensional equality, for what it's worth. >=20 > For the reasons given by Andrew, in most cases it suffices to simply > say "equality". It only occasionally happens that we need to > disambiguate what kind of equality we are talking about, and in that > case I think it better to use a word that conveys *exactly* what the > distinction is, rather than any historical or opinionable gloss on > that distinction. (If this is "logical" equality, is the other one > "illogical"?) Typal equality is indeed related to other kinds of > equality that existed before type theory, but inside of type theory, > what distinguishes it is precisely that it is a type (and inside of > type theory, "predicate/formula/thing-you-can-prove-or-inhabit" is > just a long-winded way of saying "type"). Now, in response to this, Andrew has said:=20 > The distinction is that it is the equality predicate/formula/thing-you-ca= n-prove-or-inhabit. If this was intended to mean that the propositional/"typal"/internal equality is the one you can inhabit/prove, whereas the judgmental equality holds or fails to hold on its own (i.e. is not susceptible to mathematical argument), I must disagree. The notion of a "judgment" is very broad and very old, and in general, a judgment may become evident by virtue of a non-trivial proof; see Martin-L=C3=B6f's paper "Analytic and Synthetic Judgment in Type Theory". So, we can say with confidence that the distinction is not that it is a thing which you can prove=E2=80=94since that is in fact the same for judgme= nts and for types. The difference is just the level at which this object lives... >=20 > For the same reasons, I prefer "judgmental equality" because it > conveys exactly what is meant in that case, namely that the statement > of equality *is a judgment*. Maybe it doesn't have to be formulated > as a judgment, but as far as I know in all cases it can our could be > so, without changing the type theory materially. >=20 > This possible slight inaccuracy seems to me to be preferable to the > more serious problem with "definitional equality", namely that such a > statement of equality is certainly not always a definition. For > instance, in type theory with a reflection rule from typal equality to > judgmental, there is no sense in which a judgmental equality obtained > by that rule is a "definition" of one side in terms of the other. > Associativity of addition of natural numbers is not true "by > definition" unless you are willing to redefine the word "definition". Excellent remark about "judgmental equality" and "definitional equality". I also think "judgmental" is the correct term to use in general, and I would go even further as to say that there is no "slight inaccuracy" to worry about; that is, people often have this idea that untyped conversion (for instance) is not "judgmental", but whether something is typed or not is irrelevant to whether it is a judgment. Untyped conversion is still a judgment, and if you use it as equality, it is the judgmental equality for your language. [Now, contrary to remarks made on this list, Agda's underlying type theory (regardless of its implementation, which I know less about) has the full type-directed judgmental equality=E2=80=94what I recall from what = Peter Dybjer mentioned last year is that Agda is based on an extension of Martin-L=C3=B6f's Logical Framework, which is described in detail in Nordstr=C3=B6m et al's "Programming in Martin-L=C3=B6f's Type Theory"; now,= to my knowledge, Coq's equality judgment is based on untyped conversion, but this does not mean it lacks an equality judgment.] So, what's the place for "definitional equality"? In Per Martin-L=C3=B6f's Bibliopolis book (Intuitionistic Type Theory, from lectures given in Padua, 1980), he explains that definitional equality is *only* syntactic equality modulo alpha-equivalence & definitional extension (replacing left-hand-side with right-hand-side)=E2=80=94i.e. equality of "sense". A careful reader will note that definitional equality is also of course a judgment, so in some sense it is technically a form of judgmental equality; and in a theory like the Canonical Logical Framework developed by Watkins et al, it is the only possible form of judgmental equality. By convention, we do tend to use the term "judgmental equality" specifically for some type-directed thing that is a bit coarser than syntactic equality, but I don't think that's really essential=E2=80=94it ju= st depends on the theory, and sometimes one equality *judgment* is singled out as "the judgmental equality", and other finer-grained "equality" judgments get called something else=E2=80=A6 There is little rhyme or reaso= n to it, and I think that's OK. In my mind, the term "judgmental equality" only serves to contrast it with an *internal* notion of equality (what has been called propositional equality, or typal equality, etc.). The term "judgmental" just specifies at what level/layer of the theory it is happening. Best, Jon >=20 > --=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 > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.