This paper examines the connections between intuitionistic type theory and category theory. A version of type theory is developed in a category theoretic framework by interpreting types as objects and type connectives as constructions in categories. This yields a theory that uniformly models type inhabitation, proof theory, type universes, syntactic forms, equality and computation.