show/hide this revision's text 2 added 40 characters in body

Short answer: two-level type theory.

In type theory the idea that sets and propositions should be distinguished has been considered (of course). Peter Aczel and (then) his student Nicola Gambino proposed a "two-level" type theory in which $\mathsf{Set}$ and $\mathsf{Prop}$ are not identified. More recently, Giovanni Sambin and Emillia Maietti proposed a similar treatment (I am not sure I've got the best reference here, please fix it), which I think is more general, as it deals with other issues in type theory (intensionality vs. extensionality).

So, if you want to speak to type-theorists you should use the following buzzwords:

  • "I am not identifying $\mathsf{Set}$ and $\mathsf{Prop}$, you know, in the style of Aczel and Gambino.", or
  • "We consider a type theory with separate kinds for sets and propositions."
  • "We do not assume that propositions are identified with types."

If you want to be more specific, for example if your notion of proposition is that of a subobject, you can say:

  • "For me propositions are the proof-irrelevant types."

Some people know the idea of proof-irrelevance under the heading of "squash types" or "bracket "types". It is also worth mentioning that the Coq proof assistant has different kinds for sets and propositions.
show/hide this revision's text 1

In type theory the idea that sets and propositions should be distinguished has been considered (of course). Peter Aczel and (then) his student Nicola Gambino proposed a "two-level" type theory in which $\mathsf{Set}$ and $\mathsf{Prop}$ are not identified. More recently, Giovanni Sambin and Emillia Maietti proposed a similar treatment (I am not sure I've got the best reference here, please fix it), which I think is more general, as it deals with other issues in type theory (intensionality vs. extensionality).

So, if you want to speak to type-theorists you should use the following buzzwords:

  • "I am not identifying $\mathsf{Set}$ and $\mathsf{Prop}$, you know, in the style of Aczel and Gambino.", or
  • "We consider a type theory with separate kinds for sets and propositions."
  • "We do not assume that propositions are identified with types."

If you want to be more specific, for example if your notion of proposition is that of a subobject, you can say:

  • "For me propositions are the proof-irrelevant types."

Some people know the idea of proof-irrelevance under the heading of "squash types" or "bracket "types". It is also worth mentioning that the Coq proof assistant has different kinds for sets and propositions.