Michael Shulman axiom of 2-choice

The following definition is due to Mathieu Dupont.


A regular 2-category KK 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 KK satisfies the axiom of 2-choice iff 1. gpd(K)gpd(K) has enough discretes and 1. disc(K)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 XAX\to A where AA is discrete and XX is groupoidal, find an eso GXG\to X where GG is discrete, and then split the composite GAG\to A. Conversely, since discrete objects are groupoidal, the axiom of 2-choice clearly implies the ordinary axiom of choice (“1-choice”) for disc(K)disc(K). So it remains only to prove that 2-choice implies the existence of enough discretes in gpd(K)gpd(K).

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

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

Last revised on August 18, 2013 at 07:02:41. See the history of this page for a list of all contributions to it.