Different notions of equality; terminology

[Andrew Polonsky]

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.

[Andrej Bauer]

On Mon, Jul 18, 2016 at 10:45 PM, Andrew Polonsky
<andrew....@gmail.com> wrote:
> 1. DEFINITIONAL EQUALITY.

Judgmental equality seems a better phrase, no?

[Vladimir Voevodsky]

On Jul 18, 2016, at 10:45 PM, Andrew Polonsky <andrew....@gmail.com> wrote:

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.

I am not sure what you mean by this.  In fact, I emphasized that the only substitutional equality in MLTTs is the definitional equality that can not be postulated or proved, only checked. 

Vladimir.

[Andrew Polonsky]

On Mon, Jul 18, 2016 at 11:05 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> 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.
>
>
> I am not sure what you mean by this. In fact, I emphasized that the only
> substitutional equality in MLTTs is the definitional equality that can not
> be postulated or proved, only checked.

I mean that your system with two equalities promotes strict equality
of MLTT from definitional to the logical level. It remains
"substitutional" but can be asserted in context.

It would be nice to have a few simple demonstrations of the uses of
this, without getting into simplicial types.

Andrew

[Dimitris Tsementzis]

I think this is terminological. I understood Polonsky (and correct me if I’m wrong) as saying that something like the “exact equality” of HTS is a “substitutive equality” that exists at the object (or what he is calling “logical”) level and can therefore be reasoned about. (It is of course distinct from the judgmental equality of HTS which lies in the background.) 

So is the so-called exact equality of HTS an example of a “substitutive equality” for you? Or do you still call that “transportational” and reserve the name “substitutive” for meta-level equalities that can only be checked? (This is a terminological question.)

Dimitris

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

[Jon Sterling]

> 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

On the contrary, for a type theorist, this is *very good*. That's
because the entire type-theoretic/judgmental methodology is arranged
around a single move, which is to take a kind of observation which
exists at the judgmental level, and internalize it to one that exists at
the propositional level without losing information.

So, "equality reflection" in MLTT is just the recognition that nothing
at all was added when the judgmental equality (which of course includes
all the standard laws from the meaning explanation, including functional
extensionality, etc.) was internalized into a proposition.

It is interesting to remember that "equality reflection" is derivable
when restricted to the empty context (and, clearly, any type theory for
which this does not hold is broken—i.e. the type in question is then not
an "equality type", but something else—and figuring out precisely what
that "something else" is has been the main force of the past few years
in the development of cubical type theory).

As you know, the concerns that you raise only come into play in the
rule's full generality at a non-empty context, which leads me to clarify
that the real "dangerous" force of equality reflection has little to do
with equality, and everything to do with the following position (which
you are free to accept or to reject depending on what you want to use
type theory for):

The meaning of "G !- P true" (i.e. P under hypothesis) is completely
defined from the meaning of "G" and the meaning of "P" under no
hypotheses.

Indeed, the standard semantics for type theory are arranged in this way.
Nonstandard semantics, including categories-with-families, follow the
approach pioneered in universal algebra, where the meaning of a type the
specification of its closed members, but rather specifies in addition
what its members shall be under an arbitrary context, subject of course
to various coherences with substitutions.

Anyway, it's fine to want strong normalization (that is, normalization
in any context, even an inconsistent one!) & decidability—I can think of
a million places where I *do* want this. But let's be precise and
collegial with our language instead of throwing around phrases like
"really bad"—there's no point to be insulting a body of theory which has
been incredibly successful and useful, and by extension, to insult &
dismiss the people who work on it, such as myself, my advisor, and many
of my friends and heroes.

Thanks,
Jon

[Andrew Polonsky]

Dear Jon,

I am sorry to have offended you, and I hope your advisor & heroes do
not feel as you do.

But I maintain, with humility, that propositional reflection is
really, really bad.

With respect,
Andrew

> You received this message because you are subscribed to a topic in the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/HomotopyTypeTheory/1bUtH8CLGQg/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to HomotopyTypeThe...@googlegroups.com.

[Vladimir Voevodsky]

