nLab choice operator

Redirected from "global axiom of choice".
Choice operators

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Choice operators

Definitions

A (global) choice operator is structure included in some foundations of mathematics which provides a uniform way to choose an element of every inhabited set or class.

In Hilbert‘s original formulation, for any property P(x)P(x) we can form a term εx.P(x)\varepsilon x.P(x) such that

x.P(x)P(εx.P(x)).\exists x.P(x) \;\Rightarrow\; P\big(\varepsilon x.P(x)\big).

In other words, if PP holds of anything at all, then it holds of the particular term εx.P(x)\varepsilon x.P(x). A similar operator was used by Bourbaki and appears in FMathL?.

In category theory

In category theory, there are two different notions of logic, the usual external logic, and the internal logic of a category. These different notions of logic leads to different notions of a choice operator in category theory, an external choice operator and an internal choice operator

External choice operator

Let \mathcal{E} be a well-pointed Heyting category. This allows for the objects of \mathcal{E} to behave as sets and morphisms x:Hom (1,X)x:\mathrm{Hom}_\mathcal{E}(1, X) from the terminal generator 11 \in \mathcal{E} to any object XX \in \mathcal{E} to behave as elements of XX. Then Hilbert’s formulation of the external (global) choice operator is rendered as the following: for any object XX \in \mathcal{E} and any property P(x)P(x) on the hom-set Hom (1,X)\mathrm{Hom}_\mathcal{E}(1, X) we can form a morphism ε Xx.P(x)Hom (1,X)\varepsilon_X x.P(x) \in \mathrm{Hom}_\mathcal{E}(1, X) such that

xHom (1,X).P(x)P(ε Xx.P(x)).\exists x \in \mathrm{Hom}_\mathcal{E}(1, X).P(x) \;\Rightarrow\; P\big(\varepsilon_X x.P(x)\big).

This is sometimes used in categorical set theories like ETCS plus epsilon.

Internal choice operator

Let CC be a regular category. This implies that given an object XCX \in C, there is a support object [X]C[X] \in C, defined as the image of the unique morphism X1X \to 1 into the terminal object 1C1 \in C.

An internal (global) choice operator consists of, for every object XX, a morphism ε X:[X]X\varepsilon_X:[X] \to X from the support object of XX to the original object XX.

Hilbert’s original formulation of the choice operator translates over to the internal language of CC into the statement that for every object XX and subobject PXP \hookrightarrow X, there is a morphism ε P:[P]P\varepsilon_P:[P] \to P from the support object of PP to PP itself. This implies the formulation above since the object XX is always a subobject of itself; conversely, if there is a morphism ε X:[X]X\varepsilon_X:[X] \to X for every object XCX \in C, then there is a morphism ε P:[P]P\varepsilon_P:[P] \to P for subobjects PXP \hookrightarrow X.

In allegory theory

Given a regular category CC, the bicategory of relations of CC is a unitary tabular allegory. Conversely, the category of maps of a unitary tabular allegory is a regular category. Similarly, given a Heyting category CC, the bicategory of relations of CC is a division allegory, and conversely, the category of maps of a division allegory is a Heyting category. This implies that internal global choice operators can be defined in any unitary tabular allegory and external global choice operators can be defined in any (well-pointed) division allegory.

This is sometimes used in allegorical set theories like SEAR plus epsilon.

External choice operator

Recall that a map in an allegory \mathcal{E} is a morphism with a right adjoint, and an injective map between objects XX \in \mathcal{E} and YY \in \mathcal{E} is a map fMap (X,Y)f \in \mathrm{Map}_\mathcal{E}(X, Y) such that f fid Xf^\dagger \circ f \leq \mathrm{id}_X. For any objects XX \in \mathcal{E} and YY \in \mathcal{E}, let

Map (X,Y)Hom (X,Y)\mathrm{Map}_\mathcal{E}(X, Y) \subseteq \mathrm{Hom}_\mathcal{E}(X, Y)

