How to show that a type in a system with dependent types is not inhabited (i.e. formula not provable)?
That a formula is not provable can essentially be done in two ways. With some luck we might be able to show within type theory that the formula implies one which is already known to be not provable. The other way is to find a model in which the formula is invalid, and this can be quite hard. For example, it took a very long time to find the groupoid model of dependent type theory, which was the first to invalidate uniqueness of identity proofs.

The question "what is a model of dependent type theory?" has a somewhat complicated answer. If you ignore certain properties of substitution, a model is a locally cartesian closed category, and that might be the simplest answer. If you want a "real" model, then there are several options, see the nLab page on categorical models of dependent type theory. In any case, the answer is always a bit complicated because dependent type theory is a fairly complex formal system.

If I were to suggest just one article on the subject, I would probably recommend the original paper by Robert Seely, "Locally cartesian closed categories and type theory". If I were to suggest another one, it would probably be one that explains what needs to be corrected in Seely's paper, e.g., Martin Hoffman's "On the Interpretation of Type Theory in Locally Cartesian Closed Categories".

A recent important advance in this area is the realization that homotopy-theoretic models are also models of dependent type theory, see homotopytypetheory.org references. This provides a wealth of possibilities, but one must now learn homotopy theory to get hands on the models.