The principle of unique choice
Ulrik Buchholtz
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
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 view this discussion visit https://groups.google.com/d/msgid/constructivenews/b39c790f-b3ca-46a1-beea-4d71b102ad44%40gmail.com.
Martin Escardo
*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
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
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
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:
- 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.).
==================================
- 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
=========================
- 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
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:
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
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.
Martin Escardo
Thanks a lot for your message.
So I am thinking we are all in agreement? And at the same time
understanding the differences?
In any case, what I would like to reiterate, regardless of
"constructive" or "neutral" foundations, my talk was about the
surprising fact that there are plenty of infinite exhaustively
searchable infinite sets in all varieties of constructive mathematics,
which correspond to Stone spaces in classical mathematics.
In particular, the searchability of these infinite sets don't depend on
Browerian axioms or unique choice.
I believe this fact survives *any* foundation of constructive
mathematics, and that it applies, in particular to informal mathematics
in the hands of Brouwer or Bishop.
When I said "neutral" in my abstract for my talk, this is what I meant.
The infinite sets that I prove to be searchable survive any possible
interpretation of mathematics, constructive or not.
This is a very strong claim, I realize, but I stand by it.
All the best,
Martin
On 01/05/2026 09:33, Maria Emilia Maietti wrote:
>
> 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
>
> 1. The existential quantifier of the Minimalist Foundation or of the
> www.math.unipd.it/~maietti/papers/ch.pdf> and loc. cit.).
>
> ==================================
>
> 2. The existential quantifier of Homotopy Type Theory, as h-
> categories, pretopoi, or topoi
> – see p. 25 of https://www.math.unipd.it/~maietti/papers/
>
> =========================
>
> 3. The existential quantifier of Martin-Löf type theory
> =======================================
>
>
> In all of these settings, we identify:
>
> * 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:
>>
>> 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.
>>
>> 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:
>
>
> 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/
>
> * (3) is an instance of the existential quantifier of the weak
>
> And, again as a doctrinal theorem, we can prove that:
>
> 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.
>
> See Section 5.9 of https://www.math.unipd.it/~maietti/papers/
>
> In the above, we speak of /choice rules/ rather than /choice axioms/,
> mentioned type theories (see again https://www.math.unipd.it/~maietti/
> 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:
>
> * or the subobject doctrine of the underlying regular category,
> rules/principles hold.
>
> Many thanks,
> Milly
>
> <https://groups.google.com/d/msgid/constructivenews/aeb553af-d477-4e14-
> a4ff-2df8fa5d4e69%40math.unipd.it?utm_medium=email&utm_source=footer>.
Maria Emilia Maietti
Dear Martin and all
So I am thinking we are all in agreement? And at the same time understanding the differences?
Yes, with the proviso of choosing the weakest foundation available to support your “neutral” statement. For what you are doing, it seems to be the Minimalist Foundation, or some fragment of it with reduced induction, if we want to analyze the statement in the spirit of constructive reverse mathematics.
But unfortunately, we have neither the funding nor the people to build a proof assistant for the Minimalist Foundation.
In any case, what I would like to reiterate, regardless of "constructive" or "neutral" foundations, my talk was about the surprising fact that there are plenty of infinite exhaustively searchable infinite sets in all varieties of constructive mathematics, which correspond to Stone spaces in classical mathematics.
In particular, the searchability of these infinite sets don't depend on Browerian axioms or unique choice.
I believe this fact survives *any* foundation of constructive mathematics, and that it applies, in particular to informal mathematics in the hands of Brouwer or Bishop.
“Any” is always difficult to motivate; for example, what about formalizing your statement in the initial arithmetic universe?
Working in the Minimalist Foundation guarantees compatibility with both Bishop’s and Brouwer’s constructive approaches.
When I said "neutral" in my abstract for my talk, this is what I meant.
The infinite sets that I prove to be searchable survive any possible interpretation of mathematics, constructive or not.
This is a very strong claim, I realize, but I stand by it.
I would choose a foundation where to state it as a clear proof of it in the spirit of constructive reverse mathematics.
Many thanks!
Milly
Maria Emilia Maietti
Dear Ulrik
many thanks again for your message where you state some very important questions.
For now, I would like to add two comments.
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
preservation of predicativity with the addition of the law of excluded middle on propositions
which holds for the Minimalist Foundation (MF), as proved in
https://www.math.unipd.it/~maietti/papers/equimf.pdf
This is a striking property of MF, since the addition of the law of excluded middle makes most predicative foundations, including Homotopy Type Theory and Martin-Löf’s type theory, impredicative, as described in the paper
https://arxiv.org/abs/2407.04161
in Pillars of
Enduring Strenght, Learning from Hermann Weyl",
edited by L. Crosilla, O. Linnebo and M.
Rathjen,
in the series `Logic and Computation in
Philosophy', chapter 13, p.239-263, OUP, 2026.
Indeed, any Boolean locally cartesian closed pretopos is a topos.
(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.
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 we omit the word “predicative,” candidates for a counterexample could be the two constructive quasitoposes of assemblies described in
https://www.math.unipd.it/~maietti/papers/ECQT-MaiettiSabelliTrotta26.pdf
Because of the absence of choice principles in the meta-theory, these assemblies do not share all the properties of classical assemblies.
These constructive quasitoposes could be made predicative using Aczel's Constructive Zermelo–Fraenkel set theory, but this is still work in progress.
Yet another candidate as a counterexample is the quasitopos defined as the elementary quotient completion over the Calculus of Constructions, as mentioned at the end of Remark 7.8 in
https://www.math.unipd.it/~maietti/papers/quLU.pdf
Many thanks for your very interesting questions!
Milly
Martin Escardo
Thanks for your thoughtful message, Milly.
I will never use the terminology "neutral" again, I promise.
In any case, I am sad that what I really wanted to say in my talk got lost in this secondary discussion. Which is my fault, of course. In TypeTopology I use "spartan" as a characterization of what is done there, which is perhaps better, because there isn't an absolute measure of spartannes, but people may think that neutrality is absolute.
(I have trouble perceiving neutrality as absolute, though.)
All the best,
Martin
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/bd84d4aa-a860-4c48-b0b0-0078057bd32a%40math.unipd.it.
andrej...@andrej.com
first let me say it is a delight to see some activity around here, I much enjoy reading the posts.
I believe nobody has mentioned yet the fact that there are foundational setups in which unique choice is sacrificed so that a particular combination of principles can be admitted. I have in mind of course Yannick Forster’s synthetic computability, where the setup is:
1. An abridged version of the Calculus of Constructions: ∏ ∑ Id ℕ Bool, and an impredicative Prop (I might be forgetting a detail or two, and I am not sure how important impredicativity is).
2. Excluded middle for Prop.
3. Synthetic Church’s thesis stating that (abstractly, without using Kleene’s T and U) there is a universal map such that every f : ℕ → ℕ is computed by it.
The second and third principle are at odds with each other, thanks to Cantor’s diagonalization method – but only if we throw in unique choice! And since computability theory predominantly specifies functions in terms of computations, i.e., λ-terms, unique choice is not missed much. Yannick and his coworkers have developed an impressive amount of computability theory this way, and they also formalized it all.
In my opinion this is a very good reason for seriously considering mathematics without unique choice. Philosophy is inspiring but mathematics is undeniable.
With kind regards,
Andrej
Maria Emilia Maietti
Dear Martin,
Thank you very much for indirectly stimulating the discussion on
unique choice, started by Giovanni Sambin at the workshop and
continued by Ulrik on this list.
I hope that a video of your talk at the workshop will be made
available on YouTube sooner or later, so that many others can
enjoy it as much as I did.
All the best to you and everyone for a happy research!
Milly
Maria Emilia Maietti
Many thanks for remembering Forster’s synthetic computability!
Pietro Sabelli and I are currently showing how to model this approach
in suitable quasi-toposes, including that of classical assemblies within
Hyland’s Effective Topos.
Instead, the already mentioned "constructive" quasi-toposes of
assemblies in
https://www.math.unipd.it/~maietti/papers/ECQT-MaiettiSabelliTrotta26.pdf
should provide a model for the Calculus of Constructions with Synthetic
Church’s Thesis, called Type-Theoretic Church Thesis in our paper,
together with all Brouwerian principles.
This opens the way to intuitionistic synthetic computability and to
reconciling a restricted form of Markovian constructivism with
Brouwerian intuitionism.
Furthermore, adding unique choice makes the Synthetic Church’s Thesis
inconsistent with Brouwerian principles such as the Fan Theorem, by
Kleene’s well-known argument.
Therefore, all this provides another reason to avoid unique choice in
constructive mathematics in order to pursue intuitionistic synthetic
computability.
Many thanks for your attention!
Best wishes to everyone!
Milly
Martin Escardo
Thanks for the warm words, Milly. All the best, Martin
Giovanni Sambin
Dear All,
I apologize for the delay in replying, all the more so because I was the one who proposed this discussion. I hope it has been clear that my silence was due to circumstances beyond my control. During the last few days, the delay has also been due to the difficulty of addressing, in a sufficiently clear and comprehensive way, a topic that involves fundamental aspects of my conception of mathematics. To avoid further postponements, in this first contribution I shall focus on the thesis put forward by Ulrik. Many of the remarks that follow are already developed in the subsubsection “An effective notion of function” (pp. 65–68) of PTbook.
Ulrik recalls that, in the UF conception of the notions of type and function, AC! is simply true because it is provable. In my view, however, the problem is that this proof is based on assumptions that are more controversial than AC! itself.
As Ulrik recalls, in UF propositions and sets are derived concepts. The point is that this reduction is by no means innocuous or neutral. As Thorsten and Milly have pointed out, it is precisely through the identification of propositions with types having a unique element that the validity of AC! is introduced. In MLTT, the constructor \Sigma requires an operation that produces the witness; consequently, by identifying \exists with \Sigma, AC! becomes derivable.
My objection is that, in doing so, one loses a distinction that precedes any formal system and belongs to reality itself: the distinction between an existence accompanied by effective instructions that produce a witness and an existence for which one knows that a witness exists, but without possessing such instructions. From this distinction derives the distinction between a lawlike sequence and a choice sequence. In the former case, one has precise instructions for proceeding; in the latter, one positively knows that there exists a way of proceeding, but one does not possess effective instructions for determining it (see the examples on pp. 67–68 of PTbook).
As often happens, discussions about primitive notions tend to be reduced to their expression within a formal system. For me, by contrast, the essential point is exactly the opposite: first one decides which notions to adopt, and only then does one seek the formalism that expresses them in the best way. Reversing this conceptual order means, in my view, being influenced by the paradigmatically negative example of ZFC, where the appeal to a formal system arises from the inability to clarify directly the notion of set. Doing the same in a constructive view means assigning too much weight to the classical framework. For me, constructivism implies the use of notions whose meaning is sufficiently clear even independently of any formalization.
In the Minimalist Foundation - understood here not as a formal system but as a foundational conception - this is possible. In brief:
- set = we possess precise rules that allow us to construct inductively all its elements;
- operation from A to B = a family g(a):B (a:A) of elements of B indexed by A, with equal indices determining equal elements;
- proposition = a statement that can be judged true and for which one knows what what would count as a verification;
- subset of A = a property on A, that is, a proposition with an argument in A;
- relation from A to B = a proposition with one argument in A and one in B;
- function from A to B = a total and single-valued relation;
- collection = a set of objects defined by a known but neither effective nor exhaustive criterion. The main example of a collection is the collection of all subsets of a set.
(If one had not followed the classical demand to reduce everything to sets, such a “naive theory” could already have been adopted at the end of the nineteenth century, avoiding both the paradoxes and the subsequent formalist deviation of foundational debate.)
I do not see why, as constructivists, we should assume that a good foundation - and above all a good explanation of mathematics - must necessarily coincide with a formal system. Is it really necessary to speak about Lawvere–Tierney topologies m or Grothendieck quasitopoi in order to clarify what a proposition is? It does not seem so to me.
In my opinion, a theory is neutral when it is based on assumptions on which everyone, or almost everyone, can agree. Ideally, every foundation should be an extension of such a neutral theory. This is precisely the declared aim of the Minimalist Foundation (with some qualifications, for example concerning Steve’s ultrafinitism). Since even within our community there is no unanimity concerning assumptions such as PSA, AC and AC!, propositions-as-sets, univalence, etc., I do not see why a theory should be called neutral simply because it does not assume LEM.
To say that N is \emptyset, {\emptyset}, {\emptyset,{\emptyset}}, etc., is an artifice that claims to reduce to ZF but explains nothing, since it already requires understanding what is sufficient to understand N directly. Similarly, reducing N to the finite ordinals or to the first infinite ordinal introduces as primitive the concept of an arbitrary ordinal, which is not necessary for understanding the natural numbers.
The same applies to the reduction of propositions to sets in MLTT or to types with a unique inhabitant in UF (it should be noted that, in the informal view, it is by no means necessary to identify a proposition with the set of all its proofs). These are very strong and conceptually non-conservative reductions. They impose a property that conflicts with reality, since in everyday life propositions are used without having any idea how to generate inductively all their verifications, or without assuming that all verifications are equal. Consider, for example, the proposition “I like Bill”, or, in mathematics, “for all x,y,z in N and n>2, x^n+y^n is different from z^n.”
For this reason I do not agree with Martin’s statement that “In these lecture notes there are no postulates. We work in MLTT”, because the principle propositions-as-sets is itself a postulate, neither innocuous nor neutral, and MLTT itself is not part of some universal truth.
One thus ends up delegating to a relatively complex formal system - far more complex than Euclidean geometry and based on a debatable meaning explanation - the task of clarifying the fundamental concepts of mathematics. In my view, this represents a relapse into the formalism through which Hilbert believed he could save mathematics after the trauma of the paradoxes. Does constructivism really have nothing better to offer than axiomatic theories whose meaning is not fully understood because it has only been formally reduced to something else? Certainly the situation is better than in ZFC: the entities are constructed and the theory is consistent. Yet the idea remains of reducing everything to a single concept without adequately explaining the reason for that reduction.
After long reflection (from the early 1970s to the 1990s), I arrived at a conception of constructivism in a strictly human sense - natural, evolutionary, and dynamic - according to which every mathematical entity is the result of a human construction free from predetermined constraints, and justified by its effectiveness in our knowledge of reality and therefore, ultimately, by its evolutionary advantage for the species. Since then, I have adopted this perspective in mathematical practice, especially in topology; PTbook is the result.
In this view, there is no form of reality or truth independent of human constructions (with the qualification that, once the rules of a game or the instructions of a machine have been fixed, their execution does not depend on further creative acts). In particular, there is no formal system fixed once and for all to which all mathematics can be reduced. I have experienced firsthand that this also applies to Martin-Löf type theory, having experienced closely hat it is constructed by a human being and can therefore be improved by other human beings.
The issue, then, is not to gather as much as possible of a truth independent of us, but to organize our knowledge of reality in the best possible way. The relevant question is not which formal system is more powerful or contains more truths, but rather which is better suited to describing reality in a conservative manner.
ZFC is not conservative: no constructivist accepts Banach–Tarski or the well-ordering of the reals. However, another form of non-conservativity is to assume that there is a unique truth, especially if it is supposed to be completely expressible within a single and fixed formal system.
Let us now return to the specific issue of AC!. Quoting Steve, “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.” Thus, assuming that AC! is part of the truth, and therefore that a theory in which AC! does not hold is unacceptable, means, in my view, that one has chosen to give up the distinction between an element of A → B (which I call an operation, and for which extensionality is part of the notion) and a functional relation from A to B (which I call a function).
Yet it is a fact that in real life there exist both operations - that is, situations in which one possesses instructions for computing the output from the input - and functions, in which one merely knows that to each input there corresponds a unique output, without knowing how to determine it. The difference is clearly visible in concrete contexts. In a two-player game, for example, my strategy is for me an operation, whereas the strategy of my opponent Bill is for me only a function. Similarly, one may think of non-computable real numbers, for example, an experimental measurement in physics.
As one can see, what is crucial here is to keep in mind the information one actually has; the 'thing in itself' does not exist in any scientific sense. What exists are the concepts one uses to describe a real situation. To assume AC! as valid means that one cannot distinguish between the information one has about one's own strategy and the information one has about Bill's strategy.
For this reason, treating AC! as a neutral assumption means that the resulting mathematics is unable to deal adequately with situations such as the game with Bill, or that of a physicist who “plays” with nature in order to determine the measurement of some phenomenon. In other words, it means that Brouwer’s choice sequences do not exist as mathematical objects. These are deep consequences and anything but neutral.
The main difficulty perhaps lies in moving from an a priori conception - according to which mathematics exists independently of us -to an a posteriori conception, in which we construct it ourselves and nothing is given in advance as necessary or predetermined.
All this is developed in detail in PTbook. In brief, with respect to MLTT one must abandon the principle propositions-as-sets, otherwise AC and, a fortiori, AC! become provable. With respect to the original formal topology, one must introduce a binary positivity relation in order to ensure that arbitrary paths in Baire space - the geometric version of choice sequences - coincide exactly with the ideal points of a positive topology.
In this way one obtains a notion corresponding to Brouwer’s choice sequences that can enter the mathematical arsenal without any hesitation. Assuming AC!, on the contrary, means excluding this notion; it follows, for example, that the admissible real numbers are only the lawlike ones, as in Bishop and Martin-Löf. This is certainly a possible choice, but one that prevents the expression of the inexhaustible richness and unpredictability of every measurement that can be approximated beyond any predetermined bound.
Ultimately, the question is whether we wish to take into account dynamic information that depends on the individual perspective, or whether we prefer to ignore it in favour of a conception of truth as predetermined, immutable, and absolute.
Thank you all for your attention.
Giovanni
--
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.
To view this discussion visit https://groups.google.com/d/msgid/constructivenews/4b879062-61c2-4524-8312-4f72124d4664%40gmail.com.
Steve Vickers
On 12 Jun 2026, at 16:59, Giovanni Sambin <gios...@gmail.com> wrote:
To view this discussion visit https://groups.google.com/d/msgid/constructivenews/CAADExmuyrEF2OME547WRfMJZojvXpDu_m9NN3V8uyiC0_KsrCQ%40mail.gmail.com.
Giovanni Sambin
Dear Steve,
thank you for your feedback. Your first two questions are relatively easy:
>First, I was talking about "ultraminimalism", not ultrafinitism. I'm sure that was just a typo or an autocorrect.
It is neither a typo nor autocorrect: besides the ultraminimalism you refer to, there is another possible weakening of the minimalist foundation, in which infinity appears in a much more tamed form - ultrafinitism. In my talk at 7WFTop there are 3 slides authored by Mirco Mannucci, in which "resource-bounded positive topology" is mentioned, which is connected to ultrafinitism. From a pluralist perspective, both are absolutely worthy of attention and may prove useful in certain applications. That explains my mistake.
>Second, an operation as a "family" g(a):B (a:A): Have you really explained what a family is? I assumed you meant there to be computation instructions. Did I get that right?
The notion of element a:A (i.e., what can be obtained by an arbitrary finite list of applications of the rules defining A) is implicit in the notion of set A (namely, we possess precise rules that allow us to construct inductively all its elements). A family g(a):B (a:A) (alias an operation from A to B) is nothing other than an element of the set B depending on an index a:A. In detail, to know that g(a):B for every a:A, one must know how to transform the instructions for forming the element a (i.e., the finite list of applications of the rules characterising A as a set) into the rules for forming the element g(a) of B. See PTbook (*), bottom of p. 117.
In other words, g(a):B (a:A) is the information from which, by lambda-abstraction, one obtains a canonical element of A → B; and conversely, from an element of A → B one obtains an operation from A to B by application.
The crucial question is the third, and even a partial answer requires many more words, mainly examples to convey the intuition.
>Third, there were two places where you mentioned "knowing" that a witness exists, without having one. The conceptual basis for such knowledge is surely problematic. It seems to me that, ultimately, it will depend on hypotheses, possibly via logical inference in some system. That is why I stressed the idea of falsifiability: if something you "know" turns out to be false, then there is >something wrong in the hypotheses or the logic.
I am not sure I grasp what you mean. I believe "knowing that a witness exists" is a kind of judgement we all understand and use. It is just the meaning of (∃x:A)φ(x) true when φ is a proposition, if we understand propositions outside the propositions-as-sets principle. This is a "logical" explanation, which makes no reference to any operation. It suffices to say that
(1) (∃x:A)φ(x) true yields ψ true ⟺ z:A, φ(z) true yields ψ true,
for a generic z, that is, without having any specific information about z. The inference rules for ∃ are derived from equivalence (1). This follows a pattern that holds for all logical constants, called the reflection principle(**).
The main idea here (of which I have always been convinced) is that no form of mathematics should be needed in order to understand and correctly use logic (otherwise we could not explain how people with no mathematical background can master logic impeccably). Therefore, an explanation of logic different from prop-as-sets must be employed, and consequently also from the Brouwer–Heyting–Kolmogorov interpretation. This formally accounts for an existence for which one knows that a witness exists, but without possessing instructions to find it.
Informally, there are many real-life situations in which this occurs.
[The following page is taken from: G. Sambin, Unique choice is an option, unpublished and incomplete manuscript, April 24, 2014]
"There are some cases in which one can be sure that a witness exists, also constructively, although the procedure to find it is not expressed by an algorithm. Here are two examples:
1. The first example is a popular short story. The wife of a man of faith falls very sick. Doctors are of no help. One day he starts at 8am and climbs up a mountain to reach a holy man in the evening. When the holy man knows the reason of the visit, his answer is: "Your faith is strong. If tomorrow going down you will find yourself at the same time in the same place as you were to day coming up, your wife will be saved." The pilgrim is smart enough to know that his wife will be saved. Why? Simply, he starts at 8am from top and follows downward the same itinerary he followed the day before upwards. He does not know when, but there exists a time in which he will be in the same place as the day before.
We too can get convinced by performing a simple Gedankenexperiment: imagine to overlap the two days, thus with "two" pilgrims starting at 8am, one from bottom and one from top. Since they follow the same route, they will meet somewhere, and it will be the same time. However, there is no way to know in advance which place and time it will be.
2. The second example occurred to me in reality. I keep the swipe card for entrance in my department in my wallet. To save a few seconds, to open the door I don't take out the card and swipe the whole wallet. [I learnt this from a lady colleague who swipes her whole purse.] One day I was told that my card was going to expire and was given a new card to replace it. I put it in my wallet. I soon forgot the date of expiry (and I also was not sure about which card was new and which was old). Thus I kept both of them in my wallet. To open the door, I swipe the whole wallet as before. This procedure works, since the door opens. In fact, there is one active card, although I don't know which one. [For curious readers: many months later I showed both cards to the administrator and he threw away the useless one.]
There is a procedure to know which of the two cards works, and it is simply to try both of them, separately, every day. The purpose of the example is precisely to show that this extra work (and extra information) is not necessary to open the door."
[From PTbook p. 68:] "An example of such an existence [...] could be the situation where we see our wedding ring falling out of the boat while we are out on a lake. We know with positive certainty that there is a wedding ring in the lake, but we have no effective procedure for finding it."
Two examples are included in PTbook p. 67 when the extension to the case of a ∀∃ quantification is discussed, i.e., the function–operation distinction:
"We know that the value of a function on any argument exists and is unique, but in general we do not know how to obtain it explicitly. In a sense, a function can be thought of as an operation constructed by someone else, who does not, however, share with us the instructions she has used to construct it and we are unable to retrieve them, for example, if the other person is an opponent in a two-player game and the operation is her strategy in choosing moves or if she is the taxi driver who takes us to the airport and the operation is the route she chose so at any fork she knows which way to go. A dynamic view is essential for understanding that in both examples there are two distinct notions: an operation for the other is only a function for us. The static view of an ‘objective truth’ or an object in itself is unable to express the difference in information that the two persons actually have. The crucial question is not to decide which principles are true, but which information is relevant and we wish to keep."
A detailed explanation is contained in PTbook, but it is scattered across the various chapters. Unfortunately, I have not yet written a self-contained and up-to-date article devoted to this topic.
As to your implicit question about positivity relations, alias binary positivities, a complete answer is even more complex, and although the whole PTbook could be described as the result of developing the idea of positivity relations, I expect many more applications will emerge than what is known now.
All the best,
Giovanni
(*) By this abbreviation I refer to my book Positive Topology. A new practice etc., Oxford Logic Guides 57, Oxford University Press, 2025.
(**) See Sambin et al., Basic logic: reflection, symmetry, visibility, J. Symbolic Logic 65 (2000), pp. 979–1013, for the connectives; and Maietti–Sambin, Toward a minimalist foundation for constructive mathematics, in Crosilla and Schuster eds., From Sets and Types to Topology and Analysis, vol. 48 of Oxford Logic Guides, Clarendon Press, 2005, pp. 91–114, in particular pp. 100–102 for the extension of the same idea to quantifiers.
To view this discussion visit https://groups.google.com/d/msgid/constructivenews/1CC4E32A-6822-4800-B5B2-89F0795C1F6A%40hawvick.plus.com.