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.)