denote the hom-subset of maps between objects XX and YY. A division allegory \mathcal{E} is well-pointed if

  • The allegorical unit 11 is not a zero object

  • for any objects XX \in \mathcal{E} and YY \in \mathcal{E} and injective maps fMap (X,Y)f \in \mathrm{Map}_\mathcal{E}(X, Y), if for all maps yMap (1,Y)y \in \mathrm{Map}_\mathcal{E}(1, Y) from the allegorical unit 11 \in \mathcal{E} to YY, there exists a map xMap (1,X)x \in \mathrm{Map}_\mathcal{E}(1, X) such that fx=yf \circ x = y, then ff is a unitary isomorphism.

Then Hilbert’s formulation of the external (global) choice operator is rendered as the following: for any object XX \in \mathcal{E} and any property P(x)P(x) on Map (1,X)\mathrm{Map}_\mathcal{E}(1, X) we can form a map ε Xx.P(x)Map (1,X)\varepsilon_X x.P(x) \in \mathrm{Map}_\mathcal{E}(1, X) such that

xMap (1,X).P(x)P(ε Xx.P(x)).\exists x \in \mathrm{Map}_\mathcal{E}(1, X).P(x) \;\Rightarrow\; P\big(\varepsilon_X x.P(x)\big).

Internal choice operator

The support object [X][X] of an object XX in a unitary tabular allegory CC is the tabulation? of the unique map from XX into the allegorical unit? 11.

An internal (global) choice operator in CC consists of, for every object XX, an map ε X:Map C([X],X)\varepsilon_X:\mathrm{Map}_C([X], X) from the support object of XX to the original object XX.

In dependent type theory

In dependent type theory with propositional truncations, the naive translation of the global choice operator results in the following rule:

ΓAtypeΓ,x:[A]ε A(x):A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:[A] \vdash \varepsilon_A(x):A}

The above rule could be simplified to the following rule using function types:

ΓAtypeΓε A:[A]A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \varepsilon_A:[A] \to A}

This corresponds to the internal global choice operator in category theory, since the logic is only internal logic in dependent type theory; there is no separate external logic.

One can also use a Hilbert-style global choice operator which says that choice operators exist for dependent sum types

ΓAtypeΓ,x:AB(x)typeΓε Ax.B(x):x:A.B(x) x:AB(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \varepsilon_A x.B(x):\exists x:A.B(x) \to \sum_{x:A} B(x)}

where the existential quantifier is defined as

x:A.B(x)[ x:AB(x)]\exists x:A.B(x) \coloneqq \left[\sum_{x:A} B(x)\right]

The Hilbert-style global choice operator implies the other version of the global choice operator, because given a type AA, the dependent sum type x:A y:Ax= Ay\sum_{x:A} \sum_{y:A} x =_A y is definitionally isomorphic to AA. Conversely, the other version of the global choice operator implies the Hilbert style choice operator, since having a global choice operator for every type implies having choice operators for dependent sum types.

Properties

Relation to set truncation axioms

This rule is an axiom of set truncation, because given type AA and elements x:Ax:A and y:Ay:A, one has a function ε x= Ay:[x= Ay]x= Ay\varepsilon_{x =_A y}:[x =_A y] \to x =_A y. Since [x= Ay][x =_A y] is an equivalence relation, the fact that there is a function from [x= Ay][x =_A y] to x= Ayx =_A y implies that AA is a set.

One could try to set-truncate the target, or restrict the global choice operator to inhabited h-sets:

ΓAtypeΓ,x:[A]ε A(x):[A] 0ΓAtypeΓ,p:isSet(A),x:[A]ε A(p,x):A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:[A] \vdash \varepsilon_A(x):[A]_0} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, p:\mathrm{isSet}(A), x:[A] \vdash \varepsilon_A(p, x):A}

However, this inference rule implies the untruncated axiom of choice:

ΓAtypeΓ,x:AB(x)typeΓ,x:A,y:B(x)P(x,y)typeΓac A,B,P:Πx:A.y:B(x).[P(x,y)]g:(Πx:A.B(x)).Πx:A.[P(x,g(x))]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type} \quad \Gamma, x:A, y:B(x) \vdash P(x, y) \; \mathrm{type}}{\Gamma \vdash \mathrm{ac}_{A, B, P}:\Pi x:A.\exists y:B(x).[P(x, y)] \to \exists g:(\Pi x:A.B(x)).\Pi x:A.[P(x, g(x))]}

which is inconsistent with a univalent Tarski universe with non-propositional h-sets. (See the HoTT book, section 3.8).

Relation to double negation

