When working with strict categories in foundations without the axiom of choice, it is not true that every fully faithful and essentially surjective functor is an equivalence of categories, since the mere property of being isomorphic to some object in the image is not enough to get a specific such object and isomorphism without the axiom of choice. However, it is true if instead one uses split essentially surjective functors, where the isomorphisms are structure rather than mere property.
A functor $F : C \to D$ is split essentially surjective if there is a specified family
indexed by objects $y \in D$.
Every split essentially surjective functor is essentially surjective.
That every essentially surjective functor is split essentially surjective is equivalent to the axiom of choice.
In homotopy type theory (or, indeed, any dependent type theory), the definition above can be phrased for general precategories in type theoretic language:
A functor $F : C \to D$ is split essentially surjective if there is a specified dependent function
This differs from the definition of an essentially surjective functor by the lack of propositional truncations in the definition:
A functor $F : C \to D$ is essentially surjective if the there is a dependent term
for all objects $y:D$.
However, for precategories, and even for univalent categories, the axiom of choice is insufficient to ensure that every essentially surjective functor is split essentially surjective. For instance, let $G$ be a nontrivial group and $BG$ the corresponding connected univalent groupoid, and $\ast$ the terminal category; then the functor $\ast \to BG$ is essentially surjective, but not split essentially surjective.
basic properties of…
Last revised on July 25, 2023 at 02:43:39. See the history of this page for a list of all contributions to it.