Re: [HoTT] Different notions of equality; terminology

[Egbert Rijke <e.m....@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 7693 bytes --]

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 <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", since the whole
> point is that it consists in the internalization of a judgment as a
> proposition/type—and 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öf'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—since that is in fact the same for judgments
> 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—what I recall from what Peter
> Dybjer mentioned last year is that Agda is based on an extension of
> Martin-Löf's Logical Framework, which is described in detail in
> Nordström et al's "Programming in Martin-Löf'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öf'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)—i.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—it 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… There is little rhyme or reason 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 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.
>
> --
> 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.
>

[-- Attachment #2: Type: text/html, Size: 9310 bytes --]