The existence of a choice operator implies excluded middle and the double negation law, and in particular, means that in dependent type theory the propositional truncation of a type is given by the double negation modality:

[A]¬¬A[A] \coloneqq \neg \neg A

This means that the rules for choice operators can be rewritten using double negation rather than propositional truncations:

ΓAtypeΓ,x:¬¬Aε A(x):A\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:\neg \neg A \vdash \varepsilon_A(x):A}

equivalently, that

ΓAtypeΓε A:¬¬AA\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \varepsilon_A:\neg \neg A \to A}

It then becomes clear that the law of double negation is simply the choice operator only for h-propositions. Thus, choice operators could be called the type-theoretic law of double negation under the propositions as types interpretation of dependent type theory.

One could equivalently define the set-theoretic choice operator using double negations, by one of these inference rules:

ΓAtypeΓε A:¬¬A[A] 0ΓAtypeΓε A:isSet(A)׬¬AA\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \varepsilon_A:\neg \neg A \to [A]_0} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \varepsilon_A:\mathrm{isSet}(A) \times \neg \neg A \to A}

By currying the conclusion of the second rule, one gets

ΓAtypeΓε A:isSet(A)(¬¬AA)\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \varepsilon_A:\mathrm{isSet}(A) \to (\neg \neg A \to A)}

which is a version of the law of double negation for h-sets.

Relation to the axiom of choice

In dependent type theory, the usual axiom of choice says that the dependent product of a family of inhabited sets is itself inhabited:

ΓAtypeΓ,x:AB(x)typeΓAC A,B:(isSet(A)×( x:AisSet(B(x))))( x:A[B(x)])[ x:AB(x)]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{AC}^{A, B}:\left(\mathrm{isSet}(A) \times \left(\prod_{x:A} \mathrm{isSet}(B(x))\right)\right) \to \left(\prod_{x:A} [B(x)]\right) \to \left[\prod_{x:A} B(x)\right]}

If one untruncates the codomain of the function, one gets choice operators for every set-indexed family of sets:

ΓAtypeΓ,x:AB(x)typeΓAGC A,B:(isSet(A)×( x:AisSet(B(x))))( x:A[B(x)]) x:AB(x)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{AGC}^{A, B}:\left(\mathrm{isSet}(A) \times \left(\prod_{x:A} \mathrm{isSet}(B(x))\right)\right) \to \left(\prod_{x:A} [B(x)]\right) \to \prod_{x:A} B(x)}

If one removes the requirement that the type family is a family of sets from the axiom of choice, one gets the axiom of infinity-choice:

ΓAtypeΓ,x:AB(x)typeΓAC A,B:isSet(A)( x:A[B(x)])[ x:AB(x)]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{AC}_\infty^{A, B}:\mathrm{isSet}(A) \to \left(\prod_{x:A} [B(x)]\right) \to \left[\prod_{x:A} B(x)\right]}

If one untruncates the codomain of the function, one gets choice operators for every set-indexed family of type:

ΓAtypeΓ,x:AB(x)typeΓAGC A,B:isSet(A)( x:A[B(x)])[ x:AB(x)]\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma, x:A \vdash B(x) \; \mathrm{type}}{\Gamma \vdash \mathrm{AGC}_\infty^{A, B}:\mathrm{isSet}(A) \to \left(\prod_{x:A} [B(x)]\right) \to \left[\prod_{x:A} B(x)\right]}

Similarly, the axiom of countable choice says that the dependent product of a family of inhabited sets indexed by the natural numbers is itself inhabited:

Γ,n:A(n)typeΓAC A:( n:isSet(A(n)))( n:[A(n)])[ n:A(n)]\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type}}{\Gamma \vdash \mathrm{AC}_\mathbb{N}^A:\left(\prod_{n:\mathbb{N}} \mathrm{isSet}(A(n))\right) \to \left(\prod_{n:\mathbb{N}} [A(n)]\right) \to \left[\prod_{n:\mathbb{N}} A(n)\right]}

If one untruncates the codomain of the function, one gets choice operators for every \mathbb{N}-indexed family of sets:

