The following definition is due to Mathieu Dupont.
A regular 2-category 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 satisfies the axiom of 2-choice iff 1. has enough discretes and 1. satisfies the ordinary axiom of choice (with respect to regular epis).
The “if” direction is clearly true even without exactness: given an eso where is discrete and is groupoidal, find an eso where is discrete, and then split the composite . Conversely, since discrete objects are groupoidal, the axiom of 2-choice clearly implies the ordinary axiom of choice (“1-choice”) for . So it remains only to prove that 2-choice implies the existence of enough discretes in .
The obvious approach is: given , we construct its discrete reflection . Then by assumption, the eso admits a splitting , which we would like to show is also eso. Since the discretization of is an isomorphism, so is the discretization of its splitting, so it would suffice to know that for a map in a (2,1)-exact (2,1)-category, if the discretization of is an isomorphism, then 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.