In type theories, an intensional identity type $\textsf{Id}(a,b,A)$ is well-formed iff $a,b:A$ for $A:\textsf{Type}_i$. I have two small questions about the negation of intensional identity types:
- Let $a$ and $b$ be different, does $\neg\textsf{Id}(a,b,A)$ mean that $a$ and $b$ are non-equal terms of $A$?
- Let $a$ and $b$ be equal, then we have $\textsf{Id}(a,a,A)$. In this case, what does $\neg\textsf{Id}(a,a,A)$ mean? It appears to me that this negation is nonsense since the well-formedness of $\neg\textsf{Id}(a,a,A)$ already presupposes that $a:A$ and trivially $a$ and $a$ are equal terms of $A$.
I am not sure if I understood correctly the basics of intensional identity. Could anyone help with this? Thanks in advance!
First, let's fix that by equality of terms we mean definitional equality, i.e. two terms are equal if they are $\beta\eta$-convertible.
The answer depends on the typing context. It's possible that $\neg\textsf{Id}(a,a,A)$ is an assumption in context, in which case it does not follow that $a$ is not definitionally equal to $a$. So in arbitrary contexts the answer is no.
If we're in the empty context, then the answer is yes. In this case we can use the consistency of the system (which holds for usual type theories). Consistency says that the empty type has no proof in the empty context. Assume that $\neg\textsf{Id}(a,b,A)$ is provable in the empty context. Now, $a$ cannot be definitionally equal to $b$, because in that case $\textsf{Id}(a,b,A)$ would be provable by $\textsf{refl}$, which would make it possible to get an inhabitant of the empty type, contradicting consistency.
As pointed out in the comments, $\neg\textsf{Id}(a,a,A)$ is just a type which is equivalent to the empty type, as it immediately implies the empty type.