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.