\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{axiom of choice}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{foundations}{}\paragraph*{{Foundations}}\label{foundations}

[[!include foundations - contents]]

\hypertarget{the_axiom_of_choice}{}\section*{{The axiom of choice}}\label{the_axiom_of_choice}

\noindent\hyperlink{statement}{Statement}\dotfill \pageref*{statement} \linebreak
\noindent\hyperlink{in_other_categories}{In other categories}\dotfill \pageref*{in_other_categories} \linebreak
\noindent\hyperlink{external_form}{External form}\dotfill \pageref*{external_form} \linebreak
\noindent\hyperlink{internal_form}{Internal form}\dotfill \pageref*{internal_form} \linebreak
\noindent\hyperlink{in_toposes}{In toposes}\dotfill \pageref*{in_toposes} \linebreak
\noindent\hyperlink{equivalents}{Equivalents}\dotfill \pageref*{equivalents} \linebreak
\noindent\hyperlink{Variants}{Variants}\dotfill \pageref*{Variants} \linebreak
\noindent\hyperlink{in_higher_category_theory}{In higher category theory}\dotfill \pageref*{in_higher_category_theory} \linebreak
\noindent\hyperlink{InTypeTheory}{In type theory}\dotfill \pageref*{InTypeTheory} \linebreak
\noindent\hyperlink{consequences}{Consequences}\dotfill \pageref*{consequences} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak
\noindent\hyperlink{general}{General}\dotfill \pageref*{general} \linebreak
\noindent\hyperlink{ReferencesInHomotopy}{In homotopy type theory}\dotfill \pageref*{ReferencesInHomotopy} \linebreak


\hypertarget{statement}{}\subsection*{{Statement}}\label{statement}

The \textbf{axiom of choice} is the following statement:

\begin{itemize}%
\item \emph{Every [[surjection]] in the category [[Set]] of [[sets]] [[split epimorphism|splits]].}

\end{itemize}
This means: for every [[surjection]] $f\colon A \to B$ of sets, there is a function $\sigma\colon B \to A$ (a [[section]]), such that

\begin{displaymath}
(B \stackrel{\sigma}{\to} A \stackrel{f}{\to} B) 
  =
  (B \stackrel{Id_B}{\to} B)
  \,.
\end{displaymath}
Note that a surjection $A \to B$ of sets can be regarded as a $B$-indexed [[family of sets]], while the existence of a section is equivalent to a choice of one element in each set of this family. This reproduces the more classical form of the axiom of choice.

When the full axiom of choice fails, it may still be valid for some restricted class of objects $A$ and/or $B$. An object $B$ such that any [[epimorphism]] $A \to B$ [[split epimorphism|splits]] is called [[projective object|projective]]; this means that one can make choices `indexed by' $B$. Dually, an object $A$ such that one can make choices `with values in' $A$ is called a [[choice object]] (this is not quite equivalent to every epimorphism $A \to B$ splitting).

\hypertarget{in_other_categories}{}\subsection*{{In other categories}}\label{in_other_categories}

More generally, we may consider analogous statements in [[categories]] $C$ other than $Set$.

\hypertarget{external_form}{}\subsubsection*{{External form}}\label{external_form}

We say that $C$ satisfies the \textbf{external axiom of choice} if every [[epimorphism]] in $C$ [[split epimorphism|splits]].

In this form, the axiom of choice may look less mysterious than in its original formulation. For instance, it is clear that it fails in contexts such as $C =$ [[Top]] and $C =$[[Diff]], due to the existence of nontrivial topological and smooth [[fiber bundle]]s.

If $C$ is not [[balanced category|balanced]], such as a [[regular category|regular]] or [[coherent category]] which is not a [[pretopos]], it may be more appropriate to replace in this statement ``epimorphism'' by [[regular epimorphism]] (or [[extremal epimorphism]], [[effective epimorphism]], etc.) In $Set$ (and in any [[topos]]), all of these notions of epimorphism are the same.

