Michael Shulman
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

  1. gpd(K) has enough discretes and
  2. 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 XA where A is discrete and X is groupoidal, find an eso GX where G is discrete, and then split the composite GA. Conversely, since discrete objects are groupoidal, the axiom of 2-choice clearly implies the ordinary axiom of choice (“1-choice”) for disc(K). So it remains only to prove that 2-choice implies the existence of enough discretes in gpd(K).

The obvious approach is: given X, we construct its discrete reflection X 0. Then by assumption, the eso XX 0 admits a splitting X 0X, which we would like to show is also eso. Since the discretization of XX 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 (