The principle of unique choice

[Ulrik Buchholtz]

At the wonderful and recently concluded 7th Workshop on Formal Topology in
Venice, Giovanni Sambin expressed a desire to have a thorough discussion on the
status of the principle of unique choice (AC!). I promised to initiate this here
on constructive-news, and I'm hereby fulfilling this promise.

After some preliminaries, I'll discuss (1) what I take as the informal meanings
of types, functions, and AC!, and then (2) move on to models and formal
systems. There I also have a mathematical question relevant to AC!. Some
readers might want to just skim (1) and skip ahead to (2).

In Venice, we were mainly discussing AC! in the setting of neutral (and
minimalist) constructive mathematics. This can be explicated either via aiming
for the broadest range of possible models, or by being very parsimonious with
one's philosophical commitments. (These are of course related!)

(1) Informal understanding of types and functions

Putting my cards on the table, on my preferred informal understanding of the
notions of types and functions, AC! is simply true, because it's provable. I
know I share this conception (the univalent one) with many practitioners, so
nothing I say here is new; I'm merely repeating the argument for the sake of our
discussion.

On this conception, types and terms/elements are primitive notions in
constructive mathematics. Uniqueness is understood as contractibility: a type A
has a unique element if we have a : A and for every x : A, we have p : a = x,
where = refers to the Martin-Löf identity type.

In general, types are given to us extensionally, meaning any construction on
types respects equivalences. That is, given a type A, the type of pairs (B, e)
of a type B and an equivalence e : A ≃ B, is contractible/has a unique
element. To make sense of this, we of course need a universe U of (small) types,
and the statement is equivalent to univalence of U. (The type A ≃ B is the type
of pairs (f, w), where f : A → B is a function and w a witness that f is an
equivalence, meaning for all y : B, the preimage type, consisting of pairs
(x, p) with x : A and p : f x = y, is contractible.)

Likewise, functions f : A → B are given to us extensionally, i.e., function
application, f x, for x : A, is meaning-determining for the function type. From
this, we deduce informally that any construction on functions respects pointwise
identification of functions. That is, given f : A → B, the type of pairs (g, h)
of a function g : A → B and a pointwise identification h : Π x : A, f x = g x,
is contractible. This is equivalent to function extensionality. (The same holds
for Π-types.)

Now AC! states that the map φ that associates to any f : A → B its graph,
Graph(f) : A → B → U, where Graph(f) x y := (f x = y), is an embedding with
image FunRel(A,B), consisting of those type-valued relations R : A → B → U
satisfying for every x : A that the type of pairs (y, r) of y : B and r : R x y
is contractible. The proof is standard: One version notes that FunRel(A,B) is
equivalent to the type of quadruples (R, p, q, h), where
  R : U, p : R → A, q : R → B,
and h witnesses that p is an equivalence. But then we can contract away the
triple (R, p, h), replacing them by A, the identity on A, and the trivial
witness that the identity is an equivalence. We end up with only q : A → B, and
note that going back along this equivalence exactly recovers φ.

So AC! is just true. Note that we didn't talk about sets and propositions at
all. Propositions and sets are derived concepts: A type is proposition if any
two elements can be identified. This captures the informal meaning of a
proposition as a truth-value, a type whose meaning is determined just by whether
it is inhabited, without regard for the identity of an inhabitant. Likewise, a
type is a set if its identity types are propositions.

If A and B are sets, then φ restricts to a bijection between the type A → B and
the type of total functional proposition-valued relations R : A → B → U. This
statement doesn't need full univalence, only univalence for propositions, i.e.,
propositional extensionality.

Note that we are free to assume (or not) any intensionality principles, e.g.,
that any type or function comes with some intensional presentation (for example,
an operation determining the function). But that doesn't impact any of the
above, which has to do with the extensional concepts. As such, I take the above
to be valid in neutral constructive mathematics. In any case, such assumptions
would go against the minimalist spirit.

(2) On models and formal systems

