As I’m being introduced and learning about these theories, I wanted to ask your help in putting things in perspective.
My impression at the moment is that Type is a more abstract theory than Category and that Topos is a more specific theory than Category.
And when I say abstract, I’m getting the impression that I could phrase that as a theory with many axioms and few derivations where when I say specific I’m getting the impression that I could phrase that to mean few axioms and many derivations
Are these impressions accurate?
If so, where does Homotopy Type Theory fit on this scale; does it make sense as in the title (more abstract than Category but more specific than Type?)
(EDIT: any commentary or discussion on how you personally view these theories along any metric would be very welcome and useful to me.)
I believe you are trying to approach the Type Theory-Category Theory duality from the wrong perspective.
Note: In what follows I'll assume that by Category Theory you are referring to the formal system (i.e. axiomatic theory) for categories, not to theory that studies categories a relations between them.
Both Type Theory (TT from here on) and Category Theory (CT) can be thought as abstract theories of functions. Nonetheless they are very different in their spirit: while TT tries to capture function application CT is interested in function composition. This difference produce two very different kind of theories that in my personal opinion can hardly being compared.
Of course there are relation between these two kind of theories: to every type system (a model of some theory of types) you can associate a category whose objects are contexts while morphisms are terms (i.e. functions in type theoretic language). Composition of morphisms is build through function application more or less how it is done for set theoretic functions.
On the other hand you can build from any category a type system whose types are basically the objects of the category and terms are build out of morphisms.
Going too deep in these two construction would require too much space so I suggest you to read this link and some book in categorical logic (I believe that every basic text book treat this kind of stuff).
Hope this helps.