More generally still, if $C$ is a [[site]], then the axiom of choice for $C$ may be taken to say that any [[cover]] $U\to X$ admits a section. Obviously this refers only to singleton covers, but if $C$ is [[superextensive site|superextensive]] then any covering family $(p_i\colon U_i \to X)_i$ can be replaced by a singleton cover $\coprod_u U_i \to X$.

\hypertarget{internal_form}{}\subsubsection*{{Internal form}}\label{internal_form}

However, when working in a category that has an [[internal logic]], we may want to ``internalize'' the axiom of choice by asserting, not that every epimorphism has a section, but that the statement ``every epimorphism has a section'' is true in the internal logic (or more precisely the [[stack semantics]]). An equivalent statement is that every object is [[internally projective object|internally projective]]. We call this the \textbf{internal axiom of choice}.

This is generally a weaker statement: a [[topos]] satisfies the external AC if and only if it satisfies the internal AC and also (the external form of) [[supports split]]. Often, however, this is the more relevant notion to consider.

The following characterization can be found in Freyd-Scedrov (\hyperlink{FreydScedrov90}{1990}, p.181)

\begin{theorem}
\label{}\hypertarget{}{}
A [[Grothendieck topos]] satisfies the internal axiom of choice iff it is a [[Boolean topos|Boolean]] [[étendue]].

\end{theorem}
In particular, satisfaction of IAC entails Booleanness.

Classical examples of Boolean étendues are provided by toposes of group actions hence these all satisfy IAC but satisfy AC only in case the group is trivial (cf. Johnstone \hyperlink{JT77}{1977}, p.144 or Freyd-Scedrov \hyperlink{FreydScedrov90}{1990}, p.84, 179)).

