From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.17.221 with SMTP id y29mr9997388oty.18.1468955234450; Tue, 19 Jul 2016 12:07:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.17.158 with SMTP id 30ls1782129ior.15.gmail; Tue, 19 Jul 2016 12:07:13 -0700 (PDT) X-Received: by 10.98.29.4 with SMTP id d4mr28345503pfd.11.1468955233465; Tue, 19 Jul 2016 12:07:13 -0700 (PDT) Return-Path: Received: from mail-vk0-x231.google.com (mail-vk0-x231.google.com. [2607:f8b0:400c:c05::231]) by gmr-mx.google.com with ESMTPS id p17si1762030vkd.0.2016.07.19.12.07.13 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 19 Jul 2016 12:07:13 -0700 (PDT) Received-SPF: pass (google.com: domain of e.m....@gmail.com designates 2607:f8b0:400c:c05::231 as permitted sender) client-ip=2607:f8b0:400c:c05::231; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of e.m....@gmail.com designates 2607:f8b0:400c:c05::231 as permitted sender) smtp.mailfrom=e.m....@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-vk0-x231.google.com with SMTP id s189so37786282vkh.1 for ; Tue, 19 Jul 2016 12:07:13 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=oT6k8cBBJIClLfxUUFyucYWz9gHfk++re5zef+47/Uc=; b=zLTZSXXBoYaGclhZVAkn81wPMeSD1gi4s+nPWMNEP7FLG7VT4oIuRCD+CU2A4iUhsg ulPH8wwqDytPdSlmHTImezRrBdCPNFrwZhRe6f3x002CMAdkr1Opd6Qyx+3zrVJ2KXCh I9nvqb9MeQoP8Clh1IgeIu8KHUdZ5KUoQCbq1Hlup8eCHyVlywisTSg2D5Le/yGr+qU2 VPwDM2VkQi6Bp6x6rE23XoD/id1fMJzkitXO/VCqO3EB1Y5SB773Ft1nyvX0wFZxMKcg N/xwv6IfvdlRevwNz4U9pvCTY28t1tAtIkuWQeHEpmZ1azNsSkWNRwYoLzi/kYhkdWBE 2oPw== X-Gm-Message-State: ALyK8tLUBtl8sSHQZMtDBJqFHCjxehofBx1th7wnItp3eJlyU+zY7Jmt/54KpuqozYKGtIYlR7LKiiFFB7WWHQ== X-Received: by 10.31.96.74 with SMTP id u71mr22251969vkb.88.1468955233146; Tue, 19 Jul 2016 12:07:13 -0700 (PDT) MIME-Version: 1.0 Received: by 10.103.121.17 with HTTP; Tue, 19 Jul 2016 12:07:12 -0700 (PDT) In-Reply-To: <1468946947.2314129.670766785.49572383@webmail.messagingengine.com> References: <1468946947.2314129.670766785.49572383@webmail.messagingengine.com> From: Egbert Rijke Date: Tue, 19 Jul 2016 21:07:12 +0200 Message-ID: Subject: Re: [HoTT] Different notions of equality; terminology To: Jon Sterling Cc: "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary=001a114e50dcdcdd3e053801ca91 --001a114e50dcdcdd3e053801ca91 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Internal equality would be a good term when studying the internal logic of a model. However, type theory is also studied just by itself without referring to models, and moreover the semantics side of HoTT is not yet well understood. "Internal equality" suggests that we know what it is internal of, but that is not the case unless we have a (class of) model(s) in mind. Therefore I like typal equality better. With kind regards, Egbert On Tue, Jul 19, 2016 at 6:49 PM, Jon Sterling wrote= : > 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 = the > 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. > > > > ~~ > > > > 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. > > > > > 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: > > > The distinction is that it is the equality > predicate/formula/thing-you-can-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 a= nd > 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 judg= ments > and for types. The difference is just the level at which this object > lives... > > > > > 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. > > > > 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 wha= t 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"; no= w, 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 = 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=E2=80=A6 There is little rhyme or rea= son 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 > > > > > > -- > > 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 HomotopyTypeThe...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > > -- > 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. > --001a114e50dcdcdd3e053801ca91 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Internal equality would be a good term when studying the i= nternal logic of a model. However, type theory is also studied just by itse= lf without referring to models, and moreover the semantics side of HoTT is = not yet well understood. "Internal equality" suggests that we kno= w what it is internal of, but that is not the case unless we have a (class = of) model(s) in mind. Therefore I like typal equality better.

With kind regards,
Egbert

On Tue, Jul 19, 2016 at 6:49 PM, Jon St= erling <j...@jonmsterling.com> wrote:
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", si= nce 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.=C2=A0 The problem was an email issue o= n my
> end.=C2=A0 Below I summarize the content of my messages; this will be = my
> last email on the subject.
>
> ~~
>
> I have been advocating the term "typal equality" for what us= ed to be
> called "propositional".=C2=A0 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*.=C2=A0 I prefer it to "logical = equality"
> because traditionally, "logic" has often referred only to th= e type
> theory of mere propositions, so "logical equality" has somet= hing 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.

>
> For the reasons given by Andrew, in most cases it suffices to simply > say "equality".=C2=A0 It only occasionally happens that we n= eed 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.=C2=A0 (If this is "logical" equality, is t= he other one
> "illogical"?)=C2=A0 Typal equality is indeed related to othe= r 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&qu= ot; is
> just a long-winded way of saying "type").

Now, in response to this, Andrew has said:

> The distinction is that it is the equality predicate/formula/thing-you= -can-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&quo= t; 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 "Ana= lytic 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...

>
> For the same reasons, I prefer "judgmental equality" because= it
> conveys exactly what is meant in that case, namely that the statement<= br> > of equality *is a judgment*.=C2=A0 Maybe it doesn't have to be for= mulated
> as a judgment, but as far as I know in all cases it can our could be > so, without changing the type theory materially.
>
> This possible slight inaccuracy seems to me to be preferable to the > more serious problem with "definitional equality", namely th= at such a
> statement of equality is certainly not always a definition.=C2=A0 For<= br> > instance, in type theory with a reflection rule from typal equality to=
> judgmental, there is no sense in which a judgmental equality obtained<= br> > by that rule is a "definition" of one side in terms of the o= ther.
> Associativity of addition of natural numbers is not true "by
> definition" unless you are willing to redefine the word "def= inition".

Excellent remark about "judgmental equality" and "def= initional
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 "sligh= t
inaccuracy" to worry about; that is, people often have this idea that<= br> untyped conversion (for instance) is not "judgmental", but whethe= r
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<= br> this does not mean it lacks an equality judgment.]

So, what's the place for "definitional equality"? In Per Mart= in-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&q= uot;.

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 just
depends on the theory, and sometimes one equality *judgment* is singled
out as "the judgmental equality", and other finer-grained "e= quality"
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 contras= t 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


>
> --
> You received this message because you are subscribed to the Google Gro= ups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send= an
> email to Homot= opyTypeThe...@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 HomotopyTyp= eThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--001a114e50dcdcdd3e053801ca91--