Re: [HoTT] Re: Why do we need judgmental equality?

["Ansten Mørch Klev" <anstenklev@gmail.com>]

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

I would object to the characterization of definitional identity as identity
of sense. Sense is often glossed as mode of givenness; or one might say
that the sense of an expression determines a route to its reference. Now
take terms such as 7+5 and 9+3. These are definitionally identical, but
they present the number twelve in different ways; qua senses each
determines a different route to ssssssssssss(0). Hence they are not the
same senses. Identity of sense is, to my mind, a stricter relation than
definitional identity.

Very often, also in this thread, the notions of judgemental identity and
definitional identity seem to be treated as one and the same thing. But by
judgemental identity we should mean a certain form of identity assertion
that is different from the assertion that an identity proposition/type is
true/inhabited; and by definitional identity we should mean one among
several relations on terms that may properly be called a relation of
identity.

Here is an argument for the need of a form of identity assertion other than
p : Id(A,a,b). The proposition Id(A,a,b) is formed by applying the function
Id to the type of individuals (set in Martin-Löf's terminology) A, and the
elements a,b : A. The notion of a function, however, presupposes a notion
of identity: f is a function only if, when applied to identical arguments
a, b, we get identical results f(a), f(b). On pain of circularity, the
notion of identity appealed to here cannot be propositional identity.
A notion of identity is also implicit in the notion of domain presupposed
by the notion of a function: f is a function from the domain A to the
domain B. To have the right to speak of A as a domain we need to know what
it is for elements of A to be identical, we need to know a criterion of
identity for A.

In type theory the alternative form of identity assertion, used for
instance in the explanation of what a function is, is the identity
judgement a = b : A. There is nothing in the argument just given that
forces the relation picked out by this form of identity assertion to be
definitional identity; but there may be other arguments why such an
interpretation is preferable.





On Wed, Feb 13, 2019 at 7:37 AM Matt Oliveri <atmacen@gmail.com> wrote:

> OK. So it sounds like definitional equality is another way of thinking
> about equality of sense, and is generally not the same as strict equality.
> That's a relief.
>
> But the use of judgmental equality for capturing a system of paths that's
> fully coherent is actually about strict equality, in general; not
> necessarily judgmental or definitional equality.
>
> So to bring things back to HoTT, what are people's opinions about the best
> use of these three equalities?
>
> My opinion is that strict equality should be implemented as judgmental
> equality, which should be richer than definitional equality, by using a
> 2-level system with reflective equality. This is the case in HTS and
> computational higher dimensional type theory. We would still probably want
> to consider different theories of strict equality, but there would be no
> obligation to implement them as equality algorithms. Definitional equality
> would be a quite separate issue, pertaining to proof automation.
>
> On Tuesday, February 12, 2019 at 12:54:24 PM UTC-5, Michael Shulman wrote:
>>
>> For sure definitional equality doesn't have to do with models.  Like
>> all the kinds of equality we are discussing, it is a syntactic notion.
>> Actually I would say it is a *philosophical* notion, and as such is
>> imprecisely specified; syntactic notions like judgmental equality can
>> do a better or worse job of capturing it in different theories (and in
>> some cases may not even be intended to capture it at all).
>>
>> > what's the difference between "denoting by definition" and regular
>> denoting?
>>
>> x+(y+z) and (x+y)+z denote the same natural number for any natural
>> numbers x,y,z, because we can prove that they are equal.  But they
>> don't denote the same natural number *by definition*, because this
>> proof is not just unfolding the meanings of definitions; it involves
>> at least a little thought and a pair of inductions.
>>
>> For a more radical example, "1+1=2" and "there do not exist positive
>> integers x,y,z,n with n>2 and x^n+y^n=z^n" denote the same
>> proposition, namely "true".  But that's certainly not the case by
>> definition!  Same reference; different senses.
>>
> --
> 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 HomotopyTypeTheory+unsubscribe@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 HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

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