Can everything in category theory be restated in a sufficiently expressive type theory? I've been r

There are multiple issues here.
First, internal language is the term for when the structure on a class of categories can be captured by a type theory. Different type theories correspond to different classes of categories. For example, the simply typed lambda calculus (STLC) corresponds to Cartesian closed categories. This implies that any operation that would work within any Cartesian closed category corresponds to an operation in the STLC, and vice versa. It doesn't mean the STLC structure tells you everything about a particular Cartesian closed category. And if you have an arbitrary category which is not Cartesian closed, then this doesn't help you at all.
This leads to the next issue. Homotopy Type Theory (HoTT) is conjectured to be the internal language of ($\mathrm{\infty <!--\; \infty \; -->}$,1)-toposes. These have a lot of structure (as does HoTT). Most categories are not ($\mathrm{\infty <!--\; \infty \; -->}$,1)-toposes. Just like the STLC being the internal language for Cartesian closed categories doesn't help you when you have a category that isn't Cartesian closed, HoTT doesn't help you when your category isn't an ($\mathrm{\infty <!--\; \infty \; -->}$,1)-topos. Types in HoTT don't correspond to arbitrary categories.
As the final issue, the categorical semantics of dependent type theories is complicated (because dependent type theories are complicated). Very roughly speaking, to translate a type theory into a category with the additional structure needed to support the operations in that type theory, types will be interpreted as objects and terms (in context) as morphisms. For dependent type theories with universes, types are also terms and there is extra structure on the category to handle that. With or without universes, though, there is a whole bunch of extra structure beyond a plain category that you need to interpret even the basic structure of a dependent type theory. We don't map categories into type theories, instead we recognize that some categories are models of some type theories. In the internal language of left exact categories, we can axiomatize the notion of a category. Models of this give rise to internal categories. In much richer type theories, we can construct things that look like categories to the type theory. This is what the HoTT book does in Chapter 9, for example.
While a category can be treated as an algebraic object like a group or a ring, this is not what most categorists are doing most of the time. Instead categorists are usually focused on larger categories like Set or Grp or R-Mod and/or classes (or typically categories) of categories like Abelian categories, toposes, or symmetric monoidally closed categories. Rather than "abstract data structures", these classes of categories are more like languages (this is what the notion of internal languages is about) and then specific categories in those classes are like models/semantics for the corresponding internal languages. That said, most categorists don't think that much about internal languages either (at least not as explicit, formal things). This is typical. Most group theorists don't study the proof-theoretic, metalogical properties of the theory of groups but instead study (classes of) the (set-theoretic) models of the the theory of groups, namely the groups themselves.
If you did want to see what the internal language of an arbitrary category looked like, that's effectively what I'm illustrating in this blog post. If you wanted something where the "types" were arbitrary categories, then you'd want to look at what internal languages Cat was a model for, or put another way, what categorical structure Cat supports. Something that's not presented as an internal language but you may find interesting is A Higher-Order Calculus for Categories by Cáccamo and Winskel.