Abstract: I'll discuss the notion of a model of dependent type theory. After outlining the general algebraic semantics, I'll show how such models can be constructed from categories that we encounter in the so-called "mathematical practice".