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

[Michael Shulman <shulman@sandiego.edu>]

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.