On Leighton's graph covering theorem

We give short expositions of both Leighton's proof and the Bass-Kulkarni proof of Leighton's graph covering theorem, in the context of colored graphs. We discuss a further generalization, needed elsewhere, to "symmetry-restricted graphs." We can prove it in some cases, for example, if the "graph of colors" is a tree, but we do not know if it is true in general. We show that Bass's Conjugation Theorem, which is a tool in the Bass-Kulkarni approach, does hold in the symmetry-restricted context.