Categorical semantics of dependent types
Introduction
I wrote my masters thesis on the categorical semantics of dependent types. As it stands it is a decent introduction to and motivation for Martin-Lof's theory of dependent types. The bulk of the dissertation consists of a presentation of categories with families and comprehension categories.
The material is aimed at an advanced undergraduate student who is familiar with the Curry-Howard correspondence between the simply typed lambda calculus and cartesian closed categories.
Unfortunately the work is very brief in some sections, and skips a lot of details. I may expand on it at a later time.
I am happy to receive any questions or corrections.