axiom of 2-choice

The following definition is due to Mathieu Dupont.

A regular 2-category $K$ satisfies the **axiom of 2-choice** if every eso from a groupoidal object to a discrete object admits a splitting.

A (2,1)-exact and countably-coherent 2-category $K$ satisfies the axiom of 2-choice iff

- $\mathrm{gpd}(K)$ has enough discretes and
- $\mathrm{disc}(K)$ satisfies the ordinary axiom of choice (with respect to regular epis).

The “if” direction is clearly true even without exactness: given an eso $X\to A$ where $A$ is discrete and $X$ is groupoidal, find an eso $G\to X$ where $G$ is discrete, and then split the composite $G\to A$. Conversely, since discrete objects are groupoidal, the axiom of 2-choice clearly implies the ordinary axiom of choice (“1-choice”) for $\mathrm{disc}(K)$. So it remains only to prove that 2-choice implies the existence of enough discretes in $\mathrm{gpd}(K)$.

The obvious approach is: given $X$, we construct its discrete reflection ${X}_{\le 0}$. Then by assumption, the eso $X\to {X}_{\le 0}$ admits a splitting ${X}_{\le 0}\to X$, which we would like to show is also eso. Since the discretization of $X\to {X}_{\le 0}$ is an isomorphism, so is the discretization of its splitting, so it would suffice to know that for a map $f$ in a (2,1)-exact (2,1)-category, *if the discretization of $f$ is an isomorphism, then $f$ is eso*.

This is true in a (2,1)-topos, by internal arguing in homotopy type theory; see sets cover.

Revised on August 18, 2013 07:02:41
by Mike Shulman
(107.194.22.192)