Γ,n:A(n)typeΓAGC A:( n:isSet(A(n)))( n:[A(n)]) n:A(n)\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type}}{\Gamma \vdash \mathrm{AGC}_\mathbb{N}^A:\left(\prod_{n:\mathbb{N}} \mathrm{isSet}(A(n))\right) \to \left(\prod_{n:\mathbb{N}} [A(n)]\right) \to \prod_{n:\mathbb{N}} A(n)}

If one removes the requirement that the type family is a family of sets from the axiom of choice, one gets the axiom of infinity-choice:

Γ,n:A(n)typeΓAC A:( n:[A(n)])[ n:A(n)]\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type}}{\Gamma \vdash \mathrm{AC}_\mathbb{N}^A:\left(\prod_{n:\mathbb{N}} [A(n)]\right) \to \left[\prod_{n:\mathbb{N}} A(n)\right]}

If one untruncates the codomain of the function, one gets choice operators for every \mathbb{N}-indexed family of types:

Γ,n:A(n)typeΓAC A:( n:[A(n)]) n:A(n)\frac{\Gamma, n:\mathbb{N} \vdash A(n) \; \mathrm{type}}{\Gamma \vdash \mathrm{AC}_\mathbb{N}^A:\left(\prod_{n:\mathbb{N}} [A(n)]\right) \to \prod_{n:\mathbb{N}} A(n)}

The codomain-untruncated versions of these variants of the axiom of choice are all equivalent to the original inference rule of having global choice operators, which is the special case of either

  1. for the codomain-untruncated axiom of choice the type family being indexed by a contractible type

  2. for the codomain-untruncated axiom of countable choice, the type family being defined by A(n+1)A(n + 1) being a contractible type for all natural numbers, so that A(0) n:A(n)A(0) \simeq \prod_{n:\mathbb{N}} A(n).

Sets which constructively have a choice operator

Every detachable subset of the natural numbers has a choice operator. This is because, every detachable subset of the natural numbers is in bijection with the set {n|P(n)}\{n \in \mathbb{N} \vert P(n)\} for a decidable predicate P(n)P(n) on the natural numbers nn \in \mathbb{N}. Given a decidable predicate P(n)P(n) on the natural numbers nn \in \mathbb{N}, if there exists a natural number nn \in \mathbb{N} such that P(n)P(n) holds, then one can construct a minimal natural number min P\min_P such that the P(min P)P(\min_P) holds. See Rijke 2022 for a proof of this in dependent type theory, where {n|P(n)}\{n \in \mathbb{N} \vert P(n)\} is represented by the dependent sum type n:P(n)\sum_{n:\mathbb{N}} P(n) and the existential quantifier n:.P(n)\exists n:\mathbb{N}.P(n) is represented by the propositional truncation of the dependent sum type.

Every pointed set (X,pt)(X, \mathrm{pt}) has a choice operator, since its support [X][X] is a singleton and thus in bijection with the canonical singleton 𝒫()\mathcal{P}(\emptyset) in set theory, and elements in XX are thus in bijection with functions from its support to XX itself:

i:XX 𝒫()X [X]i:X \cong X^{\mathcal{P}(\emptyset)} \cong X^{[X]}

Thus the choice operator can simply be defined as the evaluation of the bijection at the given point pt\mathrm{pt} of the set,

ϵ Xi(pt)\epsilon_X \coloneqq i(\mathrm{pt})

This makes sense, since if the pointed set XX is already a subset of another set YY, then we know that there is already an element for which the predicate P XP_X on YY representing the subset XX holds - the given point of the pointed set; i.e. P X(pt)P_X(\mathrm{pt}) always holds.

Constructively, the empty set is always not pointed because the function set \emptyset^\emptyset is a singleton. However, that every set is either pointed or empty is equivalent to the excluded-middle presentation of the axiom of global choice, which says that one can construct an element of the disjoint union X+X X + X^\emptyset.

Foundational status

It should be noted that Hilbert and Bourbaki take the ε\varepsilon-operator, called τ\tau in “Theory of Sets” to be a primitive symbol in a mathematical theory. This has the advantage of also allowing the existential and universal quantifiers to be constructed explicitly, since x\exists x translates to P(ε x(P(x)))P(\varepsilon_x(P(x))). The intuitive meaning behind the operator is that it returns a distinguished object for which the proposition is true, or if no such object exists, it returns any object for which it is not true. Of course, the intuitive meaning can be misleading since the properties of the epsilon operator are governed by the axiom schema of existence and ε\varepsilon-extensionality, without which, the symbol has no meaning. The axiom scheme of existence is a statement of Hilbert’s axiom that avoids mention of the existential quantifier.