If AC! is true, then how could it be up for discussion? One way would be to deny
univalence (or propositional extensionality), or function extensionality. But
then it would be recovered as soon as we can form the real/univalent universes
of types and propositions, and function types, as (higher) quotients of the less
extensional ones. So I leave this option aside.

Another way would be to take another notion of proposition as a primitive
alongside types, as in the minimalist foundation (MF) proposed by Milly and
Giovanni (or the Prop universe in Rocq). Let's call these the
m-propositions. The task is then to relate the m-propositions to the types (and
the standard propositions among them).

Note that the version of AC! given above in (1) still holds, of course, but
another version (m-AC!) for sets A and B is possible, using m-total functional
m-proposition-valued relations. For this to have any chance, we surely need B to
be an m-separated set, i.e., have identity types be m-propositions. It seems we
need m-propositions to embed into the propositions to even state this.

I'll get to straight to the point now: The setup reminds us both of
Lawvere–Tierney topologies m, and of quasitoposes, and it's well known that
Grothendieck quasitoposes precisely arise as the m-separated objects for a local
operator m on a Grothendieck topos. See Johnstone's Elephant, C2.2.13.
(I don't know if this holds predicatively. For higher quasitoposes, it's a proposed definition, see: https://ncatlab.org/nlab/show/%28infinity%2C1%29-quasitopos)

This seems to capture the connection we seek between propositions and
m-propositions: the latter are those in the image of a Lawvere–Tierney local
operator m on the propositions.

But there might be many such operators, so why should we single out any m as
primitive? Different applications might need different m-s. And just as often,
we don't need any particular m, and can just work with all propositions: m = id.

Also note that we now have that m-AC! holds if and only if m = id. So in most
of these cases it fails, and that's expected.

Let me end with a mathematical question: The cited result is about Grothendieck
quasitoposes; is it true that any predicative quasitopos arises as the
m-separated objects for an operator m on a predicative topos? (We can vary the
question for different notions, including higher ones.)

If not, and there's a quasitopos model of interest that doesn't arise this way,
then perhaps that could motivate having primitive m-propositions. But more
generally, why stop at primitive m-propositions, and not primitive
m-types/m-sheaves in general? If we insist of having identity types be m-sheaves
(as for the usual identity type in MF/Rocq), we need m-sheaves at higher levels
in order to have m-separated types at higher levels, as well.

Looking forward to the ensuing discussion; kind regards,
Ulrik

[Martin Escardo]

To give more context, this discussion started because in my talk at that
workshop I said I was working in "neutral" mathematics.

Then Giovanni rightly objected, because in my chosen formal foundation
unique choice is a theorem, whereas in his chosen formal foundation it
is (deliberately) independent.

I used the terminology "neutral" in analogy with Euclidean geometry.
Neutral geometry is Euclidean geometry with the parallel postulate
removed. In my case, I am removing excluded middle (and hence general
choice, as it implies excluded middle).

But, of course, there are many foundations for constructive mathematics,
corresponding to different philosophies and/or different mathematical
points of view.

So neutral in the sense of keeping excluded middle open is relative to
the "coordinate system" for constructive/classical mathematics one is
positioned at.

But let me emphasize one technical point regarding Ulrik's discussion
below. Even in minimalistic foundations, unique choice does hold *if* we
adopt the point of view, from the user perspective, that "proposition"
shall mean "type with at most one element". (Users can always use a
system in unintended ways, and they often do, like HoTT people use MLTT
in unintended ways.)

So I think that, perhaps, the real point of discussion is "what kind of
proposition we are willing to consider, from philosophical and/or
mathematical considerations".

For one kind of proposition, unique choice is (deliberately)
independent. For the other, it just holds, because we can prove it.

And Ulrik discussed extensionality. But actually it is not needed to
formulate or prove unique choice in *pure* MLTT (with uniqueness
*defined* as in HoTT, without using any HoTT axioms on top of MLTT).

To wit, here is the simple proof, written in my 2019 lecture notes for MGS:

https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#simple-unique-choice

In these lecture notes there are *no* postulates. We work in MLTT, and
whenever I use any HoTT axiom, it is given explicitly as an *assumption*
for any theorem, and there is no such assumption in the link given above
for the proof of unique choice.

So this is a theorem of pure MLTT, with (1) the notion of proposition
formulated (in MLTT) as in HoTT, and (2) the proof given in pure MLTT.

I believe this can be done in minimalistic foundations, although I am
not an expert in this subject, for this different notion of proposition.

Best,
Martin

> --
> You received this message because you are subscribed to the Google
> Groups "constructivenews" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to constructivene...@googlegroups.com
> <mailto:constructivene...@googlegroups.com>.
> To view this discussion visit https://groups.google.com/d/msgid/
> constructivenews/7b3abf66-f8c2-448d-
> a7db-618cbcb42595n%40googlegroups.com <https://groups.google.com/d/
> msgid/constructivenews/7b3abf66-f8c2-448d-
> a7db-618cbcb42595n%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Thorsten Altenkirch (staff)]

