Abstract
We introduce categories with families as a new notion of model for a basic framework of dependent types. This notion is close to the ordinary syntax and yet has a clean categorical description. We present categories with families as a Generalized Algebraic Theory the define categories with families formally in extensional type theory. Finally we discuss the coherence problem for these internal categories with families.