From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.157.76 with SMTP id u73mr29375062ywg.16.1468982740669; Tue, 19 Jul 2016 19:45:40 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.86.202 with SMTP id o193ls3540150itb.19.gmail; Tue, 19 Jul 2016 19:45:39 -0700 (PDT) X-Received: by 10.66.193.39 with SMTP id hl7mr34340971pac.17.1468982739094; Tue, 19 Jul 2016 19:45:39 -0700 (PDT) Return-Path: Received: from smtp02.srv.cs.cmu.edu (smtp02.srv.cs.cmu.edu. [128.2.217.201]) by gmr-mx.google.com with ESMTPS id w1si29860yww.7.2016.07.19.19.45.38 for (version=TLS1 cipher=AES128-SHA bits=128/128); Tue, 19 Jul 2016 19:45:38 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of d...@cs.cmu.edu designates 128.2.217.201 as permitted sender) client-ip=128.2.217.201; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: best guess record for domain of d...@cs.cmu.edu designates 128.2.217.201 as permitted sender) smtp.mailfrom=d...@cs.cmu.edu Received-SPF: none (cs.cmu.edu: No applicable sender policy available) receiver=smtp02.srv.cs.cmu.edu; identity=mailfrom; envelope-from="d...@cs.cmu.edu"; helo="[172.20.12.22]"; client-ip=24.103.175.196 Received: from [172.20.12.22] (rrcs-24-103-175-196.nys.biz.rr.com [24.103.175.196]) (authenticated bits=0) by smtp02.srv.cs.cmu.edu (8.13.6/8.13.6) with ESMTP id u6K2jV5J020226 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=NO); Tue, 19 Jul 2016 22:45:37 -0400 (EDT) Content-Type: text/plain; charset=windows-1252 Mime-Version: 1.0 (Mac OS X Mail 6.6 \(1510\)) Subject: Re: [HoTT] Different notions of equality; terminology From: Dan Licata In-Reply-To: <1468946947.2314129.670766785.49572383@webmail.messagingengine.com> Date: Tue, 19 Jul 2016 22:45:31 -0400 Cc: HomotopyT...@googlegroups.com Content-Transfer-Encoding: quoted-printable Message-Id: References: <1468946947.2314129.670766785.49572383@webmail.messagingengine.com> To: Jon Sterling X-Mailer: Apple Mail (2.1510) X-Scanned-By: mimedefang-cmuscs on 128.2.217.201 Maybe part of the problem is that we are trying to jam the terminology into= too low-dimensional a feature space? I think there are at least the follo= wing different distinctions: (A) how do you use an equality? I'll use Vladimir's terminology of substit= utional vs transportational for this. =20 (B) is the equality represented by an element of a type, or by a judgement = other than membership in a type? I'll use typal vs judgemental for this, t= hough this is a generalization of what is usually called "judgemental". =20 (C) is the equality "strict"/"exact", or a "path"/"identification"? Of these, I can come up with examples for 6/8 (not (substitutional and path= )): A=3Dsubstitutional, B=3Dtypal, C=3Dexact: the equality type in a computatio= nal type theory or ITT+equality reflection A=3Dsubstitutional, B=3Dtypal, C=3Dpath: doesn't make sense A=3Dsubstitutional, B=3Djudgemental, C=3Dexact: the equality judgement in a= computational type theory A=3Dsubstitutional, B=3Djudgemental, C=3Dpath: doesn't make sense A=3Dtransportational, B=3Dtypal, C=3Dexact: the equality type in the Altenk= irch, McBride, Swierstra observational type theory paper A=3Dtransportational, B=3Dtypal, C=3Dpath: the Id_A(M,N) type in intensiona= l type theory + univalence A=3Dtransportational, B=3Djudgemental, C=3Dexact: rarer, but has come up in= some programming languages work, e.g. "System FC" which is used as an inte= rnal language in the GHC Haskell compiler. here there is a judgement of ty= pe equality that are used as "coercions" but which have no actual runtime e= ffect. another example would be something where you mark uses of (what is = usually called) a "definitional equality" judgement in the terms A=3Dtransportational, B=3Djudgemental, C=3Dpath: a line x:I |- a : A in a c= ubical type theory=20 -Dan On Jul 19, 2016, at 12:49 PM, Jon Sterling wrote: > Hi Mike, >=20 > 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=97and the evidence of the judgment corresponds to the > truth of the proposition/type. >=20 > 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". >=20 > In the programming languages field, we use "logical equivalence" to > refer to a type directed extensional equality, for what it's worth. >=20 >>=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"). >=20 > Now, in response to this, Andrew has said:=20 >=20 >> The distinction is that it is the equality predicate/formula/thing-you-c= an-prove-or-inhabit. >=20 > 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=F6f's paper "Analytic and > Synthetic Judgment in Type Theory". >=20 > So, we can say with confidence that the distinction is not that it is a > thing which you can prove=97since that is in fact the same for judgments > and for types. The difference is just the level at which this object > lives... >=20 >>=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". >=20 > 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. >=20 > [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=97what I recall from what Pete= r > Dybjer mentioned last year is that Agda is based on an extension of > Martin-L=F6f's Logical Framework, which is described in detail in > Nordstr=F6m et al's "Programming in Martin-L=F6f'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.] >=20 > So, what's the place for "definitional equality"? In Per Martin-L=F6f'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)=97i.e. equality of "sense". >=20 > 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. >=20 > 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=97it just > 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=85 There is little rhyme or reason to > it, and I think that's OK. >=20 > 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. >=20 > Best, > Jon >=20 >=20 >>=20 >> --=20 >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >=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.