In the abstract (http://fomus.weebly.com/abstracts.html)  I meant the theory of Altenkich, Capriotti and Kraus (http://arxiv.org/abs/1604.03799) or the logic-enriched type theory by Part and Lou (https://arxiv.org/abs/1506.04998).  One can also apply it to the possible theories with the second transportational equality of the form suggested at the end of my talk today.

In the HTS (https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf)  there is still only one substitutional and one transportational equality but the substitutional one is, indeed, type-based and so can be reasoned about at the object level. 

Vladimir.

On Jul 18, 2016, at 11:18 PM, Andrew Polonsky <andrew....@gmail.com> wrote:

I mean whatever system is implicitly referred to by the last sentence
in the abstract of your talk.

On Mon, Jul 18, 2016 at 11:16 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

Referring to it at what point in the talk?

On Jul 18, 2016, at 11:16 PM, Andrew Polonsky <andrew....@gmail.com> wrote:

I assumed you were referring in your talk to HTS or some variant of it.

On Mon, Jul 18, 2016 at 11:15 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:

I still do not understand. What do you mean by my system?

[Andrew Polonsky]

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

[Jon Sterling]

On Mon, Jul 18, 2016, at 03:20 PM, Andrew Polonsky wrote:
> 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.

This is false, as far as I am aware. From what Peter Dybjer told me,
Agda is based on an extension of Martin-Löf's Logical Framework +
Monomorphic Theory of Sets (these are described in "Programming in
Martin-Löf's Type Theory"). Now, there's some differences between Agda's
type theory and MLLF+MTS, but both absolutely have judgmental equality.

I am not familiar enough with Coq's type theory to comment on it.

Kind regards,
Jon

[Andrew Polonsky]

> case I think it better to use a word that conveys *exactly* what the
> distinction is,

The distinction is that it is the equality
predicate/formula/thing-you-can-prove-or-inhabit.

> I suppose judgmental equality doesn't have to be formulated as a
> judgment, but as far as I know in all cases it can be so, without
> changing the type theory materially.

In principle, this should of course always be possible. But in
practice, one often describes and implements the systems long before
the conjecture above is verified. (If ever.)

> It is not always, however, 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.

In type theory with reflection rule, one can think of all equalities
as "definitional", including those that appear in the hypothesis of
the reflection rule.

Andrew

[Andrew Polonsky]

>>> case I think it better to use a word that conveys *exactly* what the
>>> distinction is,
>>
>> The distinction is that it is the equality
>> predicate/formula/thing-you-can-prove-or-inhabit.
>

> "Predicate/formula/thing-you-can-prove-or-inhabit" is a long-winded
> way of saying "type".

However, that distinction was present before types. It is indeed
illogical to call "typal" something which was there before types were
invented.

>> In type theory with reflection rule, one can think of all equalities
>> as "definitional", including those that appear in the hypothesis of
>> the reflection rule.
>

> Only if you are willing to redefine the word "definition".

I am quite happy with it as is.

Andrew

[Michael Shulman]

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

[Jon Sterling]

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

[Egbert Rijke]

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

[Martin Hotzel Escardo]

Just a small remark.

It is indeed sui generis that equality in its various manifestations has this special status in type theory.

It is not *just* that we have different notions of equality. The notions of equality play a fundamental role in the very *architecture* of type theories.

The fundamental reason we need judgemental equality is, in particular, to make sense of type dependency.

We can have a type theory with judgemental equality but without an identity type.

It would be much more difficult, however, to have a type theory with an identity type but without a judgemental equality. (I am not saying it is impossible, and the idea sounds vaguely attractive.)

Although HoTT/UF makes good sense of the identity type ("typal equality"), I am not convinced it gives the ultimate explanation of judgemental equality. (But I am listening.)

Best,
Martin

[Dan Licata]

Maybe part of the problem is that we are trying to jam the terminology into too low-dimensional a feature space? I think there are at least the following different distinctions:

(A) how do you use an equality? I'll use Vladimir's terminology of substitutional vs transportational for this.

(B) is the equality represented by an element of a type, or by a judgement other than membership in a type? I'll use typal vs judgemental for this, though this is a generalization of what is usually called "judgemental".

(C) is the equality "strict"/"exact", or a "path"/"identification"?

Of these, I can come up with examples for 6/8 (not (substitutional and path)):

A=substitutional, B=typal, C=exact: the equality type in a computational type theory or ITT+equality reflection
A=substitutional, B=typal, C=path: doesn't make sense
A=substitutional, B=judgemental, C=exact: the equality judgement in a computational type theory
A=substitutional, B=judgemental, C=path: doesn't make sense
A=transportational, B=typal, C=exact: the equality type in the Altenkirch, McBride, Swierstra observational type theory paper
A=transportational, B=typal, C=path: the Id_A(M,N) type in intensional type theory + univalence
A=transportational, B=judgemental, C=exact: rarer, but has come up in some programming languages work, e.g. "System FC" which is used as an internal language in the GHC Haskell compiler. here there is a judgement of type equality that are used as "coercions" but which have no actual runtime effect. another example would be something where you mark uses of (what is usually called) a "definitional equality" judgement in the terms
A=transportational, B=judgemental, C=path: a line x:I |- a : A in a cubical type theory

-Dan