# Michael Shulman axiom of 2-choice

The following definition is due to Mathieu Dupont.

###### Definition

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.

###### Conjecture

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

1. $\mathrm{gpd}\left(K\right)$ has enough discretes and
2. $\mathrm{disc}\left(K\right)$ 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}\left(K\right)$. So it remains only to prove that 2-choice implies the existence of enough discretes in $\mathrm{gpd}\left(K\right)$.

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)