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.