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).

practicalperspective, internal languages of all sorts are, I think, undeniably useful. Whether or not one believes the law of excluded middle to be "true", it is a fact that it fails in the internal language of general toposes, and that internal language is a useful tool when studying such toposes. Even more basic logical laws like contraction and weakening fail in the internal languages of monoidal categories, yet the resulting "linear logics" are again a useful tool in their study. $\endgroup$ – Mike Shulman Jun 11 '18 at 18:41