I think the issue really comes down to what we mean by a proposition.

If we treat propositions as a primitive, independent notion (for example as a separate universe that may also be related to types), then there is no particular reason for unique choice to hold.

However, if we start from types and define propositions as types with at most one element, then unique choice becomes derivable. In that setting, it is not an additional principle—it is simply a theorem.

This reflects a broader methodological difference. In classical mathematics, one typically starts with propositions and then identifies collections (sets) with predicates, following Cantor. In type theory, we proceed in the opposite direction: we start with types (as collections), and propositions emerge as a special class of types.

From this perspective, unique choice is quite natural. It provides a clean bridge between functions in type theory and functional relations, by ensuring that every total relation with a unique output determines a function.

Of course, usefulness alone is not a sufficient reason to adopt a principle. But in this case, unique choice is both mathematically useful and philosophically well-motivated—at least if one adopts the “propositions-as-types” viewpoint.

A practical example of this came up recently when I formalised parts of my automata theory course in Lean. In Lean, propositions form a separate universe (Prop), and while classical choice is postulated, the constructive version of unique choice is not derivable.

This leads to some friction. For instance, when defining finite automata, I work with finite types. In Lean, finiteness is expressed as the existence of an enumeration (a propositional statement). From this, one would expect to obtain decidable equality. However, without unique choice, this extraction is not available automatically. As a result, one has to carry both finiteness and decidable equality explicitly and prove that both are preserved under constructions.

This duplication feels unnecessary and is exactly the kind of situation where unique choice would streamline the development.

To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/constructivenews/b39c790f-b3ca-46a1-beea-4d71b102ad44%40gmail.com.

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please contact the sender and delete the email and attachment. Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham. Email communications with the University of Nottingham may be monitored where permitted by law.

[Martin Escardo]

One thing to be remembered is that usually it is accepted that there is
*only one* classical mathematics, but it is also a fact that there are
many varieties of constructive mathematics (in fact, there is a book
with that title, and this nice book is already out of date, because
there is at least one new variety of constructive mathematics in the
last decade).

I also highly value the Formal Topology workshops I've attended (all of
them, except the first one), which has encouraged, since the beginning,
the interaction with all kinds of mathematicians, including classical
mathematicians, and including constructive mathematicians of different
varieties.

I've learned from *all* of them.

In particular, I learned mathematics from them, even if I don't
necessarily agree with their philosophy.

We don't need to agree with philosophical points of views in order to
agree with our mathematics.

My practical understanding, to repeat, is that although we all probably
disagree philosophically, we make great mathematical progress *together*.

I have observed and experienced this in practice, in both directions
classical <-> constructive, repeatedly.

Maybe some of you will think that there is a unique, ultimately correct,
constructive mathematics. Instead, I think, both in practice and
philosophically, that there is only *one* mathematics, which includes
all kinds of mathematical thoughts.

