Intensional identity I have some basic questions about intensional identity. Two types are said to be (intensionally) identical iff “they have the same objects and identical
objects of one of the types are also identical objects of the other'' (p. 141 in Nordstrom et al. (1990)).

*

*Does this mean that two types are (intensionally) identical iff they imply each other (or they are equivalent)?

*If this is the case, then if we negate an intensional identity type such as the following: $\neg (A=_UB)$, does it mean that $A$ and $B$ does not imply each other (or alternatively, that $A$ and $B$ do not have the same objects)?

*Then apart from their syntactic distinction, what's the difference between $\neg (A=_UB)$ and $\neg(A\leftrightarrow B)$?

 A: First, I would note that what you're quoting doesn't appear to be defining the identity type. It appears to be talking about judgmental equality of types, which is distinct from types that represent proofs that two things are equal/identical. As for your questions:

*

*No.

The notion of having 'the same' objects is not just that there are functions between them. It means that they classify exactly the same things. However, this explanation is not really something you can use to derive an equality between $A$ and $B$. You don't prove that for all $e$, $Γ ⊢ e : A$ if and only if $Γ ⊢ e : B$ and get $Γ ⊢ A = B$ or similar, even for judgmental equality. This explanation is, I think, mainly used to motivate the rules that are subsequently introduced from a meta-reasoning perspective.
(In fact, I'm a little skeptical that the meta-reasoning is actually true. I think it might be possible to have types $A$ and $B$ that classify all the same values, but they are not able to be shown equal by the rules of type theory. However, it's all right as a motivation for how equality should work.)


*No.

For this I would bring up again that what you quoted was talking (I think) about judgmental equality, not the identity type. So it doesn't really make sense to negate it or hypothesize it, at least as part of reasoning within type theory.
But also, the answer is still no for the actual identity type over all. It is correct to say that if $¬(A =_U B)$ holds, then they must not classify all the same terms (because by the previous answer's meta-reasoning, they'd be judgmentally equal in that case). However, that is not equivalent to your other condition.
First, two non-equivalent types can imply one another. It's easy to define functions with types $⊤ → ℕ$ and $ℕ → ⊤$, but the natural numbers have many more values than the singleton type. But also, Martin-löf type theory doesn't even require that equivalent types (where those functions would be inverses to one another) are equal. You could extend MLTT with rules that imply $¬ (A =_U B)$ when those types have distinct appearing elements. For instance, $¬ (ℕ =_U ⊤×ℕ)$, because values of the former are like $5$ and values of the latter are like $(\mathsf{tt}, 5)$. That isn't derivable in plain MLTT, but it isn't refuted either (just like it doesn't refute equivalence implying identity, allowing for homotopy type theory).


*The second is much stronger in general.

The first assumption just says that $A$ is not identical to $B$. The latter says that there are no pairs of functions between them. The only time those really come close to coinciding is for 'propositional' types. But even then, #2 shows that MLTT doesn't rule out e.g. $¬(⊤ =_U ⊤×⊤)$, while it exhibits $⊤ \leftrightarrow ⊤×⊤$

Editing to give a too-long answer to the comment:
The answer to this is going to change somewhat based on the context. In HoTT, there is a principle that ensures that two propositions are equal if and only if they imply each other. However, this principle is not part of MLTT (it is univalence for $\mathsf{Prop}$). Strictly speaking, it is an extensionality principle. 'Intensional' refers to only recognizing things with the same definition as equal.
MLTT does this in a weak way: things with the same definition* are provably equal, and things without the same definition are not [provably equal]. It is fairly non-committal about types being provably disequal. For instance $¬ (⊥ =_U ⊤)$ is derivable, and something like $¬(\mathsf{Fin}(n) =_U \mathsf{Fin}(\mathsf{suc}\ n))$ is derivable. However, $⊤ =_U ⊤×⊤$ is only not-provable, not provably false.
However, just as one can add the extensionality principle of univalence, one could add principles that make equality more committally intensional. Actually, I'm recalling that the book you are reading does this, because it includes an induction principle for the universe. So, it is possible to distinguish values of the universe that are defined differently, even if they denote equivalent types. So I believe $¬\mathsf{Id}(U,\hat ⊤,\hat ⊤ \hat × \hat ⊤)$ is derivable (using the notation of the book). However, this is an atypical definition of the universe of MLTT.
[*] One could quibble about induction principles and computation rules making things with distinct definitions provably equal, though.
