A category with families is a functor \(T {:} C^{op} \rightarrow \mathbf{Fam}\), where \(\mathbf{Fam}\) is the category of families of sets. The category \(C\) is the category of contexts and substitutions. If \(\Gamma\) is an object of \(C\) (a context), then \(T(\Gamma)\) is the family of terms of type \(A\) which depend on variables in \(\Gamma\). If \(\gamma\) is an arrow in \(C\) representing a substitution, then the arrow part of the functor represents substitution of \(\gamma\) in types and terms. A category with families also has a terminal object and a notion of context comprehension, reminiscent of Lawvere’s comprehension in hyperdoctrines. The terminal object captures the rules for empty contexts and empty substitutions. Context comprehension captures the rules for extending contexts and substitutions, and has projections capturing weakening and assumption of the last variable.