2 added 40 characters in body

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.

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.