People think of type theory as "internal language" of categories with certain properties (e.g. simply typed typed type theory for cartesian closed categories).

People think of type theory as "internal language" of categories with certain properties (e.g. simply typed typed type theory for cartesian closed categories). A formal way to say this is that the syntax of type theory gives rise to category with certain properties, and this category is initial among such categories. This means that it is, in a sense, the minimal category that satisfies these properties, so that all constructions in type theory give rise to this construction in every such category. To me personally, type theory feels a little like an ugly definition of this initial "category with X", and I'm currently exploring in my thesis whether a syntax derived from the categorical definitions itself could also be used for the same purpose as type theory is today.