So, maybe: we had enough of Hilbert vs. Brouwer. Let's not repeat
history discussing why my variety of constructive mathematics is better
than yours.

If you disagree with my philosophical point of view, I will still be
your friend, and I am sure I will learn from your mathematics,
independently of your point of view.

M.

[Maria Emilia Maietti]

Dear Martin,

Many thanks for sharing your thoughts.

I completely agree with what you wrote below.

One of the research goals in Padova  is to employ the Minimalist
Foundation (and its fragments)  as a tool to study and compare the
pluralist variety of foundational approaches to mathematics.

Many thanks to  Ulrik and Thorsten's contributions as well.

More on this in the near future

Best wishes to all!

Milly

[dugbr...@gmail.com]

Well said, Martin!

The danger is that even constructive mathematicians can lapse into the attitude that there is only one constructive mathematics. We must avoid that.

Best wishes from down under,
Douglas

25 Apr 2026 06:35:36 Martin Escardo <escardo...@gmail.com>:

To unsubscribe from this group and stop receiving emails from it, send an email to constructivene...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/constructivenews/9fe72f8d-fb54-4241-b540-82964dca87df%40gmail.com.

[Steve Vickers]

The View from Ultraminimalism!

Summary: There are weak forms of AC! that are unobjectionable because they are essentially just defining certain notions. A stronger form is definitely questionable.

Obviously I want to be circumspect about arguments formalized with negative connectives available, so let me try to set out more informally what AC! might be understood to mean.

Using Giovanni’s “function” and “operation”, let’s say AC! means every function (total single-valued relation) is, or at least comes from, an operation equipped with computation instructions.

The two notions live at opposite ends of the denotational semantics map [[-]] and so are distinct. Maybe for a more accurate comparison we want to place operations more in the middle as the image of [[-]], programs modulo meaning, independent of implementation. (Topologically there problems in doing that.) We may then believe that every function is an operation, but we cannot exploit that in higher-order functional programming because we cannot access the instructions. The practical consequence is that in our use of the function we don’t care whether it was computed or generated by some kind of free choice demon. AC! holds in a weak form because in our role as user we are prevented from distinguishing in use between functions and operations.

I suggest there is an analogous, though different, weak form constructively. There you might say that the very definitions of single-valuedness and totality should imply that in proving them we have already demonstrated an operation. Is that what Ulrik was suggesting, that AC! Is just true? Again it is a weak form. In our role as constructive mathematicians we are prevented from distinguishing in proof between functions and operations.

Finally, there is an observational story, and again its AC! is weak. The graph of a function is defined observationally, but its functionhood is not observable. It is an axiom in a geometric theory, an assumption about how your observations fit together. As I mentioned, the axioms can make the theory falsifiable in a Popperian sense, by looking at what can be derived from them and seeking a negation φ |- false of an actually observed φ. Those derivations are done using categorical logic to give a Set-like classifying gadget, a topos or an AU, in which the morphisms are _defined_ as the total, single-valued relations, no reference to operations. That these categories are balanced, an apparent AC!, is weak. It is simply an expression of our focus there on the observational side (done prior to constructive considerations so that the topological issues are also clear and transparent).

Milly has some relevant ideas here that I don’t yet fully understand. I’ll say what I think they are so that she can correct me if I’ve got it wrong. She finds the balance of AUs questionable because it implies AC!, and she would like to generalize to some kind of quasi-AUs where the operation-function distinction is apparent in the one category. My own feeling is that we can probably do without the quasi-AUs if we look at AUs internal in other AUs: then (I conjecture) the constructive notion of operation can be found in the way the external AU sees the internal one.

All the best,

Steve.

[Maria Emilia Maietti]

Dear all,

Many thanks to Ulrik for starting the discussion on unique choice.

In this email, I would like to add a few comments to what has been written by Thorsten and Martin on the topic.

Before I do a quick summary:

in current dependent type theory we can distinguish at least three kinds of  existential quantifiers:

