  Seely's paper "Locally cartesian closed categories and type theory" contains
a well-known result in categorical type theory: that the category of locally
cartesian closed categories is equivalent to the category of Martin-L\"of type
theories with Pi-types, Sigma-types and extensional identity types. However,
Seely's proof relies on the problematic assumption that substitution in types
can be interpreted by pullbacks. Here we prove a corrected version of Seely's
theorem: that the B\'enabou-Hofmann interpretation of Martin-L\"of type theory
in locally cartesian closed categories yields a biequivalence of 2-categories.
To facilitate the technical development we employ categories with families as a
substitute for syntactic Martin-L\"of type theories. As a second result we
prove that if we remove Pi-types the resulting categories with families are
biequivalent to left exact categories.
