In type theory, why isn't $x = x' : X$ simply wrong? If $X$ is a set, then personally, I tend to think of the equality relation on $X$ as a function $X^2 \rightarrow \mathrm{Bool}.$ Following this intuition, think that if $x$ and $y$ are variables of type $X$, then $x=y$ should be a term of type $\mathrm{Bool}.$
However, in my attempts to get educated about type theory, I have often seen expressions like
$$x = x' : X$$
where $X$ isn't the Boolean domain, nor even a poset.
Why aren't expressions like this just... wrong?
 A: The meaning of $x = x' : X$ in Pitts' chapter you cite is not to say that $x = x'$ is of type $X$, but rather $x = x' : X$ is just notation for "equality in context" which is supposed to mean that $x$ and $x'$ are equal terms of type $X$. The whole construct $x = x' : X$ is assigned no type since he's considering only equational logic at that point but it could have type $\mathrm{Prop}$, the type of propositions. 
In type theory you have two different notions of equality. The judgement $M \equiv M' : X$ which means that $M$ and $M'$ are convertible terms of type $X$. But this judgement has no type, it's a notion external to type theory. To talk about equality inside type theory one can define propositional, internal equality. Then given a type $X$ and $x, x'$ of type $X$ one can form a new type $x =_X x'$. 
For instance in case of Coq, this type itself has type $\mathrm{Prop}$, the type of propositions. In case of Agda, this type can have type $\mathrm{Set}$, the type of all "small" types.
This is explained very well in the first chapter of the HOTT book
