Re: [HoTT] Different notions of equality; terminology

[Andrew Polonsky <andrew....@gmail.com>]

That may all be true.

Yet, -- in this particular case -- it may actually be a good idea NOT
to depart completely from the traditional, intuitive meaning of
"logical".

The point is that here we are talking about what is really the most
elementary, the most canonical, the most ancient concept of equality.
The adjective "typal" suggests that something new happened when we
transitioned from FOL to MLTT.  But that change, whatever you call it,
(higher-dimensionality?) -- it affected equality in the same way as
all other formulae.

So it is not a new concept.  It is the same concept.

Regarding "judgmental" equality, this is a special case of
definitional equality.  Some formulations of type theory have it,
others don't.

For example type theories implemented in the Coq and Agda proof
assistants, they do not have judgmental equality.  In PTS formulations
of type theory, definitional equality is not a judgment.

Cheers,
Andrew

On Tue, Jul 19, 2016 at 12:02 AM, Michael Shulman <shu...@sandiego.edu> wrote:
> 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 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*.  Sometimes it is accurate to call it
> "definitional equality", but it is not always the case that such a
> statement of equality *is a definition*.)
>
> On Mon, Jul 18, 2016 at 5:45 PM, Andrew Polonsky
> <andrew....@gmail.com> wrote:
>> Good evening.
>>
>> One feature of type theory which is often confusing to newcomers is the
>> presence of several notions of equality.  Today, at the opening of the FOMUS
>> workshop, Vladimir gave a talk about the very subject -- but more on that
>> later.  The two most common notions are usually called "definitional
>> equality" and "propositional equality".
>>
>> It is agreed by most members of this list that the name of the latter notion
>> is unfortunate, if not misleading.  I would like to suggest the name
>> "logical equality" to be used for this notion.
>>
>> First, let us summarize the two notions in greater detail.
>>
>>
>> 1. DEFINITIONAL EQUALITY.
>>
>> PROPERTIES.
>>
>> - Purely syntactic: "proofs" of this equality concern only the way the
>> objects are presented;
>> - Is always interpreted strictly;
>> - Preserved under all contexts:
>>   If M=N definitionally, then C[M]=C[N], still definitionally;
>> - Validates strict conversion rule:
>>   If t has type A, and A is definitionally equal to B,
>>   Then t *itself* has type B. (Not a transport of t, nor some term equal to
>> t.)
>> - Cannot be asserted in a derivation context [*]
>> - In total languages, is usually, but not always, decidable.
>>
>> EXAMPLES.
>>
>> - Judgmental equality (in the LF formulation of type theory);
>> - Untyped conversion (in the PTS formulation of type theory);
>> - Well-typed conversion (all reduction subsequences must pass through
>> well-typed terms);
>> - Equalities which result from newly introduced rewrite rules;
>> - Equalities which result from unification/pattern-matching constraints;
>> - Any equalities arising from quotienting the term algebra (eg, by
>> contextual equivalence).
>>
>>
>> 2. LOGICAL EQUALITY
>>
>> PROPERTIES.
>> - Is a type constructor/formula former in the object language; thus
>> - Can be asserted into a derivation context;
>> - Induces isomorphism/equivalence of fibers between dependent types; thus
>> - Allows a term of any type to be transported to a type logically equal to
>> it;
>> - May be interpreted weakly/as a path.
>>
>> EXAMPLES.
>> - The native equality of first-order logic;
>> - In particular, equality in set theory;
>> - Martin-Lof identity type;
>> - Univalent equality in HoTT/UF;
>> - Leibniz equality in impredicative dependent type theories (Calculus of
>> Constructions);
>> - Extensional equality in Observational Type Theory;
>> - The Paths type in Cubical Type Theory.
>>
>> The first example above is the main motivator for this terminological
>> proposal.  Whether one considers equality as a "logical symbol", it is
>> obviously a concept which is present at the level of *formulas*.  Under
>> formulae-as-types interpretation, one would naturally tend to think of it as
>> a proposition, until one came to realize that some types are not
>> propositions.  (Indeed, it was the only dependent type former in Howard's
>> original paper.  Yet it could not be iterated/applied to itself.)
>>
>> The point is that the second kind of equality is the one which can be
>> reasoned about internally, *in the object logic*.  Hence, it exists not on
>> the level of terms and definitions, but on the level of logic and
>> proofs/constructions of formulae/types.
>>
>>
>> One argument against the adjective "logical" is that it can lead to
>> confusion with "logical equivalence".  But I don't think that that is a
>> certain outcome.
>>
>> An alternative descriptor could be "type-level" or "type-theoretic", but
>> both are rather awkward and unrevealing.
>>
>>
>> Finally, Voevodsky currently distinguishes between "substitutive" and
>> "transportational" equalities.  But in his system, both concepts are of the
>> "logical" kind.  The effect is therefore to promote "strict" equality to the
>> logical level; so one can reason about it in the object logic, while
>> retaining other properties like the conversion rule.
>>
>> The effect of Martin-Lof's "propositional reflection rule" is simply to
>> collapse the two levels and make them one and the same.
>> For the type theorist, this is really bad, because it breaks nice properties
>> like normalization and decidability of type checking.
>> For the homotopy type theorist, this is really bad, because it is
>> inconsistent with univalence.
>>
>> Best regards,
>> Andrew
>>
>> [*]  In certain settings, one can make sense of definitional equalities
>> "in-context" via the so-called Girard--Schroder-Heister (GSH) elimination
>> rule.
>>
>> --
>> 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.