Is there a word I can say which will convey to type theorists that I am not thinking about types as propositions?
Background: as a category theorist, I am mostly interested in type theories as a language to express and prove things about the categories in which they naturally have semantics. E.g. typed lambda-calculus in cartesian closed categories, dependent type theory in locally cartesian closed categories, etc. Such categorical models can also be used when thinking of types as propositions, of course, but usually I am thinking of types (i.e. the objects in the categories in question) as more like sets (or groupoids or higher groupoids, sometimes). Sometimes the type theory even includes a separate notion of "proposition" which is interpreted by monomorphisms in the category, e.g. the geometric logic or "higher-order type theory" of toposes.
Of course, I can say "categorical type theory" to refer to the whole programme of semantics for type theories in categories. However, if I want to talk only about the type theory side of things, but I don't want people to start calling types "propositions" and terms "proofs," what can I say to convey the point of view I want to take?