Re: [HoTT] Different notions of equality; terminology

[Dan Licata <d...@cs.cmu.edu>]

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.