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.