Lawvere’s definition of hyperdoctrines preceded intuitionistic type theory but did not go all the way to identifying propositions and types. Nevertheless Lawvere influenced Scott’s (1970) work on constructive validity, a somewhat preliminary precursor of intuitionistic type theory. After Martin-Löf (1998 [1972]) had presented a more definite formulation of the theory, the first work on categorical models was presented by Cartmell in 1978 with his notions of category with attributes and contextual category (Cartmell 1986). However, we will not define these structures here but instead the closely related categories with families (Dybjer 1996) which are formulated so that they directly model a variable-free version of a formulation of intuitionistic type theory with explicit substitutions (Martin-Löf 1995).