Categorical semantics of dependent types


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.

Read here