The *extension* is the *observable behavior*, where "observation" means roughly "application of an eliminator". For a predicate $p$ we may observe whether it is true for a given argument, so by collecting those arguments at which $p$ holds we observe all there is to observe. More generally, a function is "observed" by application to an argument (as opposed to examination of its "source code" or measurement of time needed to compute, etc.), which leads to the rule of *function extensionality*
$$\frac{x : A \vdash f(x) =_B g(x)}{f =_{A \to B} g}.$$
A simpler extensionality rule is that for cartesian products:
$$\frac{\pi_1(u) =_A \pi_1(v) \qquad \pi_2(u) = \pi_2(v)}{u =_{A \times B} v}
\tag{1}
$$
It says that two pairs are equal if they behave in the same way when we observe them by projecting their components.

In set theory we observe a set by testing which elements it has, and so the extensionality axiom of set theory says that two sets are equal if they have the same elements. And since in set theory there are only sets, this gives set theory as much extensionality as it could have.

In the internal language of a category, say a topos, we get extensionality from universal properties, more precisely from the uniqueness requirements. For instance, (1) is validated by the fact that there is at most one morphism $C \to A \times B$ whose composition with $\pi_1$ and $\pi_2$ are prescribed maps $C \to A$ and $C \to B$. Furthermore, because in a typical internal language we interpret (judgmental) equality on $A$ as the diagonal $A \to A \times A$, which is the least equivalence relation on $A$, there is no room for another kind of equality -- the reflection principle is automatic, and so the distinction between judgmental and propostional equality does not arise.

In contrast, the *intension* tells us how an object is built or how it works. Thus, functions $x \mapsto x + 3$ and $x \mapsto 2 + (x + 1)$ have the same behavior, but are not intensionally equal because they *compute* in different ways. A typical intensional rule of equality says that two objects are equal if they are built the same way. For pairs such a rule would be
$$\frac{a \equiv_A a' \qquad b \equiv_B b'}{(a,b) \equiv_{A \times B} (a',b')}.$$
Intensional equality of functions says that two functions are equal if they have the same "bodies of definition" (officially this goes under the name $\xi$-rule):
$$\frac{x : A \vdash e \equiv_B e'}{(\lambda x : A \,.\, e) \equiv_{A \to B} (\lambda x : A \,.\, e')}.$$
Another kind of intensional equality explains *how eliminators compute*, for instance
$$\pi_1(a,b) \equiv_A a$$
says that the first projection computes $a$ when applied to a pair $(a,b)$. Similarly, the $\beta$-rule for functions,
$$(\lambda x : A \,.\, e_1) e_2 \equiv_B e_1[e_2/x],$$
explains how $\lambda$-abstractions compute their results, so it is again an intensional rule.

We shall therefore call a notion of equaity *extensional* if it makes objects equal when they have equal observations. We shall call an equality *intensional* if it makes objects equal when they are constructed the same way from equal parts, or if it tells us how to compute. We shall call a type theory extensional or intensional according to whether its judgmental equality is extensional or intensional (this is a source of confusion, as many people think that extensional type theory is so called because it has extensionality rules for propositional equality, see Mike Shulman's answer).

For the purposes of mathematics it is good to have extensional equality, but less so for the purposes of computer science, where we generally care *how* things are computed and not just *what* the results are. As far as type theory is concerned, we have a choice. We could declare judgmental equality to be extensional, for instance
$$\frac{\pi_1(u) \equiv_A \pi_1(v) \qquad \pi_2(u) \equiv_B \pi_2(v)}{u \equiv_{A \times B} v}$$
looks reasonable. Indeed, Agda and (recent) Coq have such a rule. But things get complicated if we take this too far. The reflection rule which you stated makes judgmental equality undecidable, which does not appeal to the typical type theorist. If we make judgmental equality of functions extensional, things get at least very complicated.

It is less unreasonable to make the propositional equality extensional. This is what homotopy type theory does. It goes farther than any other kind of type theory by making the propostional equality of a universe extensional, although at the moment I cannot think of a good explanation of the Univalence axiom which starts from "what is an observation on an element of a universe".

In summary, while we have a choice to make either kind of equality extensional, it makes more sense to make propositional equality extensional and keep judgmental equality intensional.