A gentle introduction to categorical models of dependent type theory. As a warm up, Richard will explain the interpretation in locally cartesian closed categories (LCCCs), and why it necessarily leads to extensional models of type theory. Then, he will, rather informally, try to explain why models of intensional type theory should look like weak omega categories (read the ordinal ``omega'').