Different notions of equality; terminology

Different notions of equality; terminology

[Andrew Polonsky]

[-- Attachment #1.1: Type: text/plain, Size: 4214 bytes --]

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.


[-- Attachment #1.2: Type: text/html, Size: 5195 bytes --]

Re: [HoTT] Different notions of equality; terminology

[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?

Re: [HoTT] Different notions of equality; terminology

[Vladimir Voevodsky]

[-- Attachment #1.1: Type: text/plain, Size: 643 bytes --]


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




[-- Attachment #1.2: Type: text/html, Size: 1603 bytes --]

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] Different notions of equality; terminology

[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

Re: [HoTT] Different notions of equality; terminology

[Dimitris Tsementzis]

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

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

> On Jul 18, 2016, at 17:05, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> 
> 
>> On Jul 18, 2016, at 10:45 PM, Andrew Polonsky <andrew....@gmail.com <mailto: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.
> 
> 
> 
> 
> -- 
> 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 <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


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

Re: [HoTT] Different notions of equality; terminology

[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

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

Re: [HoTT] Different notions of equality; terminology

[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

On Mon, Jul 18, 2016 at 11:17 PM, Jon Sterling <j...@jonmsterling.com> wrote:
>> 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
>
> On Mon, Jul 18, 2016, at 01:45 PM, Andrew Polonsky 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.
>
> --
> 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.
> For more options, visit https://groups.google.com/d/optout.

Re: [HoTT] Different notions of equality; terminology

[Vladimir Voevodsky]

[-- Attachment #1.1: Type: text/plain, Size: 2986 bytes --]

In the abstract (http://fomus.weebly.com/abstracts.html <http://fomus.weebly.com/abstracts.html>)  I meant the theory of Altenkich, Capriotti and Kraus (http://arxiv.org/abs/1604.03799 <http://arxiv.org/abs/1604.03799>) or the logic-enriched type theory by Part and Lou (https://arxiv.org/abs/1506.04998 <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 <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?
>>>> 
>>>>> On Jul 18, 2016, at 11:13 PM, Andrew Polonsky <andrew....@gmail.com> wrote:
>>>>> 
>>>>> 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
>>>>> 
>>>>> --
>>>>> 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 #1.2: Type: text/html, Size: 4609 bytes --]

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] Different notions of equality; terminology

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

Re: [HoTT] Different notions of equality; terminology

[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


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

Re: [HoTT] Different notions of equality; terminology

[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

Re: [HoTT] Different notions of equality; terminology

[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

Re: [HoTT] Different notions of equality; terminology

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

Re: [HoTT] Different notions of equality; terminology

[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


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

Re: [HoTT] Different notions of equality; terminology

[Egbert Rijke]

[-- 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 --]

Re: Different notions of equality; terminology

[Martin Hotzel Escardo]

[-- Attachment #1.1: Type: text/plain, Size: 5357 bytes --]

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 

On Monday, July 18, 2016 at 9:45:57 PM UTC+1, Andrew Polonsky 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.
>
>

[-- Attachment #1.2: Type: text/html, Size: 6481 bytes --]

Re: [HoTT] Different notions of equality; terminology

[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

On Jul 19, 2016, at 12: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.