Re: [HoTT] Different notions of equality; terminology

[Michael Shulman <virit...@gmail.com>]

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".

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").

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".