Proposition 1 is extremely straightforward to prove (provided you have some facts like the quillen adjunction between SSet and CGWH). Sing(|S|) gives you a simplicial set where all of the edges "forget" their direction, and when you apply the inverse of the nerve functor, you get back a copy of C with all of its arrows as isomorphisms. Covering spaces are equivalent to (etale) bundles (of sets) on a topological space, which by a theorem in Mac Lane (Sheaves in Geometry and Logic) is equivalent to taking sheaves on the space, so by unraveling these equivalences, you get your result. The last equivalence is probably one you're familiar with as the espace \'etal\'e. (While in general, the nerve functor does not have an inverse, the nerve of a category has some nice properties that make the total singular complex (the $Sing$ functor) pull back intact, modulo directedness of edges. If you think about the actual graph of the nerve of an ordinary category, it's not hard to see why this is true. This is precisely because the geometric realization "forgets" some information.)

The construction you're describing is generalized by a functor in HTT called the unstraightening functor, which you can read about in HTT Ch 2.2. With a number of more sophisticated results, we can generalize the adjunction between $Sing$ and $| \cdot |$ to a Quillen equivalence between SSet-Cat and CGWH-Cat.

HTT is Higher topos theory by J. Lurie.

8 added 61 characters in body

Proposition 1 is extremely straightforward to prove (provided you have some facts like the quillen adjunction between SSet and CGWH). It's almost tautological, since Sing(|S|) gives you a simplicial set where all of the edges "forget" their direction, and when you apply the inverse of the nerve functor, you get back a copy of C with all of its arrows as isomorphisms. Covering spaces are (on the nose) equivalent to (etale) bundles (of sets) on a topological space, which by a theorem in Mac Lane (Sheaves in Geometry and Logic) is equivalent to taking sheaves on the space, so by unraveling these equivalences, you get your result. The last equivalence is probably one you're familiar with as the espace \'etal\'e. (While in general, the nerve functor does not have an inverse, the nerve of a category has some nice properties that make the total singular complex pull back intact, modulo orientation directedness of edges. If you think about the actual graph of the nerve of an ordinary category, it's not hard to see why this is true. It might also be useful to remember that This is precisely because the geometric realization "forgets" some information.)

According to a private correspondence I had earlier, the

The construction you're describing is generalized by a functor in HTT called the unstraightening functor, which you can read about in HTT Ch 2.2. With a number of more sophisticated results, we can generalize the adjunction between $Sing$ and $| \cdot |$ to a Quillen equivalence between SSet-Cat and CGWH-Cat.

HTT is Higher topos theory by J. Lurie.

7 collapsed edits

Proposition 1 is extremely straightforward to prove. It's almost tautological, since Sing(|S|) gives you a simplicial set where all of the edges "forget" their direction, and when you apply the inverse of the nerve functor, you get back a copy of C with all of its arrows as isomorphisms. Covering spaces are (on the nose) equivalent to (etale) bundles (of sets) on a topological space, which by a theorem in Mac Lane (Sheaves in Geometry and Logic) is equivalent to taking sheaves, so by unraveling these equivalences, you get your result. (While in general, the nerve functor does not have an inverse, the nerve of a category has some nice properties that make the total singular complex pull back intact, modulo orientation of edges. If you think about the actual graph of the nerve of an ordinary category, it's not hard to see why this is true. It might also be useful to remember that the geometric realization "forgets" some information.)

According to a private correspondence I had earlier, the construction you're describing is generalized by a functor in HTT called the unstraightening functor, which you can read about in HTT ch. Ch 2.2or 2.3. This is clear if you identify the category of weak Kan complexes with the category of compactly-generated (weakly hausdorff) spaces, i.e. "nice spaces". This can be done by showing that the adjunction between the total singular complex functor and the geometric realization functor is a Quillen equivalence.

EDIT 1: To clarify, the unstraightening construction is highly nontrivial, but the trivial part is to translate that back from the language of simplicially enriched categories to Topological categories (CGWH-Enriched categories). According to this personal correspondence I referenced earlier, the whole point of ch 2.1-2.3 is to establish that every quasi-category is contains its own classifying space, and that quasicategories and topologically-enriched categories are equivalent in With a sense specific to the book.

EDIT 2: I misspoke. Upon reareading, I found that the proof number of the equivalence between topologically enriched categories and simplicially enriched categories is not given until after the unstraightening construction. This just means that it's not trivial to translate the more sophisticated resultsback without the theorem. However, in the case of your proposition 1, you do not need the statement in its full generality the way Lurie proves it. You only need the standard proof of we can generalize the quillen adjunction between $Sing$ and $| \cdot |$
to a Quillen equivalence between SSet-Cat and CGWH-Cat.

6 added 213 characters in body