What exactly is the semantic difference between set and type?
To understand the difference between sets and types, ones has to go back to pre-mathematical ideas of "collection" and "construction", and see how sets and types mathematize these.

There is a spectrum of possibilities on what mathematics is about. Two of these are:


We think of mathematics as an activity in which mathematical objects are constructed according to some rules (think of geometry as the activity of constructing points, lines and circles with a ruler and a compass).
Thus mathematical objects are organized according to how they are constructed, and there are different types of construction. A mathematical object is always constructed in some unique way, which determines its unique type.
We think of mathematics as a vast universe full of pre-existing mathematical objects (think of the geometric plane as given). We discover, analyze and think about these objects (we observe that there are points, lines and circles in the plane). We collect them into set. Usually we collect elements that have something in common (for instance, all lines passing through a given point), but in principle a set may hold together an arbitrary selection of objects. A set is specified by its elements, and only by its elements. A mathematical object may belong to many sets.


We are not saying that the above possibilities are the only two, or that any one of them completely describes what mathematics is. Nevertheless, each can view can serve as a useful starting point for a general mathematical theory that usefully describes a wide range of mathematical activities.

It is natural to take a type $T$ and imagine the collection of all things that we can construct using the rules of $T$. This is the extension of $T$, and it is not $T$ itself. For instance, here are two types that have different rules of construction, but they have the same extension:


The type of pairs $(n, p)$ where $n$ is constructed as a natural number, and $p$ is constructed as a proof demonstrating that $n$ is an even prime number larger than $3$.
The type of pairs $(m, q)$ where $m$ is constructed as a natural number, and $q$ is constructed as a proof demonstrating that $m$ is an odd prime smaller than $2$.


Yes, these are silly trivial examples, but the point stands: both types have nothing in their extension, but they have different rules of construction. In contrast, the sets
$$\{ n \in \mathbb{N} \mid \text{$n$ is an even prime larger than $3$} \}$$
and
$$\{ m \in \mathbb{N} \mid \text{$m$ is an odd prime smaller than $2$} \}$$
are equal because they have the same elements.

Note that type theory is not about syntax. It is a mathematical theory of constructions, just like set theory is a mathematical theory of collections. It just so happens that the usual presentations of type theory emphasize syntax, and consequently people end up thinking type theory is syntax. This is not the case. To confuse a mathematical object (construction) with a syntactic expression that represents it (a term former) is a basic category mistake that has puzzled logicians for a long time, but not anymore.