Can the formalisms of category theory replace those of type theory?
My view is more or less similar to chi's. I see category theory as (roughly) being to type theory what model theory is to logic. Some of the consequences of that are, first, each can exist autonomously. Indeed, type theory predates category theory, and the creation of category theory was not motivated by these concerns. Second, many of the distinctions category theory/model theory are purposely trying to blur are of primary interest in type theory/logic.

As a very basic example, all presentations of the axioms of a group give rise to the same class of models (namely groups). From the perspective of universal algebra, a variety (in the universal algebra sense, or a finitary algebraic category from a CT perspective) forgets its presentation. Meanwhile, from the perspective of equational logic, presentation is all there is. A primary computational topic here is E-unification which operates entirely at the level of equational logic, i.e. presentation. 

This is typical. We say the simply typed lambda calculus (with products) (STLC) is the internal language of Cartesian closed categories, but it is really just one presentation of the internal language and not even the most "direct" one. The Categorical Abstract Machine (CAM) is arguably a more "direct" representation. Even with the STLC, the arrows of corresponding syntactic category are $\beta\eta$-equivalence classes of lambda terms! (But see this.) So either we somehow directly describe the syntactic category as a mathematical structure whose hom-sets just happen to coincide with $\beta\eta$-equivalance classes of STLC terms and have no computational content, or we need to already understand the STLC external to category theory, or we need to talk instead of presentations of Cartesian closed categories which, taking a fairly natural approach, will lead to something CAM-like. In the last case, equality of arrows becomes something like an E-unification problem. Understanding and simplifying this process as well as placing the more ergonomic facade of the STLC in front of it, requires techniques that are the bread and butter of logic and type theory but are not particularly natural within category theory.

A massively over-simplified picture that may nevertheless give a better idea of how category theory and type theory interrelate is the following. You can imagine them as two dimensions. The tools, techniques, and notations of type theory are geared toward moving vertically between different presentations of the same object, meanwhile the tools, techniques, and notations of category theory and geared toward moving horizontally between different mathematical objects. You might even say that a category is a whole vertical line and that category theory talks about moving one vertical line to another but not how the points of the two lines correspond. In this picture, category theory is not even capable of talking about the distinctions type theory is making, but this is intentional because it means that the arbitrarily complicated mapping of points on one vertical line to points on another is just irrelevant to what category theory cares about and can be ignored.

In my blog post, Category Theory, Syntactically, I describe an approach that makes category theory look more like type theory (rather than the other way around). Unsurprisingly, what I'm really discussing there are presentations of categories. Further, you can see aspects of normalization enter the picture, e.g. in my discussion of "product theories", even though this is not a focus at all of that particular post.