1. The existential quantifier of the Minimalist Foundation or of the Calculus of Constructions, with no choice principles at all (see https://www.math.unipd.it/~maietti/papers/ch.pdf and loc. cit.).

==================================

2. The existential quantifier of Homotopy Type Theory, as h-propositions, or in the internal dependent type theory of regular categories, pretopoi, or topoi
   – see p. 25 of https://www.math.unipd.it/~maietti/papers/tumscsrev.pdf

=========================

3. The existential quantifier of Martin-Löf type theory

=======================================

In all of these settings, we identify:

• propositions as some types in (1)
• propositions as mono types / h-props in (2)
• propositions as types in (3)

So I agree with Thorsten's 

On 23/04/26 19:34, 'Thorsten Altenkirch (staff)' via constructivenews wrote:

I think the issue really comes down to what we mean by a proposition.

If we treat propositions as a primitive, independent notion (for example as a separate universe that may also be related to types), then there is no particular reason for unique choice to hold.

However, if we start from types and define propositions as types with at most one element, then unique choice becomes derivable. In that setting, it is not an additional principle—it is simply a theorem.

Furthermore, I found it very helpful to use the theory of Lawvere doctrines to analyze these three quantifiers, in particular the notion of an existential elementary doctrine with weak full comprehension as a basic abstract tool.

This allows us to prove that:

• (2) is an instance of the existential quantifier of the subobject doctrine of a suitable syntactic regular category.

Moreover, as a doctrinal theorem, we can prove that:

Any existential elementary doctrine with full comprehension is the subobject doctrine of a regular category if and only if the rule of unique choice holds (due to B. Jacobs).

See Section 5.3 of https://www.math.unipd.it/~maietti/papers/mpr_tmj_rev.pdf

• (3) is an instance of the existential quantifier of the weak subobject doctrine of a weakly lex category with finite products.

And, again as a doctrinal theorem, we can prove that:

Any existential elementary doctrine with full comprehension is the subobject doctrine of a regular category if and only if the rule of choice holds.

See Section 5.9 of https://www.math.unipd.it/~maietti/papers/mpr_tmj_rev.pdf

In the above, we speak of choice rules rather than choice axioms, since choice rules imply the corresponding choice axioms in the mentioned type theories (see again https://www.math.unipd.it/~maietti/papers/ch.pdf).

Therefore, I agree with what Martin writes here:

On 23/04/26 18:00, Martin Escardo wrote:

 

And Ulrik discussed extensionality. But actually it is not needed to formulate or prove unique choice in *pure* MLTT (with uniqueness *defined* as in HoTT, without using any HoTT axioms on top of MLTT).

To wit, here is the simple proof, written in my 2019 lecture notes for MGS:

https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#simple-unique-choice

In these lecture notes there are *no* postulates. We work in MLTT, and whenever I use any HoTT axiom, it is given explicitly as an *assumption* for any theorem, and there is no such assumption in the link given above for the proof of unique choice.

So this is a theorem of pure MLTT, with (1) the notion of proposition formulated (in MLTT) as in HoTT, and (2) the proof given in pure MLTT. 

And also here

On 23/04/26 18:00, Martin Escardo wrote:

I believe this can be done in minimalistic foundations, although I am not an expert in this subject, for this different notion of proposition.

Yes, in the extensional level of the Minimalist Foundation in

https://www.math.unipd.it/~maietti/papers/tt.pdf

where propositions are identified as **some type** (which corresponds to create a doctrine of propositions enjoying a form of weak comprehension) 

 one can consider:

• the doctrine of intended propositions with no choice principles,
• or the subobject doctrine of the underlying regular category, identifying propositions with mono types for which unique choice holds,
• or the weak subobject doctrine of the underlying weakly lex category, identifying propositions with sets for which the choice rules/principles hold.

Many thanks,
Milly

---

[Maria Emilia Maietti]

Any existential elementary doctrine with weak full comprehension is the weak subobject doctrine of a weakly 

lex finite product category  if and only if the rule of choice holds.