A wonderful usage of the global choice operator in Bourbaki is that we can easily show that paradoxical sets do not exist, since the definition of a set is given in terms of whether or not the relation defining the set is collectivizing. The example of Russell's paradox is computed in (Theory of Sets, Chapter II, §1, no.4). A consequence of this formulation is that the epsilon calculus is quantifier-free, since ε\varepsilon subsumes their roles from the predicate calculus. If we adjoin ε\varepsilon to intuitionistic logic with the axiom scheme of existence, we obtain a non-conservative extension of intuitionistic logic in which the law of excluded middle still does not hold. However, the assumption of the axiom scheme of ε\varepsilon-extensionality implies the axiom of global choice and therefore the law of excluded middle.

One use of the choice operator is to eliminate undesirable details of implementation. For example, if P(x)P(x) is “xx is a Dedekind-complete totally ordered field,” then we can define “the real numbers” to be εx.P(x)\varepsilon x.P(x). Any of the numerous constructions of the real numbers can then be used to show that there exists an xx such that P(x)P(x), after which point we can discard whichever explicit construction and work only with =εx.P(x)\mathbb{R}=\varepsilon x.P(x). This way we can no longer assert that real numbers (elements of \mathbb{R}) are Dedekind cuts, or equivalence classes of Cauchy sequences, or anything in particular, since the axioms provide no rules about how εx.P(x)\varepsilon x.P(x) must be chosen other than that it must satisfy PP. So \mathbb{R} might consist of Cauchy sequences, or Dedekind cuts, or any other way to construct the reals, but we have no way of knowing, and thus we cannot make use of any such definition in a proof about \mathbb{R}; we are forced to use only its formal properties. (For a type-theoretic treatment of this situation, see generalized the).

In many cases, the assumption of a global choice operator implies the axiom of choice, since for any family (A u)(A_u) of inhabited sets, a choice function is given by u(εx.xA u)u\mapsto (\varepsilon x.x\in A_u). In fact, in the form given above it often implies the stronger global axiom of choice, which applies to proper classes as well as sets.

“Here, moreover, we come upon a very remarkable circumstance, namely, that all of these transfinite axioms are derivable from a single axiom, one that also contains the core of one of the most attacked axioms in the literature of mathematics, namely, the axiom of choice: A(a)A(ε(A))A(a) \rightarrow A(\varepsilon(A)), where ε\varepsilon is the transfinite logical choice function.”

—Hilbert (1925), “On the Infinite”, excerpted in Jean van Heijenoort, From Frege to Gödel, p. 382.

However, in some foundations it seems to be possible to avoid this conclusion (if it is unwanted) by not requiring the choice operator to be extensional, i.e. it may not be the case that A=BA = B implies εx.A=εx.B\varepsilon x.A = \varepsilon x.B.

Like the axiom of choice, the existence of a global choice operator is consistent with the other axioms of most foundations. For example, in ZF, the constructible universe (which models ZF+(V=L)ZF + (V=L), the axiom of constructibility) admits a natural classical well-ordering of the entire universe, giving rise to a naturally defined global choice operator (namely, εx.P\varepsilon x.P = the smallest xx such that PP in the global well-ordering).

On the other hand, in dependent type theory a global choice operator over the entire type theory is inconsistent with a univalent universe. For univalence requires that all operations on the type universe must be natural with respect to equivalences, which no global choice operator can be. If one only has a global choice operator over only the types in a given type universe, one can still prove the limited principle of omniscience for natural numbers LPO \mathrm{LPO}_\mathbb{N} for the entire type theory: a global choice operator for a universe UU implies that the axiom of choice and excluded middle holds in UU, which in turn implies that the boolean domain is the homotopy-initial σ \sigma -frame, which is equivalent to LPO \mathrm{LPO}_\mathbb{N}.

Readings

For the principle of global choice in dependent type theory, see example 14.4.1, remark 14.4.2. and corollary 17.5.3 of

Last revised on August 31, 2024 at 17:19:11. See the history of this page for a list of all contributions to it.