If a topos $C$ satisfies IAC, then so do all of its [[slice categories]], although this may not be obvious. See \href{http://mathoverflow.net/questions/139874/pullback-stability-of-internally-projective-objects/140262#140262}{this answer}.

\hypertarget{in_toposes}{}\subsubsection*{{In toposes}}\label{in_toposes}

\begin{theorem}
\label{}\hypertarget{}{}
A [[Grothendieck topos]] satisfies the external axiom of choice iff it is equivalent to the [[category of sheaves]] on a [[complete Boolean algebra]].

\end{theorem}
\hypertarget{equivalents}{}\subsection*{{Equivalents}}\label{equivalents}

The following statements are all equivalent to the axiom of choice in $Set$ (although sometimes the proof in one direction requires [[excluded middle]]). This is a \emph{very} short list; much longer lists can be found elsewhere, such as at \href{http://en.wikipedia.org/wiki/Axiom_of_choice#Equivalents}{Wikipedia}. Some of the statements on this list, though, may be of interest to nLabbers but are not commonly mentioned as equivalents of choice.

\begin{itemize}%
\item The [[well-ordering theorem]] (that any set can be [[well-order|well-ordered]]),
\item [[Zorn's lemma]],
\item That ($L =$ [[monomorphism]]s, $R =$ [[epimorphism]]s) is a [[weak factorization system on Set]].
\item That [[Set]] is equivalent to its own [[free exact completion]].
\item That there exists a [[group]] structure on every [[inhabited set]] (see [[Hartogs number]], or \href{http://mathoverflow.net/questions/12973/does-every-non-empty-set-admit-a-group-structure-in-zf/12988#12988}{this MO answer}).
\item That every [[fully faithful functor|fully faithful]] and [[essentially surjective functor|essentially surjective]] functor between [[strict categories]] is a strong [[equivalence of categories]].
\item That the [[nonabelian cohomology]] $H^1(X;G)$ is trivial for every set $X$ and every [[group]] $G$ (see \href{http://golem.ph.utexas.edu/category/2013/07/cohomology_detects_failures_of.html}{this post}).

\end{itemize}
\hypertarget{Variants}{}\subsection*{{Variants}}\label{Variants}

There are a number of weaker axioms which are implied by the full axiom of choice. Some of these are valid or accepted more generally than the full AC, and/or suffice for some of the usual applications of choice. In particular, the full axiom of choice is generally rejected in [[constructive mathematics]], whereas some of these weaker forms of choice may be accepted, such as (in order of increasing strength) [[countable choice]], [[dependent choice]], and [[COSHEP]].

\begin{itemize}%
\item Many applications of choice in [[logic]], [[topology]], and [[algebra]] require only the [[ultrafilter principle]] (UF), or equivalently the \emph{Boolean prime ideal theorem}.


\item From the perspective of [[constructive mathematics]], the principle of [[excluded middle]] (EM) may be seen as a weak form of the axiom of choice; EM is equivalent to the statement that every [[Kuratowski-finite set]] is projective. See at \emph{[[Diaconescu-Goodman-Myhill theorem]]}.


\item A very weak form of choice (which follows from EM) is the statement that [[supports split]] in $Set$.


\item The axioms of [[countable choice]] (CC) and [[dependent choice]] (DC) suffice for many of the usual applications of choice in the analysis of [[separable space]]s. CC states that the set $\mathbb{N}$ of [[natural number]]s is projective. DC strenghtens CC by allowing the set of possible choices for $n+1$ to depend on the choice made for $n$.


\item The axiom [[COSHEP]], also called the ``presentation axiom,'' says that any set admits a surjection from a projective one (whereas full AC says that all sets are projective). This implies CC and DC, and is moreover sufficient for the existence of [[projective resolution]]s and cofibrant replacements, as well as the usual theorems in algebra that (for example) [[Mod]] has enough projectives. For example, see the [[canonical model structure on Cat]].


\item The [[axiom of small violations of choice]] (SVC) asserts there is a set $S$ such that every set is a [[subquotient]] of $C\times S$ for some choice set $C$. Intuitively, this says that the failure of AC is parametrized by a single set. It can be regarded as a ``dual'' of COSHEP, since it deals with choice sets rather than projective ones, it implies the existence of (at least some) [[injective resolution]]s, and together with COSHEP and EM it implies full AC.


\item The [[axiom of multiple choice]] is a different way of saying that choice is violated in only a small way, which is more ``local'' than SVC. It apparently follows from SVC, at least in [[ZF]].


\item The [[small cardinality selection axiom]] is another similar axiom. It asserts that there is a class function selecting for every set an isomorphic set (its ``cardinality'') such that among each isomorphism class of sets, the collection of all ``cardinalities'' forms only a set.


\item A still weaker axiom along the lines of ``AC fails in only a small way,'' which is implied by AMC, is [[WISC]], i.e. that for any set $X$, the full subcategory of $Set/X$ consisting of the surjections has a [[weakly initial set]] (under COSHEP it has a single weakly initial object, namely a projective cover of $X$). Two similar assertions are that the [[free exact completion]] $Set_{ex/lex}$ of $Set$ is a [[topos]] (i.e. that $Set$ has a [[generic proof]]), and that $Set_{ex/lex}$ is [[well-powered category|well-powered]]; both of these imply WISC.



\end{itemize}
The axiom of choice can also be strengthened in a few ways.

\begin{itemize}%
\item While the ordinary axiom of choice says that any surjection of sets is split, the \emph{axiom of global choice} says that this is also true for any surjection of [[proper classes]]. (Making this precise requires a bit of work.) It is equivalent to the existence of a well-ordering of the class of all sets.


\item One can also postulate a [[choice operator]], which gives a \emph{specified} way to choose an element from any nonempty set. This implies global choice, and conversely a choice operator can be defined from any well-ordering of the class of all sets.



\end{itemize}
Finally, one can instead adopt the \emph{negation} of the axiom of choice, or a strengthened version of this negation:

\begin{itemize}%
\item The assumption that every subset of the [[real line]] has the [[Baire property]] (BP) is consistent with DC but not AC; the same holds for the assumption that every subset of the real line is [[Lebesgue measure|measurable]] (LM) if at least one [[Grothendieck universe]] exists. These assumptions leads to a very nice setting for analysis called [[dream mathematics]].


\item The [[axiom of determinacy]] is a natural statement in [[game theory]] that is consistent with dependent choice; in fact, it implies dependent choices in certain models, such as in the constructible (in the sense of Goedel) closure of the set of reals. However, determinacy contradicts full AC (for example, it implies LM and BP, as in the previous entry).


\item Any of the varieties of [[constructive mathematics]] that contradict excluded middle necessarily contradict choice, but they are usually (if not always) consistent with DC (and even COSHEP).



\end{itemize}
\hypertarget{in_higher_category_theory}{}\subsubsection*{{In higher category theory}}\label{in_higher_category_theory}

To formulate a version of the axiom of choice in a higher category, one has to make an appropriate choice of the meaning of ``epimorphism''. In most cases, it is best to choose [[effective epimorphisms|effective epimorphism in an (infinity,1)-category]] or a related notion such as [[eso morphisms]].

Less obviously, we usually want to also impose [[truncated object|truncation]] requirements on at least some of the objects involved in the axiom of choice. It seems usually necessary to require the codomain to be 0-truncated (axioms of choice without this requirement tend to be inconsistent); as for the domain we can choose to or not.

\begin{itemize}%
\item An $(\infty,1)$-category satisfies the \textbf{axiom of $n$-choice}, or $AC_n$, if every $n$-[[truncated morphism]] with 0-truncated codomain has a section. We write $AC_\infty$ for the \textbf{axiom of infinity-choice}: the statement that \emph{every} morphism with 0-truncated codomain has a section.

\end{itemize}
These are stronger axioms as $n$ increases. The ``difference'' between $AC_0$ and $AC_\infty$ is roughly the axiom that [[sets cover]].

For $(n,k)$-categories with $k\gt 1$ it is unclear whether it is sensible to allow the domain to be non-groupoidal.

\begin{itemize}%
\item In [[2-category theory]], the \emph{[[michaelshulman:axiom of 2-choice]]} has been proposed to mean that every [[eso morphism]] with groupoidal domain and 0-truncated codomain has a section.

\end{itemize}
There are also ``internal'' versions of these axioms.

\begin{itemize}%
\item In [[homotopy type theory]] (the internal logic of an $(\infty,1)$-topos), the internal version of $AC_n$ is ``every surjection onto a set with $n$-type fibers has a section'', or equivalently

\begin{displaymath}
\prod_{(X:Set)} \prod_{(Y:X\to n Type)} \Big( \prod_{(x:X)} \Vert Y(x)\Vert \to \big\Vert \prod_{(x:X)} Y(x) \big\Vert \Big)
\end{displaymath}

\item More generally, we can replace the $(-1)$-truncation by the $k$-truncation to obtain a family of axioms $AC_{k,n}$.


\item We can also replace the $(-1)$-truncation by the assertion of $k$-connectedness, obtaining the \textbf{axiom of $k$-connected choice}.



\end{itemize}
\hypertarget{InTypeTheory}{}\subsubsection*{{In type theory}}\label{InTypeTheory}

In [[Martin-Lof type theory]], if ``there exists'' and ``for all'' are interpreted in the classical way according to [[propositions as types]], then the statement of the axiom of choice comes out as simply the statement that products distribute over coproducts. (See [[distributivity pullback]] for a discussion in terms of the internal type theory of a locally cartesian closed category.) Since this statement is provable, traditionally type theorists say that ``the axiom of choice is provable'' in type theory. However, this is arguably not really a faithful representation of the axiom of choice, not only because it is provable, but because it lacks the usual strong consequences of the set-theoretic axiom of choice.

A better type-theoretic form of the axiom of choice is obtained by inserting [[propositional truncations]] in the notion of ``exists''. See for instance the \hyperlink{HoTTBook}{HoTT Book} for further discussion.

\hypertarget{consequences}{}\subsection*{{Consequences}}\label{consequences}

\begin{itemize}%
\item The axiom of choice implies the [[principle of excluded middle]] (due to Diaconesu 1975) see \hyperlink{McLarty}{McLarty, theorem 17.9}, and see at \emph{\href{excluded+middle#RelationToTheAxiomOfChoice}{excluded middle -- Relation to axiom of choice}}

\end{itemize}
See also the \hyperlink{ConsequencesDatabase}{choice consequences data base}

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[well-ordering]]


\item [[anafunctor]]


\item [[foundations]]


\item [[Boolean topos]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

\hypertarget{general}{}\subsubsection*{{General}}\label{general}

\begin{itemize}%
\item [[HAF|Eric Schechter's analysis book]] surveys several variants of AC and its negation with a view to applications of [[analysis]], including this nice picture:



(Here, UF, DC, CC, BP, and LM are as defined above.)



\end{itemize}
Discussion in [[toposes]] is in

\begin{itemize}%
\item [[Colin McLarty]], section 17.6 of \emph{Elementary Categories, Elementary Toposes}


\item The \href{http://consequences.emich.edu/conseq.htm}{Consequences of the Axiom of Choice Project} provides an interactive data base that can be used to search for implications between various (weakened) forms of the Axiom of Choice. \href{http://cgraph.inters.co/}{Choiceless grapher} builds on this data and provides a graphical presentation.


\item Gon\c{c}alo Gutierres da Concei\c{c}\~a{}o, \emph{The Axiom of Countable Choice in Topology}, \href{http://www.mat.uc.pt/~ggutc/teses/teseingles.pdf}{pdf}

Despite the title, this covers more than countable choice, but the focus is on sequential aspects (metric spaces, first- and second-countable spaces, etc).



\end{itemize}
A classical reference for AC in toposes is section 5.2 (pp.140ff) in

\begin{itemize}%
\item [[Peter Johnstone]], \emph{Topos Theory} , Academic Press New York 1977. (Reprinted by Dover Mineola 2014)

\end{itemize}
Relation to [[cohomology]] is discussed in

\begin{itemize}%
\item [[Andreas Blass]], \emph{Cohomology detects failures of the axiom of choice}, Trans. Amer. Math. Soc. 279 (1983), 257-269 (\href{http://www.ams.org/journals/tran/1983-279-01/S0002-9947-1983-0704615-7/}{web})


\item [[Mike Shulman]], \emph{Cohomology} on the [[homotopy type theory]] blog \href{http://homotopytypetheory.org/2013/07/24/cohomology/}{here}



\end{itemize}
An alternative form of AC in toposes using injectivity is explored in

\begin{itemize}%
\item Toby Kenney, \emph{Injective Power Objects and the Axiom of Choice} , JPAA \textbf{215} (2011) pp.131--144.

\end{itemize}
The result on IAC in toposes stems from

\begin{itemize}%
\item [[Peter Freyd|P. J. Freyd]], A. Scedrov, \emph{[[Categories, Allegories]]} , North-Holland Amsterdam 1990.

\end{itemize}
\hypertarget{ReferencesInHomotopy}{}\subsubsection*{{In homotopy type theory}}\label{ReferencesInHomotopy}

Discussion in [[homotopy type theory]]:

\begin{itemize}%
\item [[Univalent Foundations Project]], section 3.8 of \emph{[[Homotopy Type Theory -- Univalent Foundations of Mathematics]]}

\end{itemize}
category: foundational axiom

[[!redirects axioms of choice]] [[!redirects Choice]] [[!redirects AC]] [[!redirects full choice]] [[!redirects full AC]]

[[!redirects axiom of global choice]] [[!redirects global axiom of choice]]

[[!redirects axiom of infinity-choice]] [[!redirects axiom of n-choice]] [[!redirects axiom of k-connected choice]]

[[!redirects type-theoretic axiom of choice]] [[!redirects type theoretic axiom of choice]] [[!redirects external axiom of choice]] [[!redirects internal axiom of choice]]



\end{document}