The principle of unique choice (PUC), also called the principle of function comprehension, says that if $R$ is a relation between two sets $A,B$, and for every $x\in A$ there exists a unique $y\in B$ such that $R(x,y)$, then there exists a function $f:A\to B$ such that $R(x,f(x))$ for every $x\in A$.
In ZF set theory (without the axiom of choice) this principle is provable; indeed it is basically the definition of what it means to be a "function". The same is true in weaker, e.g. intuitionistic set theories, and also for h-sets and h-relations in homotopy type theory / univalent foundations. However, PUC is not provable in (classical or intuitionistic) higher-order logic (HOL) — unless we assert it, or something that implies it, as an additional axiom.
Moreover, there are naturally-arising models of HOL in which PUC fails. For instance, we can take the types to be topological spaces, and the predicates on a space $A$ to be the subspaces of $A$ (subsets with the subspace topology); then a relation $R$ as in PUC corresponds to a span $A \leftarrow R \to B$ in which $R\to A$ is a continuous bijection, but need not have a continuous inverse enabling us to define a continuous map $A\to B$. (To be more precise, it would be better to replace topological spaces by something slightly better-behaved, such as a quasitopos.) We can also take the types to be partial equivalence relations on a partial combinatory algebra, or partial equivalence relations in a tripos.
Constructive mathematicians following Brouwer and Bishop have explored in depth what mathematics looks like in the absence of the full axiom of choice and the law of excluded middle. Usually it's not much different; one just has to take extra care in various places and state various theorems in idiosyncratic ways. Moreover, classical mathematics can be embedded in constructive mathematics, e.g. by judicious insertion of double-negations; thus constructive mathematics is simply "more informative", i.e. it "draws distinctions that classical mathematics ignores".
However, all constructive mathematicians that I know of accept the principle of unique choice. Has anyone seriously explored what mathematics would look like in the absence of PUC? I don't mean simply using the internal language of a quasitopos to prove a few things; I mean a serious development of large swaths of mathematics akin to Bishop's Constructive analysis.
Note that, as is the case with classical and constructive mathematics, ordinary mathematics with PUC should embed into mathematics without PUC by simply interpreting the word "function" to mean a total functional relation as appears in the hypothesis of PUC (which I call an anafunction after Makkai's "anafunctors"). So it seems that mathematics without PUC should again be simply "drawing previously-ignored distinctions", keeping track of which anafunctions are actually functions.
Edit: Frank Waaldijk's answer below points out that I should be more specific about what I mean by "mathematics without PUC", as there is actually more than one way that PUC could fail. In this question I'm thinking about mathematics formalizable (though not necessarily actually formalized) in higher-order logic in one of two ways:
Define "sets" to be types equipped with equivalence relations (or partial equivalence relations), and "functions" to be maps between types ("operations") that preserve these equality relations.
Include "subtypes" and "quotient types" in the logic, and define "sets" to be simply types, and "functions" to be maps between them.
In either case there is also a natural notion of "anafunction", namely a binary relation that is total and functional, and PUC need not hold: not every anafunction is representable by a function. By contrast, we can also formalize mathematics with PUC in HOL in either of these ways by defining a "function" to be such an "anafunction", i.e. a total functional binary relation. For instance, this is what is done semantically in constructing a topos from a tripos.
Frank describes a different approach that is something akin to the following (also in HOL):
- Define a "set" to be a type equipped with both an equivalence relation of "equality" and a compatible binary relation of inequality or apartness, and define a "function" to be a binary relation between types that is total, functional, and reflects inequality (i.e. is "strongly extensional").
Here we appear to take the "anafunction" route by defining a "function" to be a total functional relation, but we also include "strong extensionality" in the definition of "function". Now PUC fails because a total functional relation need not be strongly extensional. This is also interesting, but it is not what I had in mind.
Of course, the two could be combined: we could define a function to be a map of types that is strongly extensional, so that a total functional relation could fail to be represented by a map of types and also fail to be strongly extensional.
Edit 2: Monroe Eskew points out in the comments yet another situation (again, not the one I'm asking about right now) where a version of PUC can fail, namely in ZF-type set theories without the replacement axiom. In that case one can have a class-relation that is functional and whose domain is a set, but whose codomain is not a set, and hence which does not define a function (a function being required to be itself a set).