We present a model of Martin-Lof type theory that includes both dependent products and the identity type. It is based on the category of small categories, with cloven Grothendieck bi brations used to model dependent types. The identity type is modelled by a path functor that seems to have independent interest from the point of view of homotopy theory. We brie y describe this model's strengths and limitations.