1. There are at least two ways in which types are not sets. Firstly, when reasoning classically, we have a membership relation whereby we can postulate the membership of elements in a given set. It may seem similar to a : A but in this case writing a : B would make no sense, whereas in set theory membership can be disproven. This is quite a subtle notion and is closely related to the difference between structural and material set theories which Mike Shulman wrote a nice paper on
https://arxiv.org/pdf/1808.05204.pdf. But I am sure someone else here will do a better job at explain that.
The second difference is what I think Harper was referring to, which is that sets are types which satisfy what is called Uniqueness of identity proofs (UIP). This means that given a : A and b : A, we can form the identity type Id(a, b). If we wish to show there is an equality between a and b we construct a term p : Id(a, b). But what if we can construct another equality q : Id(a, b)? UIP (a.k.a axiom K) ensures that there is always a term r : Id(p, q). Which in English means: Any two proofs of equality between elements of a set are themselves equal.
Why does this matter? Well because in Martin-Lof type theory (with univalent universes) (the type theory that HoTT is based on), you can construct seperate proofs of the same thing. Take for example the type 2. It has two terms 1_2 : 2 and 2_2 : 2. If we consider the ways in which 2 can be equal to itself, i.e. terms of Id(2, 2), we see that (with univalence) there are two possible ways. The first is just reflexivity and the second is "an equality" which swaps 1_2 with 2_2. These are both proofs of Id(2, 2) but they are definitely not the same. And in fact can't be shown to be the same without assuming UIP.
2. One heuristic way to see that judgemental equality can be decided is by "completely computing" a given term, i.e. beta reduce it all the way down. Theorems such as Church-Rosser guarantee that the order of reductions does not matter. There are more properties such as "canonicity" which roughly state that fully reduced terms are identical. I am not an expert on these properties however but there are many experts on this list.
Checking whether two terms are judgementally equal is a commonly studied problem in type theory. There are ways to test equality without fully reducing down such as the one detailed here:
3. Simply typed lambda calculus has "natural numbers" via the Church-encoding. The key difference between this and regular arithmetic is that you can't really define a function out of the type of such things. Or in other words, there is no recursion principle for the natural numbers. Adding such a rule would give you something like Godels system T. Universes only need a sucessor structure, and not really the full arithmetic capabilities of the natural numbers themselves.
These are just some of my thoughts on your questions, hopefully it will help.
Ali Caglayan