In a Bishop setting without any form of choice, while PUC does not hold generally, there are codomains for which it is provable, in a way that perhaps feels trivial. For the simplest example I can think of, given some set $B$ (equipped with an equality relation), consider the set of singleton subsets of $B$, $$S(B) := \{ X \in \mathscr{P}(B) \mid X \text{ inhabited and } x = y \text{ for all } x,y \in X\},$$
with equality just the usual equality of subsets ($X = Y$ when $x \in X$ iff $x \in Y$). Now, given a total functional relation $R$ over $A \times S(B)$, we can define $f:A \to S(B)$ by $$ f(a) := \{ b \in B \mid \text{for all } Y \in S(B),
 R(a, Y) \text{ implies } b \in Y \}.$$ It is not difficult to show (1) $f(a) \in S(B)$ for $a \in A$, (2) $R(a,Y)$ implies $Y = f(a)$ for $a \in A$, $Y \in S(B)$, (3) $R(a,f(a))$ for $a \in A$, and (4) $f$ respects equality on $A$. That proves PUC for codomain $S(B)$.

This is of course not magic, since we still need a choice function to recover anything from an element of $S(B)$. In a sense, we've just "flattened" two applications of choice into one.

You may well ask why you'd ever want to use this particular codomain, since it's basically just the classical definition of equivalence classes, avoiding which was the whole point of Bishop's idea of sets equipped with equality relations. Well, for basically the same reason as for $S(B)$, PUC is provable for the codomain of the Dedekind reals.

Another example of a codomain for which PUC is provable is Richman's construction of the completion of a metric space $X$ as a subset of $\mathbb{Q}^{+} \to \mathscr{P}(X)$ satisfying Cauchy-like criteria [1]. It's notable that Richman's motivation for the construction was to avoid (countable/dependent) choice. (I've also seen this construction referred to as Cauchy approximations.) I would argue that the "best" definition of metric completion is the terminal object of an appropriate category (specifically, the objects under a metric space $X$ in the category of dense isometries). If you accept that, then it follows that PUC is provable when the codomain is a metric completion, at least in this foundational setting (since Richman's construction has the corresponding universal property).

So, at least in this foundational setting, large swaths of mathematics (particularly analysis) remain unchanged without PUC, since it is simply provable (in perhaps an unsatisfying way) for many codomains of interest, particularly the reals and any other complete metric space.

[1] <cite authors="Richman, Fred">_Richman, Fred_, [**Real numbers and other completions**](http://dx.doi.org/10.1002/malq.200710024), Math. Log. Q. 54, No. 1, 98-108 (2008). [ZBL1134.03041](https://zbmath.org/?q=an:1134.03041).</cite>