I am going to draw heavily from Github discussion on HoTT book pull request 617.
There are different kinds of equality. Let us say that equality is "intensional" if it distinguishes objects based on how they are defined, and "extensional" if it distinguishes objects based on their "extension" or "observable behavior". In Frege's terminology, intensional equality compares sense and extensional equality compares reference.
To use Russell's example, intensionally the morning star and the evening star are clearly not the same (because their definitions are different), but they are extensionally the same because they both denote the same object (planet Venus). A more mathematical example is comparison of $x + y$ and $y + x$. These are extensionally equal, but intensionally differ because (the usual) definition of $+$ treats its arguments asymmetrically. It should be clear that two functions may be extensionally equal (have same behavior) even though they differ intensionally (have different definitions).
It is possible for two kinds of equality to coexist. Thus in type theory there are two equalities. The intensional one is called "judgmental" or "definitional equality" $\equiv$ and the extensional one is known as "propositional equality" $=$. Mathematicians are aware of $=$ as a "real thing" while they think of $\equiv$ as "formal manipulation of symbolic expressions" or some such.
We may control the two kinds of equality and the relationship between them with additional axioms. For instance, the reflection rule collapses $\equiv$ and $=$ by allowing us to conclude $a \equiv b$ from $a = b$ (the other direction is automatic). There are also varying degrees of extensionality of $=$. Without any extra axioms, $=$ is already somewhat extensional. For instance, we can prove commutativity of $+$ on natural numbers by induction in the form $x + y = y + x$, but we cannot prove $x + y \equiv y + x$. Function extensionality is an axiom which describes what constitutes an "observation" on functions: by saying that two functions are equal when they give equal values we are in essence saying that only values matter (but not for example the "running time" or some other aspect of evaluation). Another axiom which makes $=$ "more extensional" is the Univalence axiom.
It is hard to do mathematics without function extensionality, but type theorists have their reasons for not including it as an axiom by default. But before I explain the reason, let me mention that there is a standard workaround. We may introduce user-defined equalities on types by equipping types with equivalence relations. This is what Bishop did in his constructive mathematics, and this is what we do in Coq when we use setoids. With such user-defined equalities we of course recover function extensionality by construction. However, setoids are often annoying to work with, and they drag in technical problems which we would prefer to avoid. Incidentally, the setoid model shows that function extensionality does not increase the power of type theory (it is a model validating function extensionality built in type theory without function extensionality).
So why don't type theorist adopt function extensionality? If we want to have a type theory with nice properties, and a useful proof assistant, then $\equiv$ should be "easy" to deal with. Technically speaking, we would like a strongly normalizing $\equiv$. By assuming function extensionality we throw into type theory a new constant funext without explaining how it interacts with the process of strong normalization, and things break. Type theorists would say that we failed to explain the computational meaning of funext.
Consequently, Coq does not adopt function extensionality because that would lead to a lot of problems. Coq would not be able to handle $\equiv$ automagically anymore, and the whole system would just have worse behavior. Type theorists of course recognize that having a good computational explanation of function extensionality, and more generally of the univalence problem, would be extremely desirable. This is why the HoTTest open problem is to give a computational interpretation of the univalence axiom. Once this is accomplished, we ought to have at our disposal type systems and proof assistants which are much more natural from a mathematician's point of view. Until then, you can always assume funext as an axiom and work around the resulting complications. To see how this can be done, have a loot at the Funext axiom in the HoTT library.
[This P.S. is outdated after the question was edited.] P.S. The title of your question points to a common leap of reasoning from "not accepting function extensionality" to "denying function extensionality". While there are models in which function extensionality has counter-examples, one should be aware of the difference between "not accept" and "deny". (I am complaining because this sort of leap is often made about the law of excluded middle, and there it leads to absurdity.)
Best Answer
There are a couple of very similar statements that all work out:
A more round-about way which works at least in computable analysis even allows to make case distinctions here. (Classical metatheory from here on). We can use the three-valued space $\mathbb{T}$ with underlying set $\{\bot,0,1\}$ and topology generated by $\{\{0\},\{1\}\}$. Given $x,y \in \mathbb{R}$ with $xy = 0$, we can compute $c(x,y) \in \mathbb{T}$ where $c(x,y) = 0$ if $y \neq 0$, $c(x,y) = 1$ if $x \neq 0$ and $c(0,0) = \bot$.
For any reasonable[1] space $\mathbf{X}$, the map $\operatorname{Merge}_\mathbf{X} : \subseteq \mathbb{T} \times \mathbf{X} \times \mathbf{X} \to \mathbf{X}$ defined as $\operatorname{Merge}_\mathbf{X}(0,x,y) = x$, $\operatorname{Merge}_\mathbf{X}(1,x,y) = y$ and $\operatorname{Merge}_\mathbf{X}(\bot,x,x) = x$ will be computable. Note that $\operatorname{Merge}_\mathbf{X}(\bot,x,y)$ is undefined if $x \neq y$.
Thus, we are allowed to make a case distinction according to the zero product property in computable analysis, as long as we end up with the same result no matter which case we pick if they are both true (and as long as the result lives in a reasonable[1] space). This is not really specific to the zero product property, but more a general case of being able to get away with something that may at first glance look like using $\mathrm{LLPO}$.
[1] Reasonable spaces include the computably admissible ones, as well as any other example I'm aware of anyone would want to be working with. It doesn't work for everything though.