But category theory has been done in Martin-Löof type theory: http://www.cs.st-andrews.ac.uk/~rd/publications/CTMLTT.pdf It has also been done in the type-theoretic proof assistant Coq: http://coq.inria.fr/distrib/v8.2/contribs-20090527/ConCaT.html
In both of these, there *is* a notion of equality (or better, identity) at all types, hence a notion of identity of objects of any given category, allowing one to define isomorphism of categories, etc. However, this logicians' identity does not match mathematicians' equality; the easiest way to see this is that there are no quotient types. (This means that already to do set theory, let alone category theory, you must define a set to be a type equipped with an equivalence relation. Such a thing is also called "setoid", depending on which author you read.)
I don't know any reasonable formalisation in Intensional Type Theory. People usually assume that hom sets are a setoid but objects aren't. This means that constructions like arrow categories are not available. To avoid this one would have to formalize explicitely what is a family of setoids indexed over a setoid. After this it is hard to see the category theory... Cheers, Thorsten [For admin and other information see: http://www.mta.ca/~cat-dist/ ]